Deriving and Formalising Safety and Security Requirements for Control Systems

  • Elena Troubitsyna
  • Inna VistbakkaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11093)


Safety-critical control systems become increasingly open and interconnected. However, there is still a lack of the techniques that enable an integrated analysis of safety and security requirements. In this paper, we propose an approach that allows the designers to derive and formalise safety and security requirements in a structured systematic way. To elicit both types of the requirements, we adapt and integrate traditional safety and security analysis techniques. To formally specify and verify them, we rely on Event-B framework. The framework allows us to develop a complex specification of system behaviour in presence of both accidental faults and security attacks and analyse mutual interdependencies between safety and security requirements.


Formal modelling Safety analysis Data flow Event-B Refinement Safety-critical systems Security 


  1. 1.
    Abrial, J.R.: Modeling in Event-B. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  2. 2.
    Brunel, J., Rioux, L., Paul, S., Faucogney, A., Vallée, F.: Formal safety and security assessment of an avionic architecture with alloy. In: ESSS 2014, pp. 8–19 (2014)Google Scholar
  3. 3.
    Bruza, P., van der Weide, T.P.: The Semantics of Data Flow Diagrams. Technical report 89-16, University of Nijmegen, The Netherlands (1989)Google Scholar
  4. 4.
    Bytschkow, D., Quilbeuf, J., Igna, G., Ruess, H.: Distributed MILS architectural approach for secure smart grids. In: Cuellar, J. (ed.) SmartGridSec 2014. LNCS, vol. 8448, pp. 16–29. Springer, Cham (2014). Scholar
  5. 5.
    Cimatti, A., DeLong, R., Marcantonio, D., Tonetta, S.: Combining MILS with contract-based design for safety and security requirements. In: Koornneef, F., van Gulijk, C. (eds.) SAFECOMP 2015. LNCS, vol. 9338, pp. 264–276. Springer, Cham (2015). Scholar
  6. 6.
    Fovino, I.N., Masera, M., Cian, A.D.: Integrating cyber attacks within fault trees. Rel. Eng. Sys. Saf. 94(9), 1394–1402 (2009)CrossRefGoogle Scholar
  7. 7.
    Iliasov, A., Romanovsky, A., Laibinis, L., Troubitsyna, E., Latvala, T.: Augmenting Event-B modelling with real-time verification. In: Proceedings of the FormSERA 2012, pp. 51–57. IEEE (2012)Google Scholar
  8. 8.
    Kriaa, S., Bouissou, M., Colin, F., Halgand, Y., Pietre-Cambacedes, L.: Safety and security interactions modeling using the bdmp formalism: case study of a pipeline. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 326–341. Springer, Cham (2014). Scholar
  9. 9.
    Laibinis, L., Troubitsyna, E.: Refinement of fault tolerant control systems in B. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 254–268. Springer, Heidelberg (2004). Scholar
  10. 10.
    Leveson, N.G.: Safeware: System Safety and Computers. Addison-Wesley, Boston (1995)Google Scholar
  11. 11.
    Lopatkin, I., Iliasov, A., Romanovsky, A., Prokhorova, Y., Troubitsyna, E.: Patterns for Representing FMEA in formal specification of control systems. In: HASE 2011, Boca Raton, FL, USA, pp. 146–151. IEEE Computer Society (2011)Google Scholar
  12. 12.
    Ministry of Defence: Interim Defence Standard 00–58/1: Hazop Studies on Systems Containing Programmable Electronics. In: Directorate of Standardization (1994)Google Scholar
  13. 13.
    Prokhorova, Y., Laibinis, L., Troubitsyna, E.: Facilitating construction of safety cases from formal models in Event-B. Inf. Softw. Technol. 60, 51–76 (2015)CrossRefGoogle Scholar
  14. 14.
    Rodin: Event-B platform.
  15. 15.
    Schmittner, C., Gruber, T., Puschner, P., Schoitsch, E.: Security application of failure mode and effect analysis (FMEA). In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 310–325. Springer, Cham (2014). Scholar
  16. 16.
    Schmittner, C., Ma, Z., Puschner, P.: Limitation and improvement of STPA-sec for safety and security co-analysis. In: Skavhaug, A., Guiochet, J., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9923, pp. 195–209. Springer, Cham (2016). Scholar
  17. 17.
    Sere, K., Troubitsyna, E.: Safety analysis in formal specication. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1564–1583. Springer, Heidelberg (1999). Scholar
  18. 18.
    Tarasyuk, A., Pereverzeva, I., Troubitsyna, E., Latvala, T., Nummila, L.: Formal development and assessment of a reconfigurable on-board satellite system. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012. LNCS, vol. 7612, pp. 210–222. Springer, Heidelberg (2012). Scholar
  19. 19.
    Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Towards probabilistic modelling in Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 275–289. Springer, Heidelberg (2010). Scholar
  20. 20.
    Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Integrating stochastic reasoning into event-B development. Form. Asp. Comput. 27(1), 53–77 (2015)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Troubitsyna, E.: Stepwise Development of Dependable Systems. Technical report (2000)Google Scholar
  22. 22.
    Troubitsyna, E., Laibinis, L., Pereverzeva, I., Kuismin, T., Ilic, D., Latvala, T.: Towards security-explicit formal modelling of safety-critical systems. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 213–225. Springer, Cham (2016). Scholar
  23. 23.
    Vistbakka, I., Troubitsyna, E., Kuismin, T., Latvala, T.: Co-engineering safety and security in industrial control systems: a formal outlook. In: Romanovsky, A., Troubitsyna, E.A. (eds.) SERENE 2017. LNCS, vol. 10479, pp. 96–114. Springer, Cham (2017). Scholar
  24. 24.
    Winther, R., Johnsen, O.-A., Gran, B.A.: Security assessments of safety critical systems using HAZOPs. In: Voges, U. (ed.) SAFECOMP 2001. LNCS, vol. 2187, pp. 14–24. Springer, Heidelberg (2001). Scholar
  25. 25.
    Young, W., Leveson, N.G.: An integrated approach to safety and security based on systems theory. Commun. ACM 57(2), 31–35 (2014)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.KTHStockholmSweden
  2. 2.Åbo Akademi UniversityTurkuFinland

Personalised recommendations