Parametric Ontologies in Formal Software Engineering

@Article{ brucker.ea:parametric-ontologies:2025,
  title     = {Parametric Ontologies in Formal Software Engineering},
  journal   = {Science of Computer Programming},
  volume    = {},
  pages     = {},
  areas     = {formal methods, software},
  year      = {2025},
  issn      = {0167-6423},
  doi       = {10.1016/j.scico.2024.103231},
  author    = {Achim D. Brucker and Idir Ait-Sadoune and Nicolas M{\'e}ric
               and Burkhart Wolff},
  keywords  = {Ontologies, Generic Classes, Ontology Mapping, Formal
               Development, Formal Documents, Isabelle/HOL, Software
               Engineering, Certification},
  abstract  = {Isabelle/DOF is an ontology framework on top of Isabelle/HOL.
               It allows for the formal development of ontologies and
               continuous conformity-checking of integrated documents,
               including the tracing of typed meta-data of documents.
               Isabelle/DOF deeply integrates into the Isabelle/HOL
               ecosystem, allowing to write documents containing (informal)
               text, executable code, (formal and semi- formal) definitions,
               and proofs. Users of Isabelle/DOF can either use HOL or one of
               the many formal methods that have been embedded into
               Isabelle/HOL to express formal parts of their documents. In
               this paper, we extend Isabelle/DOF with annotations of
               lambda-terms, a pervasive data-structure underlying Isabelle
               to syntactically represent expressions and formulas. We
               achieve this by using Higher-order Logic (HOL) itself for
               query-expressions and data-constraints (ontological
               invariants) executed via code-generation and reflection.
               Moreover, we add support for parametric onto- logical classes,
               thus exploiting HOL's polymorphic type system. The benefits
               are: First, the HOL representation allows for flexible and
               efficient run-time checking of abstract properties of formal
               content under evolution. Second, it is possible to prove
               properties over generic ontological classes. We demonstrate
               these new features by a number of smaller ontologies from
               various domains and a case study using a substantial ontology
               for formal system development targeting certification
               according to CENELEC 50128.},
  publisher = {Elsevier Science Publishers },
  address   = {Amsterdam },
  note      = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-parametric-ontologies-2025/}},
}