Abstract
Safety assurance using argument-based safety cases is an accepted best-practice in many safety-critical sectors. Goal Structuring Notation (GSN), which is widely used for presenting safety arguments graphically, provides a notion of modular arguments to support the goal of incremental certification. Despite the efforts at standardization, GSN remains an informal notation whereas the GSN standard contains appreciable ambiguity especially concerning modular extensions. This, in turn, presents challenges when developing tools and methods to intelligently manipulate modular GSN arguments. This paper develops the elements of a theory of modular safety cases, leveraging our previous work on formalizing GSN arguments. Using example argument structures we highlight some ambiguities arising through the existing guidance, present the intuition underlying the theory, clarify syntax, and address modular arguments, contracts, well-formedness and well-scopedness of modules. Based on this theory, we have a preliminary implementation of modular arguments in our toolset, AdvoCATE.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Assurance and Safety Case Environment, available at: http://www.adelard.com/asce/.
- 2.
To save space, we consider free variables to be implicitly universally quantified.
- 3.
The rationale is to directly resolve auxiliary subgoals internal to the contract, without needing to create an additional, external module.
- 4.
Recall that (modular) argument structures are forests.
- 5.
Module references are handled by item 2 of Definition 5.
- 6.
Note that the public goal node need not be the root of module M (Fig. 4a).
- 7.
A possible relaxation of this condition would be that modules can access child modules of siblings, i.e., in \(\mathcal {H}\), the module containing the target of an away node is \(\le \) the module containing the source node. Another possible relaxation is to allow a module access to its grandchildren. However, these alternatives limit the benefits of encapsulation.
References
Despotou, G., Kelly, T.: Investigating the use of argument modularity to optimise through-life system safety assurance. In: 3rd IET International Conference on System Safety, pp. 1–6, October 2008
Kelly, T.: Managing complex safety cases. In: Redmill, F., Anderson, T. (eds.) Current Issues in Safety-Critical Systems, pp. 99–115. Springer, London (2003)
Fenn, J., Hawkins, R., Williams, P., Kelly, T., Banner, M., Oakshott, Y.: The who, where, how, why and when of modular and incremental certification. In: 2nd IET International Conference on System Safety, pp. 135–140, October 2007
Goal Structuring Notation Working Group: GSN Community Standard v1, November 2011
Kelly, T., Bates, S.: The costs, benefits, and risks associated with pattern-based and modular safety case development. In: Proceedings UK MoD Equipment Safety Assurance Symposium, October 2005
Denney, E., Pai, G.: A formal basis for safety case patterns. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP. LNCS, vol. 8153, pp. 21–32. Springer, Heidelberg (2013)
Denney, E., Naylor, D., Pai, G.: Querying safety cases. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 294–309. Springer, Heidelberg (2014)
Object Management Group: Structured Assurance Case Metamodel (SACM) version 1.0. Formal/2013-02-01, February 2013
Denney, E., Pai, G., Pohl, J.: AdvoCATE: an assurance case automation toolset. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP Workshops 2012. LNCS, vol. 7613, pp. 8–21. Springer, Heidelberg (2012)
Fenn, J., Hawkins, R., Williams, P., Kelly, T.: Safety case composition using contracts - refinements based on feedback from an industrial case study. In: Proceedings of the 15th Safety Critical Systems Symposium (SSS 2007), February 2007
Industrial Avionics Working Group: Modular Software Safety Case Process GSN - MSSC 203 Issue 1, November 2012
Denney, E., Pai, G., Whiteside, I.: Formal foundations for hierarchical safety cases. In: Proceedings of the 16th International Symposium on High Assurance System Engineering (HASE 2015), January 2015
Warg, F., Vedder, B., Skoglund, M., Söderberg, A.: SafetyADD: a tool for safety-contract based design. In: Proceedings of the 25th International Symposium on Software Reliability Engineering Workshops (ISSREW 2014) (2014)
Kelly, T.: Concepts and principles of compositional safety case construction. In: Technical report COMSA/2001/1/1, University of York (2001)
Industrial Avionics Working Group: Modular Software Safety Case Process Description - MSSC 201 Issue 1, November 2012
Matsuno, Y.: A design and implementation of an assurance case language. In: 44th International Conference on Dependable Systems and Networks (DSN 2014), pp. 630–641, June 2014
Acknowledgements
We thank Jane Fenn (BAE Systems), Ibrahim Habli, and Richard Hawkins (University of York) for earlier discussions on modular GSN. We also thank the anonymous reviewers for their helpful comments. This work was supported by the SASO project of the NASA ARMD Airspace Operations and Safety Program.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Denney, E., Pai, G. (2015). Towards a Formal Basis for Modular Safety Cases. In: Koornneef, F., van Gulijk, C. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2014. Lecture Notes in Computer Science(), vol 9337. Springer, Cham. https://doi.org/10.1007/978-3-319-24255-2_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-24255-2_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24254-5
Online ISBN: 978-3-319-24255-2
eBook Packages: Computer ScienceComputer Science (R0)