[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Modeling of a speed control system using Event-B

  • General
  • Special Section: ABZ 2020/2021
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

This paper presents an Event-B model of a speed control system, a part of the case study provided in the ABZ2020 conference. The case study describes how the system regulates the current speed of a car according to a set of criteria like the driver’s desired speed, the position of a possible preceding vehicle, but also a given speed limit that the driver must not exceed. For that purpose, this controller reads different information from the available sensors (key state, desired speed) and takes adequate actions by acting on the actuators of the car’s speed according to the information read. To formally model this system, we adopt a stepwise refinement approach with the Event-B method. We consider most of the features of the case study. All proof obligations of the invariant properties have been discharged using the Rodin provers. Our model has been validated using ProB by applying the different provided scenarios. This validation has permitted us to point out and correct some mistakes, ambiguities and oversights contained in the first versions of the case study.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abrial, J.R.: The B-book – Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  Google Scholar 

  2. Abrial, J.R.: Modeling in Event-B – System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  3. 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. Transf. 12(6), 447–466 (2010)

    Article  Google Scholar 

  4. Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Modelling an automotive software-intensive system with adaptive features using ASMETA. In: Rigorous State-Based Methods – 7th International Conference ABZ. Lecture Notes in Computer Science, vol. 12071, pp. 302–317. Springer, Berlin (2020)

    Chapter  Google Scholar 

  5. Bendisposto, J., Geleßus, D., Jansing, Y., Leuschel, M., Pütz, A., Vu, F., Werth, M.: ProB 2-UI: a Java-based user interface for ProB. In: Proceedings FMICS (International Conference on Formal Methods for Industrial Critical Systems). Lecture Notes in Computer Science, vol. 12863, pp. 193–201. Springer, Berlin (2021)

    Chapter  Google Scholar 

  6. Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Berlin (2003)

    Google Scholar 

  7. Butler, M., Maamria, I.: Practical Theory Extension in Event-B. In: Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pp. 67–81. Springer, Berlin (2013)

    Chapter  Google Scholar 

  8. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: 25 Years of Model Checking – History, Achievements, Perspectives. Lecture Notes in Computer Science, vol. 5000, pp. 196–215. Springer, Berlin (2008)

    Chapter  Google Scholar 

  9. Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference TACAS. Lecture Notes in Computer Science, vol. 2988, pp. 168–176. Springer, Berlin (2004)

    Google Scholar 

  10. Clearsy. https://www.atelierb.eu/en/presentation-of-the-b-method/formal-proof-presentation/

  11. Event-B Consortium. http://www.event-b.org/

  12. Event-B Consortium: SMT Solvers Plug-in. https://wiki.event-b.org/index.php/SMT_Solvers_Plug-in

  13. Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid ERTMS/ETCS level 3 standard using a formal requirements engineering approach. Int. J. Softw. Tools Technol. Transf. 22(3), 349–363 (2020)

    Article  Google Scholar 

  14. Hoang, T.S., Dghaym, D., Snook, C., Butler, M.: A composition mechanism for refinement-based methods. In: 22nd International Conference on Engineering of Complex Computer Systems ICECCS, pp. 100–109. IEEE Comput. Soc., Los Alamitos (2017)

    Google Scholar 

  15. Hoang, T.S., Butler, M., Reichl, K.: The hybrid ERTMS/ETCS level 3 case study. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z. Lecture Notes in Computer Science, pp. 251–261. Springer, Berlin (2018)

    Chapter  Google Scholar 

  16. Houdek, F., Raschke, A.: Adaptive Exterior Light and Speed Control System (2019). https://abz2020.uni-ulm.de/case-study#Specification-Document

  17. Krings, S., Körner, P., Dunkelau, J., Rutenkolk, C.: A verified low-level implementation of the adaptive exterior light and speed control system. In: Rigorous State-Based Methods – 7th International Conference ABZ. Lecture Notes in Computer Science, vol. 12071, pp. 382–397. Springer, Berlin (2020)

    Chapter  Google Scholar 

  18. Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)

    Article  Google Scholar 

  19. Leuschel, M., Bendisposto, J., Dobrikov, I., Krings, S., Plagge, D.: From animation to data validation: the ProB constraint solver 10 years on. In: Formal Methods Applied to Complex Systems: Implementation of the B Method, pp. 427–446. Wiley, New York (2014). Chap. 14

    Chapter  Google Scholar 

  20. Mammar, A., Frappier, M.: Modeling of a speed control system using Event-B. In: Rigorous State-Based Methods – 7th International Conference ABZ. Lecture Notes in Computer Science, vol. 12071, pp. 367–381. Springer, Berlin (2020)

    Chapter  Google Scholar 

  21. Mammar, A., Frappier, M.: An Event-B model of a speed control system (2023). Available at https://github.com/AmelMammar/SpeedControlSystem

  22. Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. In: ABZ 2014: The Landing Gear Case Study – Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z. Communications in Computer and Information Science, vol. 433, pp. 80–94. Springer, Berlin (2014)

    Google Scholar 

  23. Mammar, A., Laleau, R.: Modeling a landing gear system in Event-B. Int. J. Softw. Tools Technol. Transf. 19(2), 167–186 (2017)

    Article  Google Scholar 

  24. Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: An Event-B model of the hybrid ERTMS/ETCS level 3 standard. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z – 6th International Conference ABZ. Lecture Notes in Computer Science, vol. 10817, pp. 353–366. Springer, Berlin (2018)

    Google Scholar 

  25. Mammar, A., Frappier, M., Fotso, S.J.T., Laleau, R.: A formal refinement-based analysis of the hybrid ERTMS/ETCS level 3 standard. Int. J. Softw. Tools Technol. Transf. 22(3), 333–347 (2020)

    Article  Google Scholar 

  26. Mammar, A., Frappier, M., Laleau, R.: An Event-B model of an automotive adaptive exterior light system. In: Rigorous State-Based Methods – 7th International Conference ABZ. Lecture Notes in Computer Science, vol. 12071, pp. 351–366. Springer, Berlin (2020)

    Chapter  Google Scholar 

  27. Nakahori, K., Yamaguchi, S.: A support tool to design IoT services with NuSMV. In: IEEE International Conference on Consumer Electronics, (ICCE), pp. 80–83. IEEE (2017)

    Google Scholar 

  28. Parnas, D.L., Madey, J.: Functional documents for computer systems. Sci. Comput. Program. 25(1), 41–61 (1995)

    Article  Google Scholar 

  29. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE Computer Society, Providence (1977)

    Google Scholar 

  30. ProB: https://prob.hhu.de/

  31. Snook, C.: http://wiki.event-b.org/index.php/Event-B_Statemachines

  32. Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)

    Article  Google Scholar 

  33. Werth, M., Leuschel, M.: VisB: a lightweight tool to visualize formal models with SVG graphics. In: Raschke, A., Méry, D., Houdek, F. (eds.) Proceedings ABZ 2020. Lecture Notes in Computer Science, pp. 260–265. Springer, Berlin (2020)

    Google Scholar 

Download references

Acknowledgements

The authors would like to thank the case study authors, and Frank Houdek in particular, for his responsiveness and useful feedback during the modeling process when questions were raised or when ambiguities were found. The authors would also like to thank Michael Leuschel for his quick feedback on using ProB for this large case study. Since the first version of the paper, the very valuable reviewers’ comments have helped us improve the quality of the paper. We would like to sincerely thank them.

Funding

This work was supported in part by the DISCONT ANR French project and NSERC (Natural Sciences and Engineering Research Council of Canada).

Author information

Authors and Affiliations

  1. SAMOVAR, Institut Polytechnique de Paris, Télécom SudParis, Palaiseau, France

    Amel Mammar

  2. GRIC, Département d’informatique, Faculté des sciences, Université de Sherbrooke, Québec, Canada

    Marc Frappier

Authors
  1. Amel Mammar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marc Frappier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Amel Mammar.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Mammar, A., Frappier, M. Modeling of a speed control system using Event-B. Int J Softw Tools Technol Transfer 26, 347–363 (2024). https://doi.org/10.1007/s10009-024-00749-y

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-024-00749-y

Keywords

Search

Navigation