Using Deep Ontologies in Formal Software Engineering

@InCollection{ brucker.ea:deep-ontologies:2023,
  abstract  = {Isabelle/DOF is an ontology framework on top of Isabelle. It
               allows for the formal development of ontologies as well as
               continuous conformity-checking of integrated documents
               annotated by ontological data. An integrated document may
               contain text, code, definitions, proofs, and user-programmed
               constructs supporting a wide range of formal methods.
               Isabelle/DOF is designed to leverage traceability in inte-
               grated documents by supporting navigation in Isabelle's IDE as
               well as the document generation process.
               
               In this paper, we extend Isabelle/DOF with annotations of
               $\lambda$-terms, a pervasive data-structure underlying
               Isabelle used to syntactically represent expressions and
               formulas. Rather than introducing an own pro- gramming
               language for meta-data, we use Higher-order Logic (HOL) for
               expressions, data-constraints, ontological invariants, and
               queries via code-generation and reflection. This allows both
               for powerful query languages and logical reasoning over
               ontologies in, for example, ontological mappings. Our
               application examples cover documents targeting formal
               certifications such as CENELEC 50128 or Common Criteria.
               
               },
  keywords  = {Ontologies, Formal Documents, Formal Development,
               Isabelle/HOL, Ontology Mapping, Certification},
  location  = {Loria, Nance, France},
  author    = {Achim D. Brucker and Idir Ait-Sadoune and Nicolas M{\'e}ric
               and Burkhart Wolff},
  booktitle = {International Conference on Rigorous State Based Methods (ABZ
               2023)},
  language  = {english},
  doi       = {},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {},
  editor    = {Uwe Gl{\"a}sser and Dominique M{\'e}ry},
  title     = {Using Deep Ontologies in Formal Software Engineering},
  areas     = {formal methods, software engineering},
  year      = {2023},
  isbn      = {978-3-642-38915-3},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-deep-ontologies-2023/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-deep-ontologies-2023/brucker.ea-deep-ontologies-2023.pdf},
}