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

Using Ontologies in Formal Developments Targeting Certification

A common problem in the certification of highly safety or security critical systems is the consistency of the certification documentation in general and, in particular, the linking between semiformal and formal content of the certification documentation.

We address this problem by using an existing framework, Isabelle/DOF, that allows writing certification documents with consistency guarantees, in both, the semiformal and formal parts. Isabelle/DOF supports the modeling of document ontologies using a strongly typed ontology definition language. An ontology is then enforced inside documents including formal parts, e.g., system models, verification proofs, code, tests and validations of corner-cases. The entire set of documents is checked within Isabelle/HOL, which includes the definition of ontologies and the editing of integrated documents based on them. This process is supported by an IDE that provides continuous checking of the document consistency.

In our iFM paper [1], we present how a specific software-engineering certification standard, namely CENELEC 50128, can be modeled inside Isabelle/DOF. Based on an ontology covering a substantial part of this standard, we present how Isabelle/DOF can be applied to a certification case-study in the railway domain.


A. D. Brucker and B. Wolff, “Using ontologies in formal developments targeting certification,” in Integrated formal methods (iFM), W. Ahrendt and S. L. T. Tarifa, Eds. Heidelberg: Springer-Verlag, 2019. doi: 10.1007/978-3-030-34968-4_4.

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