Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Isabelle/DOF: Design and Implementation

DOF is a novel framework for defining ontologies and en- forcing them during document development and document evolution. A major goal of DOF is the integrated development of formal certification documents (e.g., for Common Criteria or CENELEC 50128) that require consistency across both formal and informal arguments.

To support a consistent development of formal and informal parts of a document, we provide Isabelle/DOF, an implementation of DOF on top of Isabelle/HOL. Isabelle/DOF is integrated into Isabelle’s IDE, which allows for smooth ontology development as well as immediate ontological feedback during the editing of a document.

In our SEFM paper [1], we give an in-depth presentation of the design concepts of DOF’s Ontology Definition Language (ODL) and key aspects of the technology of its implementation. Isabelle/DOF is the first ontology language supporting machine-checked links between the formal and informal parts in an LCF-style interactive theorem proving environment. Sufficiently annotated, large documents can easily be developed collaboratively, while ensuring their consistency, and the impact of changes (in the formal and the semiformal content) is tracked automatically.


A. D. Brucker and B. Wolff, Isabelle/DOF: Design and implementation,” in Software engineering and formal methods (SEFM), P. C. Ölveczky and G. Salaün, Eds. Heidelberg: Springer-Verlag, 2019, pp. 275–292. doi: 10.1007/978-3-030-30446-1_15.

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site