Towards Security-Explicit Formal Modelling of Safety-Critical Systems

  • Elena Troubitsyna
  • Linas LaibinisEmail author
  • Inna Pereverzeva
  • Tuomas Kuismin
  • Dubravka Ilic
  • Timo Latvala
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9922)


Modern industrial control systems become increasingly interconnected and rely on external networks to provide their services. Hence they become vulnerable to security attacks that might directly jeopardise their safety. The growing understanding that if the system is not secure then it is not safe calls for novel development and verification techniques weaving security consideration into the safety-driven design. In this paper, we demonstrate how to make explicit the relationships between safety and security in the formal system development by refinement. The proposed approach allows the designers to identify at early design states mutual interdependencies between the mechanisms ensuring safety and security and build robust system architecture.



This work is partially funded by the TEKES project Cyber Trust.


  1. 1.
    Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)CrossRefzbMATHGoogle 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, EPTCS, vol. 150, pp. 8–19 (2014)Google Scholar
  3. 3.
    Cimatti, A., DeLong, R., Marcantonio, D., Tonetta, S.: Combining MILS with contract-based design for safety and security requirements. In: Koornnee, F., van Gulijk, C. (eds.) SAFECOMP 2015 Workshops. LNCS, vol. 9338, pp. 264–276. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24249-1_23 CrossRefGoogle Scholar
  4. 4.
    Fovino, I.N., Masera, M., Cian, A.D.: Integrating cyber attacks within fault trees. Reliab. Eng. Syst. Safety 94(9), 1394–1402 (2009)CrossRefGoogle Scholar
  5. 5.
    Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A.: Formal derivation of a distributed program in Event B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 420–436. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Kelly, T.P.: Arguing safety - a systematic approach to managing safety cases. Ph.D. thesis (1998)Google Scholar
  7. 7.
    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, Heidelberg (2014)Google Scholar
  8. 8.
    Rodin: Event-B platform.
  9. 9.
    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, Heidelberg (2014)Google Scholar
  10. 10.
    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 International Publishing Switzerland 2016

Authors and Affiliations

  • Elena Troubitsyna
    • 1
  • Linas Laibinis
    • 1
    Email author
  • Inna Pereverzeva
    • 1
  • Tuomas Kuismin
    • 2
  • Dubravka Ilic
    • 2
  • Timo Latvala
    • 2
  1. 1.Åbo Akademi UniversityTurkuFinland
  2. 2.Space Systems FinlandEspooFinland

Personalised recommendations