Developing an Ontology for Certification Norms in Isabelle_DOF

Description

Isabelle/DOF [1,2,4] is a framework for the development of formal ontologies that can be linked to formal developments containing texts, code, tests, and, least but not least, definitions and proofs in Isabelle/HOL. See Isabelle DOF Design Principle Meeting. While in principle versatile and usable in a wide range of application domains ranging from knowledge-aware text-processing to type-safe FM-tool exchange formats, an initial motivation of Isabelle/DOF's development was the use of documentation containing formal definitions and proofs targeting formal certifications such as CENELEC 50128 [3,7,8] or Common Criteria [6].

The goal of this project is to provide a larger case study addressing either:

• ... the extension of an existing Isabelle/DOF ontology [5] for CENELEC 50128 to a larger fragment of the standard. This includes the modeling of ontological rules ("invariants") implicit in the standard such that they can be supported by Isabelle/DOF while editing a certification document according this standard
• ... or the development from scratch of an analogous Isabelle/DOF ontology for Common Criteria[6]

Proceeding

After a study of both (semiformal) certification standards, a decision over the target is made. Then an extension/analogue of [5] is developed in Isabelle/DOF, together with a suite of micro-examples. Finally, specific presentation support for categories of the standard is developed (example: generation of the table of requirements in an annex).

Work Plan

• study of standards, report of the state of the art
• identifying key-features of the standard (such as: roles or certification levels) and their impact on classes
• developing invariants and deriving editing support
• developing a suite of micro-examples together with LaTeX templates.

Required Skills

• Understanding of Software Development Processes (for example, L3-GLA course, ...)
• Interest in (semi-formal) standards and software development targeting a certification
• Understanding of UML, OCL, Meta-Modeling, Ontologies helpful
• basics in logic and functional programming
• no knowledge of theorem proving necessary.

Bibliography

[1] Achim D. Brucker, Burkhart Wolff:

    Isabelle/DOF: Design and Implementation. SEFM 2019: 275-292

[2] Achim D. Brucker, Idir Aït-Sadoune, Paolo Crisafulli, Burkhart Wolff:

    Using the Isabelle Ontology Framework - Linking the Formal with the Informal. CICM 2018: 23-38

[3] Achim D. Brucker, Burkhart Wolff:

    Using Ontologies in Formal Developments Targeting Certification. IFM 2019: 65-82

[4] Repositories:

    Exeter Logical Hacking
    The Isabelle_DOF Zenodo page

[5] The CENELEC 50128 Ontology Model (Fragment):

    src

[6] Common Criteria: Common criteria for information technology security evaluation (version 3.1),

    Part 3: Security assurance components (2006). CCMB-2006-09-003

[7] Jean-Louis Boulanger, Q. Ochem (for ADACORE) : CENELEC 50128

    pdf

[8] CENELEC EN 50128: Railway Applications -Communication, signaling and processing systems, Software for railway control and protection systems. pdf available on demand.

Skillset

• good functional programming skills
• interest in formal software engineering and certification processes
• no knowledge in theorem proving necessary