Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2019: Integrated Formal Methods pp 65–82Cite as

Using Ontologies in Formal Developments Targeting Certification

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11918))

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, , that allows writing certification documents with consistency guarantees, in both, the semi-formal and formal parts. 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 . Based on an ontology covering a substantial part of this standard, we present how can be applied to a certification case-study in the railway domain.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Availability

The framework [9], the discussed ontology definitions, and examples are available at https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/. is licensed under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).

Notes

  1. 1.

    The company SYSGO/Thales behind this initiative finally abandoned the approach and restarted a certification on a later version.

References

  1. Fluent editor (2018). http://www.cognitum.eu/Semantics/FluentEditor/

  2. The neon toolkit (2018). http://neon-toolkit.org

  3. Owlgred (2018). http://owlgred.lumii.lv/

  4. Protégé (2018). https://protege.stanford.edu

  5. Barras, B., et al.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 359–363. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_29

    Chapter  Google Scholar 

  6. Bezzecchi, S., Crisafulli, P., Pichot, C., Wolff, B.: Making agile development processes fit for V-style certification procedures. In: ERTS Conference Proceedings (2018)

    Google Scholar 

  7. Bicchierai, I., Bucci, G., Nocentini, C., Vicario, E.: Using ontologies in the integration of structural, functional, and process perspectives in the development of safety critical systems. In: Keller, H.B., Plödereder, E., Dencker, P., Klenk, H. (eds.) Ada-Europe 2013. LNCS, vol. 7896, pp. 95–108. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38601-5_7

    Chapter  Google Scholar 

  8. Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B.: Using the isabelle ontology framework. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 23–38. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96812-4_3

    Chapter  Google Scholar 

  9. Brucker, A.D., Wolff, B.: Isabelle/DOF (2019).https://doi.org/10.5281/zenodo.3370483

  10. Brucker, A.D., Wolff, B.: Isabelle/DOF: design and implementation. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 275–292. Springer, Cham (2019b). https://doi.org/10.1007/978-3-030-30446-1_15

    Chapter  Google Scholar 

  11. BS EN 50128:2011: Bs en 50128:2011: Railway applications - communication, signalling and processing systems - software for railway control and protecting systems. Standard, Britisch Standards Institute (BSI) (2014)

    Google Scholar 

  12. Common Criteria: Common criteria for information technology security evaluation (version 3.1), Part 3: Security assurance components (2006). CCMB-2006-09-003

  13. Daum, M., Dörrenbächer, J., Wolff, B.: Proving fairness and implementation correctness of a microkernel scheduler. J. Autom. Reasoning 42(2), 349–388 (2009). https://doi.org/10.1007/s10817-009-9119-8

    Article  MATH  Google Scholar 

  14. Denney, E., Pai, G.: Evidence arguments for using formal methods in software certification. In: IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 375–380 (2013). https://doi.org/10.1109/ISSREW.2013.6688924

  15. Ekclhart, A., Fenz, S., Goluch, G., Weippl, E.: Ontological mapping of common criteria’s security assurance requirements. In: Venter, H., Eloff, M., Labuschagne, L., Eloff, J., von Solms, R. (eds.) SEC 2007. IIFIP, vol. 232, pp. 85–95. Springer, Boston, MA (2007). https://doi.org/10.1007/978-0-387-72367-9_8

    Chapter  Google Scholar 

  16. Gleirscher, M., Ratiu, D., Schatz, B.: Incremental integration of heterogeneous systems views. In: 2007 International Conference on Systems Engineering and Modeling, pp. 50–59 (2007). https://doi.org/10.1109/ICSEM.2007.373334

  17. Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 99–115. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_8

    Chapter  Google Scholar 

  18. Kaluvuri, S.P., Bezzi, M., Roudier, Y.: A quantitative analysis of common criteria certification practice. In: Eckert, C., Katsikas, S.K., Pernul, G. (eds.) TrustBus 2014. LNCS, vol. 8647, pp. 132–143. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09770-1_12

    Chapter  Google Scholar 

  19. Kelly, T., Weaver, R.: The goal structuring notation - a safety argument notation. In: Dependable Systems and Networks (2004)

    Google Scholar 

  20. Klein, G.: Operating system verification – an overview. Sādhanā 34(1), 27–69 (2009)

    Article  MathSciNet  Google Scholar 

  21. Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2:1–2:70 (2014). https://doi.org/10.1145/2560537

    Article  Google Scholar 

  22. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  23. Rushby, J.: Formal methods and the certification of critical systems. Technical report SRI-CSL-93-7, Computer Science Laboratory, SRI International, Menlo Park, CA (1993). Also issued under the title Formal Methods and Digital Systems Validation for Airborne Systems as NASA Contractor Report 4551, December 1993

    Google Scholar 

  24. Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515–530. Springer, Cham (2014a). https://doi.org/10.1007/978-3-319-08970-6_33

    Chapter  Google Scholar 

  25. Wenzel, M.: System description: Isabelle/jEdit in 2014. In: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014, pp. 84–94 (2014b). https://doi.org/10.4204/EPTCS.167.10

    Article  Google Scholar 

  26. Zhao, Y., Sanán, D., Zhang, F., Liu, Y.: Formal specification and analysis of partitioning operating systems by integrating ontology and refinement. IEEE Trans. Ind. Inf. 12(4), 1321–1331 (2016)

    Article  Google Scholar 

Download references

Acknowledgments

This work has been partially supported by IRT SystemX, Paris-Saclay, France, and therefore granted with public funds of the Program “Investissements d’Avenir.”

Author information

Authors and Affiliations

  1. University of Exeter, Exeter, UK

    Achim D. Brucker

  2. LRI, Université Paris-Saclay, Paris, France

    Burkhart Wolff

Authors
  1. Achim D. Brucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Burkhart Wolff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Achim D. Brucker .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. University of Oslo, Oslo, Norway

    Silvia Lizeth Tapia Tarifa

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Brucker, A.D., Wolff, B. (2019). Using Ontologies in Formal Developments Targeting Certification. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34968-4_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34967-7

  • Online ISBN: 978-3-030-34968-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation