Abstract
Modern automotive systems with adaptive control features require rigorous analysis to guarantee correct operation. We report our experience in modeling the automotive case study from the ABZ2020 conference using the ASMETA toolset, based on the Abstract State Machine formal method. We adopted a seamless system engineering method: from an incremental formal specification of high-level requirements to increasingly refined ASMETA models, to the C++ code generation from the model. Along this process, different validation and verification activities were performed. We explored modeling styles and idioms to face the modeling complexity and ensure that the ASMETA models can best capture and reflect specific behavioral patterns. Through this realistic automotive case study, we evaluated the applicability and usability of our formal modeling approach.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Proc. Of the Second International Conference on Abstract State Machines, Alloy, B and Z, ABZ’10, pp. 61–74. Springer, Berlin (2010). https://doi.org/10.1007/978-3-642-11811-1_6
Arcaini, P., Gargantini, A., Riccobene, E.: Automatic review of abstract state machines by meta property verification. In: Muñoz, C. (ed.) Proc. Of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, pp. 4–13, NASA, Langley Research Center, Hampton (2010)
Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Exp. 41, 155–166 (2011). https://doi.org/10.1002/spe.1019
Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2015, pp. 80–89. IEEE, Los Alamitos (2015). https://doi.org/10.1109/MEMCOD.2015.7340473
Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from ASM models to Java code. Int. J. Softw. Tools Technol. Transf. 19(2), 247–269 (2015). https://doi.org/10.1007/s10009-015-0394-x
Arcaini, P., Bonfanti, S., Dausend, M., Gargantini, A., Mashkoor, A., Raschke, A., Riccobene, E., Scandurra, P., Stegmaier, M.: Unified syntax for abstract state machines. In: Butler, M., Schewe, K.D., Mashkoor, A., Biro, M. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23–27, 2016. Proceedings, vol. 9675, pp. 231–236. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_14
Arcaini, P., Gargantini, A., Riccobene, E.: SMT-based automatic proof of ASM model refinement. In: De Nicola, R., Kühn, E. (eds.) Software Engineering and Formal Methods, pp. 253–269. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_17
Arcaini, P., Holom, R.M., Riccobene, E.: ASM-based formal design of an adaptivity component for a cloud system. Form. Asp. Comput. 28(4), 567–595 (2016). https://doi.org/10.1007/s00165-016-0371-5
Arcaini, P., Riccobene, E., Scandurra, P.: Formal design and verification of self-adaptive systems with decentralized control. ACM Trans. Auton. Adapt. Syst. 11(4), 25:1–25:35 (2017). https://doi.org/10.1145/3019598
Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Integrating formal methods into medical software development: the ASM approach. Sci. Comput. Program. 158, 148–167 (2018). https://doi.org/10.1016/j.scico.2017.07.003
Arcaini, P., Melioli, R., Riccobene, E.: AsmetaF: a flattener for the ASMETA framework. In: Masci, P., Monahan, R., Prevosto, V. (eds.) Proc. 4th Workshop on Formal Integrated Development Environment, Oxford, England, 14 July 2018, Electronic Proceedings in Theoretical Computer Science, vol. 284, pp. 26–36. Open Publishing Association (2018). https://doi.org/10.4204/EPTCS.284.3
Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Addressing usability in a formal development environment. In: Sekerinski, E., Moreira, N., Oliveira, J.N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P., Delmas, D. (eds.) Formal Methods. FM 2019 International Workshops, pp. 61–76. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54994-7_6
Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Modelling an automotive software-intensive system with adaptive features using ASMETA. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 302–317. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_25
Arcaini, P., Mirandola, R., Riccobene, E., Scandurra, P.: MSL: a pattern language for engineering self-adaptive systems. J. Syst. Softw. 164, 110558 (2020). https://doi.org/10.1016/j.jss.2020.110558
Arcaini, P., Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: The ASMETA approach to safety assurance of software systems. In: Raschke, A., Riccobene, E., Schewe, K.D. (eds.) Logic, Computation and Rigorous Methods: Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday, pp. 215–238. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76020-5_13
Banach, R., Zhu, H., Su, W., Wu, X.: Asm, controller synthesis, and complete refinement. Sci. Comput. Program. 94, 109–129 (2014). https://doi.org/10.1016/j.scico.2014.04.013
Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms. ACM Trans. Comput. Log. 4, 578–651 (2003). https://doi.org/10.1145/937555.937561
Bombarda, A., Bonfanti, S., Gargantini, A.: Developing medical devices from abstract state machines to embedded systems: a smart pill box case study. In: Mazzara, M., Bruel, J.M., Meyer, B., Petrenko, A. (eds.) Software Technology: Methods and Tools, pp. 89–103. Springer, Cham (2019)
Bombarda, A., Bonfanti, S., Gargantini, A., Radavelli, M., Duan, F., Lei, Y.: Combining model refinement and test generation for conformance testing of the IEEE PHD protocol using abstract state machines. In: Gaston, C., Kosmatov, N., Le Gall, P. (eds.) Testing Software and Systems, pp. 67–85. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31280-0_5
Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E.: Developing a prototype of a mechanical ventilator controller from requirements to code with ASMETA. In: Gleirscher, M., van de Pol, J., Woodcock, J. (eds.) Proc. First Workshop on Applicable Formal Methods, AppFM@FM 2021, Virtual, 23rd November 2021, EPTCS, vol. 349, pp. 13–29 (2021). https://doi.org/10.4204/EPTCS.349.2
Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E.: Extending ASMETA with time features. In: Raschke, A., Méry, D. (eds.) Rigorous State-Based Methods, pp. 105–111. Springer, Cham (2021)
Bonfanti, S., Gargantini, A., Mashkoor, A.: AsmetaA: animator for abstract state machines. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 369–373. Springer, Cham (2018)
Bonfanti, S., Gargantini, A., Mashkoor, A.: Design and validation of a C++ code generator from abstract state machines specifications. J. Softw. Evol. Process 32(2), e2205 (2020). https://doi.org/10.1002/smr.2205
Bonfanti, S., Riccobene, E., Scandurra, P.: A runtime safety enforcement approach by monitoring and adaptation. In: Biffl, S., Navarro, E., Löwe, W., Sirjani, M., Mirandola, R., Weyns, D. (eds.) Software Architecture, pp. 20–36. Springer, Cham (2021)
Börger, E.: The ASM refinement method. Form. Asp. Comput. 15, 237–257 (2003)
Börger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Berlin (2018). https://doi.org/10.1007/978-3-662-56641-1
Börger, E., Schewe, K.: Concurrent abstract state machines. Acta Inform. 53(5), 469–492 (2016). https://doi.org/10.1007/s00236-015-0249-7
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin (2003)
Cunha, A., Macedo, N., Liu, C.: Validating multiple variants of an automotive light system with electrum. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 318–334. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_26
Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: an extensible ASM execution engine. Fundam. Inform. 77(1–2), 71–103 (2007)
Gaspari, P., Riccobene, E., Gargantini, A.: A formal design of the hybrid European rail traffic management system. In: Proc. Of the 13th European Conference on Software Architecture, ECSA’19, vol. 2, pp. 156–162. Assoc. Comput. Mach., New York (2019). https://doi.org/10.1145/3344948.3344993
Houdek, F., Raschke, A.: Adaptive exterior light and speed control system. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 281–301. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_24
Kephart, J.O., Chess, D.M.: The vision of autonomic computing. Computer 36(1), 41–50 (2003). https://doi.org/10.1109/MC.2003.1160055
Krings, S., Körner, P., Dunkelau, J., Rutenkolk, C.: A verified low-level implementation of the adaptive exterior light and speed control system. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 382–397. Springer, Cham (2020)
Leuschel, M., Mutz, M., Werth, M.: Modelling and validating an automotive system in classical B and Event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 335–350. Springer, Cham (2020)
Lezuo, R., Paulweber, P., Krall, A.: CASM – optimized compilation of abstract state machines. In: ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2014, pp. 13–22. ACM, New York (2014)
Mammar, A., Frappier, M.: Modeling of a speed control system using Event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 367–381. Springer, Cham (2020)
Mammar, A., Frappier, M., Laleau, R.: An Event-B model of an automotive adaptive exterior light system. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp. 351–366. Springer, Cham (2020)
Mirandola, R., Potena, P., Riccobene, E., Scandurra, P.: A reliability model for service component architectures. J. Syst. Softw. 89, 109–127 (2014). https://doi.org/10.1016/j.jss.2013.11.002
Riccobene, E., Scandurra, P.: Towards ASM-based formal specification of self-adaptive systems. In: Ait Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 204–209. Springer, Berlin (2014)
Schmid, J.: Compiling abstract state machines to C++. In: Moreno-Dìaz, R., Quesanda-Arencibia, A. (eds.) Formal Methods and Tools for Computer Science, Eurocast (2001). Universidad de Las Palmas de Gran Canaria. Extended Abstract
Sommerville, I.: Software Engineering, 9th edn. Addison-Wesley, Reading (2010)
Acknowledgements
We thank the student Giorgio Brugali who performed the translation from the ASMETA models to Arduino code and realized the Arduino implementation.
Funding
Open access funding provided by Università degli studi di Bergamo within the CRUI-CARE Agreement. P. Arcaini is supported by MIRAI Engineerable AI Project (No. JPMJMI20B8), JST; and ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST, Funding Reference number: 10.13039/501100009024 ERATO.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Arcaini, P., Bonfanti, S., Gargantini, A. et al. A journey with ASMETA from requirements to code: application to an automotive system with adaptive features. Int J Softw Tools Technol Transfer 26, 379–401 (2024). https://doi.org/10.1007/s10009-024-00751-4
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-024-00751-4