Advertisement

Using Ontologies in Formal Developments Targeting Certification

  • Achim D. BruckerEmail author
  • Burkhart Wolff
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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, Open image in new window, that allows writing certification documents with consistency guarantees, in both, the semi-formal and formal parts. Open image in new window 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 Open image in new window. Based on an ontology covering a substantial part of this standard, we present how Open image in new window 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 

Notes

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.”

References

  1. 1.
  2. 2.
    The neon toolkit (2018). http://neon-toolkit.org
  3. 3.
    Owlgred (2018). http://owlgred.lumii.lv/
  4. 4.
  5. 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_29CrossRefGoogle Scholar
  6. 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. 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_7CrossRefGoogle Scholar
  8. 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_3CrossRefGoogle Scholar
  9. 9.
    Brucker, A.D., Wolff, B.: Isabelle/DOF (2019). https://doi.org/10.5281/zenodo.3370483
  10. 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_15CrossRefGoogle Scholar
  11. 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. 12.
    Common Criteria: Common criteria for information technology security evaluation (version 3.1), Part 3: Security assurance components (2006). CCMB-2006-09-003
  13. 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-8CrossRefzbMATHGoogle Scholar
  14. 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. 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_8CrossRefGoogle Scholar
  16. 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. 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_8CrossRefGoogle Scholar
  18. 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_12CrossRefGoogle Scholar
  19. 19.
    Kelly, T., Weaver, R.: The goal structuring notation - a safety argument notation. In: Dependable Systems and Networks (2004)Google Scholar
  20. 20.
    Klein, G.: Operating system verification – an overview. Sādhanā 34(1), 27–69 (2009)MathSciNetCrossRefGoogle Scholar
  21. 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/2560537CrossRefGoogle Scholar
  22. 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-9CrossRefzbMATHGoogle Scholar
  23. 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 1993Google Scholar
  24. 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_33CrossRefGoogle Scholar
  25. 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.10CrossRefGoogle Scholar
  26. 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)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.University of ExeterExeterUK
  2. 2.LRIUniversité Paris-SaclayParisFrance

Personalised recommendations