PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases | SpringerLink
Skip to main content
Springer Nature Link
Log in

PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15234))

Included in the following conference series:

  • 97 Accesses

Abstract

In critical software engineering, structured assurance cases (ACs) are used to demonstrate how key properties (e.g., safety, security) are supported by evidence artifacts (e.g., test results, proofs). ACs can also be studied as formal objects in themselves, such that formal methods can be used to establish their correctness. Creating rigorous ACs is particularly challenging in the context of software product lines (SPLs), wherein a family of related software products is engineered simultaneously. Since creating individual ACs for each product is infeasible, AC development must be lifted to the level of product lines. In this work, we propose \(\textsf{PLACIDUS}\), a methodology for integrating formal methods and software product line engineering to develop provably correct ACs for SPLs. To provide rigorous foundations for \(\textsf{PLACIDUS}\), we define a variability-aware AC language and formalize its semantics using the proof assistant Lean. We provide tool support for \(\textsf{PLACIDUS}\) as part of an Eclipse-based model management framework. Finally, we demonstrate the feasibility of \(\textsf{PLACIDUS}\) by developing an AC for a product line of medical devices.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 14871
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 18589
Price includes VAT (Japan)
  • 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

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Product Line Assurance Cases vIa DedUction and analySis.

  2. 2.

    Of course, there may be some product-level work which cannot be avoided; strictly speaking, \(\textsf{PLACIDUS}\) seeks to eliminate unnecessary product-based work.

  3. 3.

    https://github.com/loganrjmurphy/placs.

  4. 4.

    https://github.com/adisandro/MMINT.

References

  1. Alur, R., et al.: Formal specifications and analysis of the computer-assisted resuscitation algorithm (CARA) infusion pump control system. Int. J. Softw. Tools Technol. Transfer 5, 308–319 (2004)

    Article  Google Scholar 

  2. Alves, T., Teixeira, L., Alves, V., Castro, T.: Porting the software product line refinement theory to the coq proof assistant. In: Carvalho, G., Stolz, V. (eds.) SBMF 2020. LNCS, vol. 12475, pp. 192–209. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-63882-5_12

    Chapter  Google Scholar 

  3. Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product lines. Springer (2016)

    Google Scholar 

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

    Google Scholar 

  5. ter Beek, M.H., Damiani, F., Lienhardt, M., Mazzanti, F., Paolini, L.: Static analysis of featured transition systems. In: Proceedings of the 23rd International Systems and Software Product Line Conference-Volume A, pp. 39–51 (2019)

    Google Scholar 

  6. ter Beek, M.H., Damiani, F., Lienhardt, M., Mazzanti, F., Paolini, L., Scarso, G.: Fts4vmc: a front-end tool for static analysis and family-based model checking of ftss with vmc. Sci. Comput. Program. 224, 102879 (2022)

    Article  Google Scholar 

  7. Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Model checking software product lines with snip. Int. J. Softw. Tools Technol. Transfer 14, 589–612 (2012)

    Article  Google Scholar 

  8. Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, 416–439 (2014)

    Article  Google Scholar 

  9. Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1, pp. 335–344 (2010)

    Google Scholar 

  10. Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52335-9_47

    Chapter  Google Scholar 

  11. Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 275–294. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_18

    Chapter  Google Scholar 

  12. Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625–635. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_37

    Chapter  Google Scholar 

  13. de Oliveira, A.L., Braga, R.T.V., Masiero, P.C., Papadopoulos, Y., Habli, I., Kelly, T.: Supporting the automated generation of modular product line safety cases. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds.) Theory and Engineering of Complex Systems and Dependability. AISC, vol. 365, pp. 319–330. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19216-1_30

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  15. Denney, E., Pai, G.: Tool support for assurance case development. J. Automated Software Eng. 25(3), 435–499 (2018)

    Article  Google Scholar 

  16. Denney, E., Pai, G., Pohl, J.: AdvoCATE: an assurance case automation toolset. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012. LNCS, vol. 7613, pp. 8–21. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33675-1_2

    Chapter  Google Scholar 

  17. 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:1–15:5. ACM (2020)

    Google Scholar 

  18. Di Sandro, A., Shahin, R., Chechik, M.: Adding product-line capabilities to your favourite modeling language. In: Proceedings of the 17th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS’23), pp. 3–12 (2023)

    Google Scholar 

  19. Foster, S., Nemouchi, Y., Gleirscher, M., Wei, R., Kelly, T.: Integration of formal proof into unified assurance cases with Isabelle/Sacm. Formal Aspects Comput. 33(6), 855–884 (2021)

    Article  MathSciNet  Google Scholar 

  20. Habli, I.: Model-based assurance of safety-critical product lines. Ph.D. thesis, University of York (2009)

    Google Scholar 

  21. Habli, I., Kelly, T.: A safety case approach to assuring configurable architectures of safety-critical product lines. In: Giese, H. (ed.) ISARCS 2010. LNCS, vol. 6150, pp. 142–160. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13556-9_9

  22. Hall, C.V., Hammond, K., Peyton Jones, S.L., Wadler, P.L.: Type classes in haskell. ACM Trans. Program. Lang. Syst. (TOPLAS) 18(2), 109–138 (1996)

    Article  Google Scholar 

  23. ISO: ISO26262: Road vehicles – Functional safety (2011)

    Google Scholar 

  24. Kästner, C., Apel, S., Thüm, T., Saake, G.: Type checking annotation-based product lines. ACM Trans. Software Eng. Methodol. (TOSEM) 21(3), 1–39 (2012)

    Article  Google Scholar 

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

    Google Scholar 

  26. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  Google Scholar 

  27. Matsuno, Y.: A design and implementation of an assurance case language. In: 2014 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, pp. 630–641. IEEE (2014)

    Google Scholar 

  28. Murphy, L., Di Sandro, A., Shahin, R.I., Chechik, M.: Reusing your favourite analysis framework to handle workflows of product line models. In: Proceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A (2023). https://api.semanticscholar.org/CorpusID:261124727

  29. Nešić, D., Nyberg, M., Gallina, B.: Product-line assurance cases from contract-based design. J. Syst. Softw. 176, 110922 (2021)

    Article  Google Scholar 

  30. Rushby, J.: Formalism in safety cases. In: Dale, C., Anderson, T. (eds.) Making Systems Safer, pp. 3–17. Springer, London (2009). https://doi.org/10.1007/978-1-84996-086-1_1

  31. Rushby, J.: The interpretation and evaluation of assurance cases. Comp. Science Laboratory, SRI International, Technical report. SRI-CSL-15-01 (2015)

    Google Scholar 

  32. Salay, R., Famelis, M., Rubin, J., Di Sandro, A., Chechik, M.: Lifting model transformations to product lines. In: Proceedings of the 36th International Conference on Software Engineering, pp. 117–128 (2014)

    Google Scholar 

  33. Sandro, A.D., Salay, R., Famelis, M., Kokaly, S., Chechik, M.: MMINT: a graphical tool for interactive model management. In: Proceedings of the MoDELS 2015 Demo and Poster Session co-located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2015), Ottawa, Canada, September 27, 2015. CEUR Workshop Proceedings, vol. 1554, pp. 16–19. CEUR-WS.org (2015). https://ceur-ws.org/Vol-1554/PD_MoDELS_2015_paper_6.pdf

  34. Shahin, R., Chechik, M., Salay, R.: Lifting datalog-based analyses to software product lines. In: Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 39–49 (2019)

    Google Scholar 

  35. Shahin, R., Kokaly, S., Chechik, M.: Towards certified analysis of software product line safety cases. In: Habli, I., Sujan, M., Bitsch, F. (eds.) SAFECOMP 2021. LNCS, vol. 12852, pp. 130–145. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-83903-1_9

    Chapter  Google Scholar 

  36. Sljivo, I., Gallina, B., Carlson, J., Hansson, H., Puri, S.: Tool-supported safety-relevant component reuse: from specification to argumentation. In: Casimiro, A., Ferreira, P.M. (eds.) Ada-Europe 2018. LNCS, vol. 10873, pp. 19–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92432-8_2

    Chapter  Google Scholar 

  37. Takeyama, M.: Towards formal assurance case framework in Agda (2014). https://cs.ioc.ee/~tarmo/tsem14/takeyama-slides.pdf

  38. Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. (CSUR) 47(1), 1–45 (2014)

    Article  Google Scholar 

  39. Thüm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, pp. 11–20 (2012)

    Google Scholar 

  40. Varadarajan, S., et al.: Clarissa: foundations, tools & automation for assurance cases. In: 2023 IEEE/AIAA 42nd Digital Avionics Systems Conference (DASC), pp. 1–10. IEEE (2023)

    Google Scholar 

  41. 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. Software Syst. Model. 15(3), 609–629 (2016)

    Article  Google Scholar 

  42. Viger, T., Murphy, L., Di Sandro, A., Menghi, C., Shahin, R., Chechik, M.: The foremost approach to building valid model-based safety arguments. Softw. Syst. Model. 22(5), 1473–1494 (2023)

    Article  Google Scholar 

  43. Viger, T., Salay, R., Selim, G., Chechik, M.: Just enough formality in assurance argument structures. In: Casimiro, A., Ortmeier, F., Bitsch, F., Ferreira, P. (eds.) SAFECOMP 2020. LNCS, vol. 12234, pp. 34–49. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54549-9_3

    Chapter  Google Scholar 

  44. Walkingshaw, E., Kästner, C., Erwig, M., Apel, S., Bodden, E.: Variational data structures: exploring tradeoffs in computing with variability. In: Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, pp. 213–226 (2014)

    Google Scholar 

  45. Zhang, Y., Jones, P.L., Jetley, R.: A hazard analysis for a generic insulin infusion pump. J. Diabetes Sci. Technol. 4(2), 263–283 (2010)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Toronto, Toronto, Canada

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

Authors
  1. Logan Murphy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Torin Viger
    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. Marsha Chechik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Logan Murphy .

Editor information

Editors and Affiliations

  1. Thales Research and Technology, Palaiseau, France

    Nikolai Kosmatov

  2. TU Wien, Vienna, Austria

    Laura Kovács

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Murphy, L., Viger, T., Sandro, A.D., Chechik, M. (2025). PLACIDUS: Engineering Product Lines of Rigorous Assurance Cases. In: Kosmatov, N., Kovács, L. (eds) Integrated Formal Methods. IFM 2024. Lecture Notes in Computer Science, vol 15234. Springer, Cham. https://doi.org/10.1007/978-3-031-76554-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-76554-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-76553-7

  • Online ISBN: 978-3-031-76554-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation