Abstract
Survivability is a property of systems that guarantees services which operate safe and timely. Safety-critical services must survive despite the presence of faults or attacks. The contribution of the paper is twofold: construction of a survivability assessment model (SAM) and its transformation to a model checking problem. Our SAM is automatically obtained from an improved specification of misuse cases, which encompasses essential services, threats and survivability strategies. The SAM is automatically converted, using model-driven techniques, into a Petri Net model for verifying survivability properties through model checking. The method has been applied to a military command-and-control information system.
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
Similar content being viewed by others
Notes
- 1.
The choice node is graphically represented by the diamond shape.
- 2.
Petri Nets have well-established properties, such as home state, which are usually defined in terms of place markings and transition firings [15].
- 3.
To avoid cluttering, the figure shows only the essential services considered in this iteration.
- 4.
Observe that attack is a transient fault.
References
Alexander, I.: Misuse cases: use cases with hostile intent. IEEE Softw. 20(1), 58–66 (2003)
Allenby, K., Kelly, K.: Deriving safety requirements using scenarios. In: International Conference on Requirements Engineering, pp. 228–235. IEEE Computer Society (2001)
Avizienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secure Comput. 01(1), 11–33 (2004)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)
Donzelli, P., Basili, V.: A practical framework for eliciting and modeling system dependability requirements: experience from the NASA high dependability computing project. J. Syst. Softw. 79, 107–119 (2006)
Diedrichsen, L.D.: Command & Control operational requirements and system implementation. Inf. Secur. Int. J. 5, 23–40 (2000)
Ellison, R.J., Linger, R.C., Longstaff, T., Mead, N.R.: Survivable network system analysis: a case study. IEEE Softw. 16(4), 70–77 (1999)
Girault, C., Valle, R. (eds.): System Engineering: A Petri Net Based Approach to Modelling, Verification and Implementation, Chapter: State Space Based Methods and Model Checking, pp. 171–190. KRONOS (1998)
Iwu, F., Galloway, A., McDermid, J., Toyn, J.: Integrating safety and formal analyses using UML and PFS. Reliab. Eng. Syst. Saf. 92(2), 156–170 (2007)
Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison Wesley, Reading (1999)
Knight, J.C., Strunk, E.A.: Achieving critical system survivability through software architectures. In: de Lemos, R., Gacek, C., Romanovsky, A. (eds.) Architecting Dependable Systems II. LNCS, vol. 3069, pp. 51–78. Springer, Heidelberg (2004)
Kruchten, P.: The Rational Unified Process: An Introduction. Addison-Wesley Longman Publishing, Boston (2003)
Mustafiz, S., Kienzle, J., Berlizev, A.: Addressing degraded service outcomes and exceptional modes of operation in behavioural models. In: Proceedings of the RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, SERENE 2008, pp. 19–28. ACM, New York (2008)
Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13(1), 45–60 (1981)
Reisig, W.: Petri Nets. An Introduction. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1985)
Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual, 2nd edn. Addison Wesley, Reading (2004)
Varpaaniemi, K., Heljanko, K., Lilius, J.: PROD 3.2 — an advanced tool for efficient reachability analysis. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 472–475. Springer, Heidelberg (1997)
Acknowledgements
Special thanks to the Lieutenant Colonel Félix Borque Pérez of the CASIOPEA centre at CENAD “San Gregorio‘” (Zaragoza, Spain) for his help in gathering the C2IS requirements. This work has been supported by the Spanish projects TIN2011-24932 and TIN2013-46238-C4-1-R of the Ministerio de Economía y Competitividad, and by the Distributed Computation (DisCo) research group of the Aragonese Government (Ref. T94).
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
Bernardi, S., Dranca, L., Merseguer, J. (2015). Modelling and Verification of Survivability Requirements for Critical Systems. In: Canal, C., Idani, A. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science(), vol 8938. Springer, Cham. https://doi.org/10.1007/978-3-319-15201-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-15201-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-15200-4
Online ISBN: 978-3-319-15201-1
eBook Packages: Computer ScienceComputer Science (R0)