Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

The ForeMoSt approach to building valid model-based safety arguments

  • Special Section Paper
  • Published:
Software and Systems Modeling Aims and scope Submit manuscript

Abstract

Safety assurance cases (ACs) are structured arguments designed to comprehensively show that a system is safe. ACs are often model-based, meaning that a model of the system is a primary subject of the argument. ACs use reasoning steps called strategies to decompose high-level claims about system safety into refined subclaims that can be directly supported by evidence. Strategies are often informal and difficult to rigorously evaluate in practice, and consequently, AC arguments often contain reasoning errors. This has led to the deployment of unsafe systems, and caused severe real-world consequences. These errors can be mitigated by formalizing and verifying AC strategies using formal methods; however, these techniques are difficult to use without formal methods expertise. To mitigate potential challenges faced by engineers when developing and interpreting formal ACs, we present ForeMoSt, our tool-supported framework for rigorously validating AC strategies using the Lean theorem prover. The goal of the framework is to straddle the level of abstraction used by the theorem prover and by software engineers. We use case studies from the literature to demonstrate that ForeMoSt is able to (i) augment and validate ACs from the research literature, (ii) support AC development for systems with large models, and (iii) support different model types.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16

Similar content being viewed by others

Notes

  1. Since the source code of LTSA is no longer available, we used its successor: the Modal Transition System Analyzer (MTSA) [19].

  2. Available at https://github.com/adisandro/MMINT.

  3. www.omg.org/spec/OCL

  4. The Lean listings shown in Sects. 4.6 and 6.3 have been slightly simplified for ease of presentation; for the complete Lean source code, see https://github.com/loganrjmurphy/ForeMoSt.

  5. For simplicity, our formalization makes some omissions. For instance, it only considers discrete traces, while OCRA supports both discrete and hybrid traces. Our formalization also assumes a synchronous model of communication between components.

References

  1. ISO: ISO26262: Road Vehicles—Functional Safety. ISO, Geneva (2011)

  2. SOTIF: ISO/PAS 21448:2019: Road Vehicles—Safety of the Intended Functionality. ISO (2019)

  3. Kelly, T.P.: Arguing safety: a systematic approach to managing safety cases. Ph.D. thesis, University of York, UK (1999)

  4. Nair, S., De La Vara, J.L., Sabetzadeh, M., Briand, L.: An extended systematic literature review on provision of evidence for safety certification. Inf. Softw. Technol. 56(7), 689–717 (2014)

    Article  Google Scholar 

  5. Goal Structuring Notation Community Standard (Version 2). Jan (2018)

  6. Barry, M.R.: CertWare: a workbench for safety case production and analysis. In: Proceedings of 2011 Aerospace Conference, pp. 1–10. IEEE (2011)

  7. Di Sandro, A., Selim, G.M.K., Salay, R., Viger, T., Chechik, M., Kokaly, S.: MMINT-A 2.0: tool support for the lifecycle of model-based safety artifacts. In: Proceedings of MODELS’20 Companion, pp. 15–1155. ACM (2020)

  8. Astah. https://astah.net/products/astah-gsn/ (2021)

  9. Ansys Medini Analyze. https://www.ansys.com/products/safety-analysis/ansys-medini-analyze (2021)

  10. IBM Rhapsody. https://www.ibm.com/docs/en/rhapsody (2021)

  11. Greenwell, W.S., Knight, J.C., Holloway, C.M., Pease, J.J.: A taxonomy of fallacies in system safety arguments. In: Proceedings of ISSC’06 (2006)

  12. Haddon-Cave, C.: The nimrod review: an independent review into the broader issues surrounding the loss of the RAF nimrod MR2 aircraft XV230 (2009)

  13. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371–384 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  14. Viger, T., Salay, R., Selim, G., Chechik, M.: Just enough formality in assurance argument structures. In: Proceedings of SAFECOMP’20, pp. 34–49. Springer (2020)

  15. Viger, T., Murphy, L., Di Sandro, A., Shahin, R., Chechik, M.: A lean approach to building valid model-based safety arguments. In: Proceedings of MODELS’21, pp. 194–204. IEEE (2021)

  16. Murphy, L., Viger, T., Di Sandro, A., Shahin, R., Chechik, M.: Validating safety arguments with lean. In: Proceedings of SEFM’21. LNCS, vol. 13085, pp. 23–43. Springer (2021)

  17. de Moura, L., Kong, S., Avigad, J., Van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Proceedings of CADE’15, pp. 378–388 (2015)

  18. Magee, J., Kramer, J.: State Models and Java Programs. Wiley, Hoboken (1999)

    MATH  Google Scholar 

  19. D’Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: Proceedings of ASE’08, pp. 475–476. IEEE (2008)

  20. Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. J. Autom. Softw. Eng. 12(3), 297–320 (2005)

    Article  Google Scholar 

  21. Sljivo, I., Gallina, B., Carlson, J., Hansson, H., Puri, S.: Tool-supported safety-relevant component reuse: from specification to argumentation. In: Ada-Europe International Conference on Reliable Software Technologies, pp. 19–33. Springer (2018)

  22. Sljivo, I., Gallina, B., Carlson, J., Hansson, H., Puri, S.: A method to generate reusable safety case argument-fragments from compositional safety analysis. J. Syst. Softw. 131, 570–590 (2017)

    Article  Google Scholar 

  23. Coquand, T., Paulin, C.: Inductively defined types. In: Proceedings of ICCL’88, pp. 50–66. Springer (1988)

  24. Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of ICFP’17, pp. 1–29. ACM (2017)

  25. GSN Working Group: GSN community standard version 2. http://www.goalstructuringnotation.info/. York, UK (2011)

  26. Denney, E., Pai, G.: Tool support for assurance case development. J. Autom. Softw. Eng. 25(3), 435–499 (2018)

    Article  Google Scholar 

  27. Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education, London (2008)

    Google Scholar 

  28. Bézivin, J., Jouault, F., Valduriez, P.: On the need for megamodels. In: OOPSLA/GPCE Workshops’04 (2004)

  29. Salay, R., Kokaly, S., Di Sandro, A., Fung, N.L.S., Chechik, M.: Heterogeneous megamodel management using collection operators. SoSyM 19(1), 231–260 (2020)

    Google Scholar 

  30. Dwyer, M., Avrunin, G., Corbett, J.: Property specification patterns for finite-state verification. In: Proceedings of Workshop on Formal Methods in Software Practice (1998)

  31. Di Sandro, A., Kokaly, S., Salay, R., Chechik, M.: Querying automotive system models and safety artifacts with MMINT and Viatra. In: Proceedings of MODELS’19 Companion, pp. 2–11. IEEE (2019)

  32. Di Sandro, A., Kokaly, S., Salay, R., Chechik, M.: Querying automotive system models and safety artifacts: tool support and case study. J. Automot. Softw. Eng. 1, 34–50 (2020)

    Article  Google Scholar 

  33. Varró, D., Bergmann, G., Hegedüs, Á., Horváth, Á., Ráth, I., Ujhelyi, Z.: Road to a Reactive and incremental model transformation platform: three generations of the VIATRA framework. Softw. Syst. Model. 15(3), 609–629 (2016)

    Article  Google Scholar 

  34. The Mathlib Community: The lean mathematical library. In: Proceedings of CPP’20. ACM (2020)

  35. Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P.L., Zhang, Y., Jetley, R.P.: Safety-assured development of the GPCA infusion pump software. In: Proceedings of EMSOFT’11, pp. 155–164. ACM (2011)

  36. Viger, T., Murphy, L., Di Sandro, A., Menghi, C., Shahin, R., Chechik, M.: The ForeMoSt approach to building valid model-based safety arguments. https://doi.org/10.5281/zenodo.6360845

  37. Ayoub, A., Kim, B., Lee, I., Sokolsky, O.: A safety case pattern for model-based development approach. In: Lecture Notes in Computer Science, vol. 7226, pp. 141–146. Springer (2012)

  38. Rushby, J., Xu, X., Rangarajan, M., Weaver, T.L.: Understanding and evaluating assurance cases. NASA Contractor Report NASA/CR-2015-218802, NASA Langley Research Center (2015)

  39. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  40. Arney, D.E., Jetley, R., Jones, P., Lee, I., Ray, A., Sokolsky, O., Zhang, Y.: Generic infusion pump hazard analysis and safety requirements version 1.0. Technical report, CIS (2009)

  41. Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163–203 (2011)

    Article  MATH  Google Scholar 

  42. Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217–238 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  43. Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Validation of requirements for hybrid systems: a formal approach. ACM Trans. Softw. Eng. Methodol. 21, 1–34 (2012)

    Article  Google Scholar 

  44. Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: Proceedings of ASE’13, pp. 702–705. IEEE Press (2013)

  45. Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333–348 (2015)

    Article  Google Scholar 

  46. Gérard, S., Dumoulin, C., Tessier, P., Selic, B.: Papyrus: a UML2 tool for domain-specific language modeling model-based engineering of embedded real-time systems, pp. 361–368 (2011)

  47. Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: Proceedings 38th Euromicro Conference on Software Engineering and Advanced Applications, pp. 21–28. IEEE (2012)

  48. Pakonen, A., Pang, C., Buzhinsky, I., Vyatkin, V.: User-friendly formal specification languages-conclusions drawn from industrial experience on model checking. In: 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA), pp. 1–8. IEEE (2016)

  49. Filipovikj, P., Jagerfield, T., Nyberg, M., Rodriguez-Navas, G., Seceleanu, C.: Integrating pattern-based formal requirements specification in an industrial tool-chain. In: 2016 IEEE 40th Annual Computer Software and Applications Conference (COMPSAC), vol. 2, pp. 167–173. IEEE (2016)

  50. Cobleigh, R.L., Avrunin, G.S., Clarke, L.A.: User guidance for creating precise and accessible property specifications. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 208–218 (2006)

  51. Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Proceedings of VMCAI’13. LNCS, vol. 7737, pp. 275–294. Springer (2013)

  52. Diskin, Z., Maibaum, T., Wassyng, A., Wynn-Williams, S., Lawford, M.: Assurance via model transformations and their hierarchical refinement. In: Proceedings of MODELS’18, pp. 426–436 (2018)

  53. Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T.: Isabelle/SACM: computer-assisted assurance cases with integrated formal methods. In: Proceedings of iFM’19, pp. 379–398. Springer (2019)

  54. Denney, E., Pai, G.: Automating the assembly of aviation safety cases. IEEE Trans. Reliab. 63(4), 830–849 (2014)

    Article  Google Scholar 

  55. Kelly, T., McDermid, J.: Safety case construction and reuse using patterns. In: Proceedings of SAFECOMP’97, pp. 55–69. Springer (1997)

  56. Picardi, C., Paterson, C., Hawkins, R.D., Calinescu, R., Habli, I.: Assurance argument patterns and processes for machine learning in safety-related systems. In: Proceedings of the Workshop on Artificial Intelligence Safety (SafeAI 2020), pp. 23–30. CEUR Workshop Proceedings (2020)

  57. Gleirscher, M., Carlan, C.: Arguing from hazard analysis in safety cases: a modular argument pattern. In: 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), pp. 53–60. IEEE (2017)

  58. Chowdhury, T., Lin, C.-W., Kim, B., Lawford, M., Shiraishi, S., Wassyng, A.: Principles for systematic development of an assurance case template from ISO 26262. In: International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 69–72. IEEE (2017)

  59. Hawkins, R., Kelly, T., Knight, J., Graydon, P.: A new approach to creating clear safety arguments. In: Advances in Systems Safety, pp. 3–23. Springer (2011)

  60. Chowdhury, T., Wassyng, A., Paige, R.F., Lawford, M.: Systematic evaluation of (safety) assurance cases. In: International Conference on Computer Safety, Reliability, and Security, pp. 18–33. Springer (2020)

  61. Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363–446 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  62. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: formal verification of an OS kernel. In: Proceedings of SOSP’09, pp. 207–220 (2009)

  63. Shahin, R., Kokaly, S., Chechik, M.: Towards certified analysis of software product line safety cases. In: Proceedings of SAFECOMP’21. LNCS, vol. 12852, pp. 130–145. Springer (2021)

  64. Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–9. IEEE (2018)

  65. Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for sat-based model checking. Formal Methods Syst. Des. 57(2), 178–210 (2021)

    Article  MATH  Google Scholar 

  66. Peled, D., Zuck, L.: From model checking to a temporal proof. In: International SPIN Workshop on Model Checking of Software, pp. 1–14. Springer (2001)

  67. Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L.D., Ghezzi, C.: From model checking to a temporal proof for partial models. In: Software Engineering and Formal Methods (SEFM), pp. 54–69. Springer (2017)

  68. Menghi, C., Rizzi, A.M., Bernasconi, A., Spoletini, P.: Torpedo: witnessing model correctness with topological proofs. Formal Aspects Comput. 33(6), 1039–1066 (2021)

    Article  MathSciNet  MATH  Google Scholar 

  69. Menghi, C., Rizzi, A.M., Bernasconi, A.: Integrating topological proofs with model checking to instrument iterative design. In: Fundamental Approaches to Software Engineering (FASE), pp. 53–74. Springer (2020)

  70. Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 362–376. Springer (2006)

Download references

Acknowledgements

We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC) (funding reference numbers RGPIN-2022-04622,DGECR-2022-00406). We are also grateful to anonymous reviewers for their help with improving this manuscript.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Toronto, Toronto, Canada

    Torin Viger, Logan Murphy, Alessio Di Sandro, Ramy Shahin & Marsha Chechik

  2. Department of Computing and Software, McMaster University, Hamilton, Canada

    Claudio Menghi

Authors
  1. Torin Viger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Logan Murphy
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alessio Di Sandro
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Claudio Menghi
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ramy Shahin
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Marsha Chechik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Torin Viger.

Additional information

Communicated by Shiva Nejati and Daniel Varro.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Viger, T., Murphy, L., Di Sandro, A. et al. The ForeMoSt approach to building valid model-based safety arguments. Softw Syst Model 22, 1473–1494 (2023). https://doi.org/10.1007/s10270-022-01063-4

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10270-022-01063-4

Keywords

Search

Navigation