Show simple item record

dc.contributor.authorBrucker, AD
dc.contributor.authorAit-Sadoune, I
dc.contributor.authorMéric, N
dc.contributor.authorWolff, B
dc.date.accessioned2023-05-22T08:24:19Z
dc.date.issued2023-05-15
dc.date.updated2023-05-21T12:10:19Z
dc.description.abstractIsabelle/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 λ-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.en_GB
dc.identifier.citationIn: Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, 30 May - 2 June 2023, edited by Uwe Glässer, Jose Creissac Campos, Dominique Méry, and Philippe Palanque, pp. 15 - 32. Lecture Notes in Computer Science volume 14010en_GB
dc.identifier.doi10.1007/978-3-031-33163-3_2
dc.identifier.urihttp://hdl.handle.net/10871/133205
dc.identifierORCID: 0000-0002-6355-1200 (Brucker, Achim D)
dc.identifierScopusID: 8868852700 (Brucker, Achim D)
dc.identifierResearcherID: J-7083-2013 (Brucker, Achim D)
dc.language.isoenen_GB
dc.publisherSpringeren_GB
dc.relation.ispartofseriesLecture Notes in Computer Science
dc.rights.embargoreasonUnder embargo until 15 May 2024 in compliance with publisher policyen_GB
dc.rights© The Author(s), under exclusive license to Springer Nature Switzerland AG 2023en_GB
dc.subjectOntologiesen_GB
dc.subjectFormal Documentsen_GB
dc.subjectFormal Developmenten_GB
dc.subjectIsabelle/HOLen_GB
dc.subjectOntology Mappingen_GB
dc.subjectCertificationen_GB
dc.titleUsing Deep Ontologies in Formal Software Engineeringen_GB
dc.typeConference paperen_GB
dc.date.available2023-05-22T08:24:19Z
dc.contributor.editorGlässer, U
dc.contributor.editorMéry, D
dc.identifier.isbn978-3-642-38915-3
exeter.place-of-publicationHeidelberg
dc.descriptionThis is the author accepted manuscript. The final version is available from Springer via the DOI on this recorden_GB
dc.relation.ispartofInternational Conference on Rigorous State Based Methods (ABZ 2023)
dc.rights.urihttp://www.rioxx.net/licenses/all-rights-reserveden_GB
rioxxterms.versionAMen_GB
rioxxterms.licenseref.startdate2023-05-15
rioxxterms.typeConference Paper/Proceeding/Abstracten_GB
refterms.dateFCD2023-05-22T08:22:07Z
refterms.versionFCDAM
refterms.panelBen_GB


Files in this item

This item appears in the following Collection(s)

Show simple item record