Isabelle/DOF: Design and Implementation

By Achim D. Brucker and Burkhart Wolff.

DOF is a novel framework for defining ontologies and enforcing them during document development and 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 the formal methods framework Isabelle/HOL. A particular emphasis is put on a deep integration into Isabelleâs IDE, which allows for smooth ontology development as well as immediate ontological feedback during the editing of a document.

In this paper, 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 collabo- ratively, while ensuring their consistency, and the impact of changes (in the formal and the semi-formal content) is tracked automatically.

Keywords:
Ontology, Formal Document Development, Certification, DOF, Isabelle/DOF

Please cite this work as follows:
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. Author copy: https://logicalhacking.com/publications/brucker.ea-isabelledof-2019/

BibTeX
@InCollection{ brucker.ea:isabelledof:2019,
  abstract  = {DOF is a novel framework for defining ontologies and
               enforcing them during document development and 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 the formal methods framework
               Isabelle/HOL. A particular emphasis is put on a deep
               integration into Isabelle{\^a}s IDE, which allows for smooth
               ontology development as well as immediate ontological feedback
               during the editing of a document.
               
               In this paper, we give an in-depth presentation of the design
               concepts of DOF{\^a}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 collabo- ratively, while ensuring their consistency,
               and the impact of changes (in the formal and the semi-formal
               content) is tracked automatically.},
  keywords  = {Ontology, Formal Document Development, Certification, DOF,
               Isabelle/DOF},
  location  = {Oslo},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Software Engineering and Formal Methods (SEFM)},
  language  = {USenglish},
  pages     = {275--292},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {11724},
  isbn      = {3-540-25109-X},
  doi       = {10.1007/978-3-030-30446-1_15},
  editor    = {Peter C. {\"O}lveczky and Gwen Sala{\"u}n},
  title     = {{Isabelle/DOF}: Design and Implementation},
  areas     = {formal methods, software},
  year      = {2019},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-isabelledof-2019/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-isabelledof-2019/brucker.ea-isabelledof-2019.pdf},
}