Abstract
Our lives become increasingly dependent on safety- and security-critical systems, so formal techniques are advocated for engineering such systems. One of such techniques is validation obligations that enable formalizing requirements early in development to ensure their correctness. Furthermore, validation obligations help hold requirements consistent in an evolving model and create assurances about the model’s completeness. Although initially proposed for safety properties, this paper shows how the technique of validation obligations enables us to also reason about security concerns through an example from the medical domain.
The research presented in this paper has been conducted within the IVOIRE project, which is funded by “Deutsche Forschungsgemeinschaft” (DFG) and the Austrian Science Fund (FWF) grant # I 4744-N. The work of Sebastian Stock and Atif Mashkoor has been partly funded by the LIT Secure and Correct Systems Lab sponsored by the province of Upper Austria.
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.
\(e(\texttt {startSystem})\) means that this event is enabled because its guard is true.
- 2.
We omitted parts of the graphic for space reasons.
References
Abrial, J.R.: Modeling in Event-B: system and software engineering. Cambridge University Press (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)
Biró, M., Mashkoor, A., Sametinger, J., Seker, R.: Software safety and security risk mitigation in cyber-physical systems. IEEE Softw. 35(1), 24–29 (2018)
Copper, D., Barnes, J.: Tokeneer id station eal5 demonstrator: Summary report. Tech. Rep., Augugst, Altran Praxis Limited (2008)
Cristiá, M., Rossi, G.: An automatically verified prototype of the tokeneer id station specification. J. Autom. Reason. 65(8), 1125–1151 (2021)
Fitzgerald, J.S., Tjell, S., Larsen, P.G., Verhoef, M.: Validation support for distributed real-time embedded systems in vdm++. In: 10th IEEE High Assurance Systems Engineering Symposium (HASE 2007). pp. 331–340. IEEE (2007)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_46
Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329–343. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_29
Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exp. 48(12), 2350–2379 (2018)
Mashkoor, A., Leuschel, M., Egyed, A.: Validation obligations: a novel approach to check compliance between requirements and their formal specification. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pp. 1–5. IEEE (2021)
Mashkoor, A., Sametinger, J., Biro, M., Egyed, A.: Security- and safety-critical cyber-physical systems. J. Soft. Evol. Process 32(2), e2239 (2020)
(NSA): The tokeneer case study. https://www.adacore.com/tokeneer, (Accessed 19 July 2022, 14:12:17)
Rivera, V., Bhattacharya, S., Cataño, N.: Undertaking the tokeneer challenge in event-b. In: Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, pp. 8–14 (2016)
Schneier, B.: Attack trees. Dr. Dobb’s J. 24(12), 21–29 (1999)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Stock, S., Mashkoor, A., Egyed, A. (2022). Application of Validation Obligations to Security Concerns. In: Kotsis, G., et al. Database and Expert Systems Applications - DEXA 2022 Workshops. DEXA 2022. Communications in Computer and Information Science, vol 1633. Springer, Cham. https://doi.org/10.1007/978-3-031-14343-4_31
Download citation
DOI: https://doi.org/10.1007/978-3-031-14343-4_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-14342-7
Online ISBN: 978-3-031-14343-4
eBook Packages: Computer ScienceComputer Science (R0)