Abstract
Ability to scale up from toy examples to real life problems is a crucial issue for formal methods. Formalizing a algorithm used in vehicle automation (platooning control) in a certification perspective, we had the opportunity to study the scaling up when going from a (toy) model in 1D to a (more realistic) model in 2D. The formalism, Event-B, belongs to the family of mathematical state based methods. Increase was quantitative: 3 times more events and 4 times more proofs; and qualitative: trigonometric functions and integrals are used. Edition and verification of the specification scale up well. The crucial part of the work was the adaptation of the mathematical and physical model through standard heuristics. The validation of temporal properties and behaviors do not scale up so well. Analysis of the difficulties suggests improvements in both tool support and formalism.
Work partially supported by ANR under project ANR-06-SETI-017 TACOS (http://tacos.loria.fr), and by Pôle de Compétitivité Alsace/Franche-Comté under CRISTAL project (http://www.projet-cristal.net).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Balzer, R.M., Goldman, N.M., Wile, D.S.: Operational specification as the basis for rapid prototyping. SIGSOFT Softw. Eng. Notes 7(5), 3–16 (1982)
Bendisposto, J., Leuschel, M., Ligot, O., Samia, M.: La validation de modèles Event-B avec le plug-in ProB pour RODIN. Technique et Science Informatiques 27(8), 1065–1084 (2008)
Bendisposto, J., Fritz, F., Leuschel, M.: Developing Camille, a Text Editor for Rodin. In: Proc. Workshop on Tool Building in Formal Methods. colocated with ABZ Conference, Orford, Canada (2010)
Colin, S., Lanoix, A., Kouchnarenko, O., Souquières, J.: Using CSP||B Components: Application to a Platoon of Vehicles. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 103–118. Springer, Heidelberg (2009)
Daviet, P., Parent, M.: Longitudinal and Lateral Servoing of Vehicles in a Platoon. In: Proceeding of the IEEE Intelligent Vehicles Symposium, pp. 41–46 (1996)
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)
Ferber, J.: Multi-Agent Systems: An Introduction to Distributed Artificial Intelligence. Addison-Wesley Professional, Reading (1999)
Ferber, J., Muller, J.P.: Influences and Reaction: a Model of Situated Multiagent Systems. In: 2nd Int. Conf. on Multi-agent Systems, pp. 72–79 (1996)
Lamport, L.: Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Lanoix, A.: Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles. In: 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 297–304. IEEE Computer Society, Los Alamitos (2008)
Leuschel, M., Adhianto, L., Butler, M., Ferreira, C., Mikhailov, L.: Animation and Model Checking of CSP and B using Prolog Technology. In: Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL 2001, pp. 97–109 (2001)
Leuschel, M., Butler, M.: ProB: An Automated Analysis Toolset for the B Method. STTT 10(2), 185–203 (2008)
Mashkoor, A., Jacquot, J.P.: Domain Engineering with Event-B: Some Lessons We Learned. In: 18th International Requirements Engineering Conference - RE 2010, pp. 252–261. IEEE, Sydney (2010)
Mashkoor, A., Jacquot, J.P., Souquières, J.: B événementiel pour la modélisation du domaine: application au transport. In: Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2009), France, Toulouse, p. 19 (2009), http://hal.inria.fr/inria-00326355/en/
Mashkoor, A., Jacquot, J.P., Souquières, J.: Transformation Heuristics for Formal Requirements Validation by Animation. In: 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems - SafeCert 2009, Royaume-Uni York (2009), http://hal.inria.fr/inria-00374082/en/
Metayer, C., Voisin, L.: The Event-B Mathematical Language (October 2007)
Nguyen, H.N., Jacquot, J.P.: A Tool for Checking CSP||B Specifications. In: Proc. Workshop on Tool Building in Formal Methods. colocated with ABZ Conference, Orford, Canada (2010)
RODIN: Rigorous Open Development Environment for Complex Systems. website (August 2007), http://rodin-b-sharp.sourceforge.net
Schmid, R., Ryser, J., Berner, S., Glinz, M., Reutemann, R., Fahr, E.: A Survey of Simulation Tools for Requirements Engineering. Tech. Rep. 2000.06, University of Zurich (2000)
Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 416–435. Springer, Heidelberg (2002)
Siddiqi, J.I., Morrey, I.C., Roast, C.R., Ozcan, M.B.: Towards quality requirements via animated formal specifications. Ann. Softw. Eng. 3, 131–155 (1997)
Simonin, O., Lanoix, A., Colin, S., Scheuer, A., Charpillet, F.: Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems. INRIA Research Report 6304, INRIA (September 2007), http://hal.inria.fr/inria-00173876/en/
Treharne, H.: Combining Control Executives and Software Specifications. Ph.D. thesis, University of London (2000)
Van, H.T., van Lamsweerde, A., Massonet, P., Ponsard, C.: Goal-Oriented Requirements Animation. In: RE ’04: Proceedings of the Requirements Engineering Conference, 12th IEEE International. pp. 218–228. IEEE Computer Society, Washington, DC, USA (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, F., Jacquot, JP. (2011). Scaling Up with Event-B: A Case Study. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)