Using Ontologies in Formal Developments Targeting Certification

by Achim D. Brucker and Burkhart Wolff

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 semi-formal 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 semi-formal 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 this paper, 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.

Keywords: Certification of Safety-Critical Systems, CENELEC 50128, Formal Document Development, Isabelle/DOF, Isabelle/HOL
Categories: ,
Documents: (full text as PDF file)

Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff. Using Ontologies in Formal Developments Targeting Certification. In Integrated Formal Methods (iFM). Lecture Notes in Computer Science (11918), Springer-Verlag, 2019.
Keywords: Certification of Safety-Critical Systems, CENELEC 50128, Formal Document Development, Isabelle/DOF, Isabelle/HOL
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-030-34968-4_4) ( )