
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
Please cite this work as follows: 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. Author copy: https://logicalhacking.com/publications/brucker.ea-ontologies-certification-2019/
@InCollection{ brucker.ea:ontologies-certification:2019,
abstract = {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\emph{modeling} of document
parts. Isabelle/DOF supports the
ontologies using a strongly typed ontology definition\emph{enforced} inside documents
language. An ontology is then
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},location = {Bergen},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Integrated Formal Methods (iFM)},
language = {USenglish},
publisher = {Springer-Verlag },
address = {Heidelberg },
series = {Lecture Notes in Computer Science },
number = {11918},
isbn = {3-540-25109-X},
doi = {10.1007/978-3-030-34968-4_4},
editor = {Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa},
title = {Using Ontologies in Formal Developments Targeting
Certification},areas = {formal methods, software},
year = {2019},
note = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-ontologies-certification-2019/}},
pdf = {https://logicalhacking.com/publications/brucker.ea-ontologies-certification-2019/brucker.ea-ontologies-certification-2019.pdf},
}