Abstract
This paper presents insights gained during modeling and analyzing the arrival manager (AMAN) case study in Event-B with validation obligations (VOs). AMAN is a safety-critical interactive system for air traffic controllers to organize the landing of airplanes at airports. The presented model consists of a human-machine interface comprising interactive and autonomous parts. We employ VOs to formalize requirements, uncover contradictions and ambiguities, and validate the model’s compliance with the requirements. To capture the AMAN’s human-machine interaction, we implement an interactive domain-specific visualization and an automatic simulation using the VisB and SimB components of ProB.
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.
The model and all other mentioned files are available at https://github.com/hhu-stups/AMAN-case-study/tree/bd044670a02092643230d6001cc2b355a2dc350a.
- 2.
Note that even on infinite state spaces, model checking can be useful in detecting errors. We did apply ProB also to the un-instantiated models.
- 3.
Note that deadlock-freedom is only verified by model checking.
- 4.
Revision f41dfd4b29c7bd95583dffcb0adad44171f4f0c0 from 2023-01-10.
- 5.
Our visualization shows the minutes relative to the current time, while the specification document shows the current minute in the current hour on the clock. Assuming that the current time is 9:03, then our visualization displays 9:05 as 2, while Fig. 6 in [9] would display 9:05 as 5.
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (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)
Aït-Ameur, Y., Aït-Sadoune, I., Baron, M., Mota, J.M.: Vérification et validation formelles de systèmes interactifs fondées sur la preuve : application aux systèmes Multi-Modaux. Journal d’Interaction Personne-Système 1 (2014). https://doi.org/10.46298/jips.59, https://jips.episciences.org/59
Bendisposto, J., et al.: ProB2-UI: a java-based user interface for ProB. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 193–201. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-85248-1_12
Borrione, D., Paul, W. (eds.): LNCS, vol. 3725. Springer, Heidelberg (2005). https://doi.org/10.1007/11560548
Leuschel, M.: Operation caching and state compression for model checking of high-level models - how to have your cake and eat it. In: ter Beek, M.H., Monahan, R. (eds.) Integrated Formal Methods, Proceedings IFM 2022, LNCS, vol. 13274, pp. 129–145 (2022). https://doi.org/10.1007/978-3-031-07727-2_8
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)
Mashkoor, A., Leuschel, M., Egyed, A.: Validation obligations: a novel approach to check compliance between requirements and their formal specification. In: ICSE’21 NIER, pp. 1–5 (2021)
Palanque, P., Campos, J.C.: AMAN case study. https://drive.google.com/file/d/1IqftxQIvrWpX1lcRts3WJzrBH7a3dMln/view
Rehm, J., Cansell, D.: Proved development of the real-time properties of the IEEE 1394 root contention protocol with the Event B method. In: Proceedings ISoLA, pp. 179–190 (2007)
Singh, N.K., Aït-Ameur, Y., Geniet, R., Méry, D., Palanque, P.: On the benefits of using MVC pattern for structuring Event-B models of WIMP interactive applications. Interact. Comput. 33(1), 92–114 (2021). https://doi.org/10.1093/iwcomp/iwab016
Stock, S., Mashkoor, A., Leuschel, M., Egyed, A.: Trace refinement in B and Event-B. In: Riesco, A., Zhang, M. (eds.) Formal Methods and Software Engineering, Proceedings ICFEM, LNCS, vol. 13478, pp. 316–333. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17244-1_19
Stock, S., Vu, F., Geleßus, D., Leuschel, M., Mashkoor, A., Egyed, A.: Validation by abstraction and refinement. In: Proceedings ABZ (2023)
Stock, S., Vu, F., Mashkoor, A., Leuschel, M., Egyed, A.: IVOIRE Deliverable 1.1: Classification of existing VOs & tools and Formalization of VOs semantics. CoRR abs/2205.06138 (2022). https://doi.org/10.48550/arXiv.2205.06138
Vu, F., Leuschel, M., Mashkoor, A.: Validation of formal models by timed probabilistic simulation. In: Raschke, A., Méry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 81–96. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-77543-8_6
Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 260–265. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_21
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Geleßus, D., Stock, S., Vu, F., Leuschel, M., Mashkoor, A. (2023). Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. In: Glässer, U., Creissac Campos, J., Méry, D., Palanque, P. (eds) Rigorous State-Based Methods. ABZ 2023. Lecture Notes in Computer Science, vol 14010. Springer, Cham. https://doi.org/10.1007/978-3-031-33163-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-031-33163-3_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-33162-6
Online ISBN: 978-3-031-33163-3
eBook Packages: Computer ScienceComputer Science (R0)