. Le-premier-poursuit-le-développement-du-système-de-platooning-jusqu-'au-niveau-d, une implantation qui pourra être exécutée dans des simulateurs virtuels puis des prototypes réels Le deuxième concerne le processus d'animation. Il faut implanter les règles de transformation des spécifications. L'élaboration et l'expression des scénarios reste une question ouverte. Le troisième axe concerne le problème des contraintes temporelles. A coté de l'emploi des techniques proposées par exemple par Rehm et Cansell, nous menons des investigations avec CSP||B, un formalisme qui combine deux méthodes formelles (Treharne et Schneider En usant des techniques présentées par Treharne nous développons un petit utilitaire pour assister les spécifieurs dans la preuve de cohérence de leur spécifications composites, 1999.

J. Abrial, The B Book, 1996.
DOI : 10.1017/CBO9780511624162

J. Abrial, Modeling in Event-B : System and Software Engineering, 2009.
DOI : 10.1017/CBO9781139195881

R. M. Balzer, N. M. Goldman, and D. S. Wile, Operational specification as the basis for rapid prototyping, ACM SIGSOFT Software Engineering Notes, vol.7, issue.5, pp.3-16, 1982.
DOI : 10.1145/1006258.1006261

J. Bendisposto, M. Leuschel, O. Ligot, and E. M. Samia, La validation de mod??les Event-B avec le plug-in ProB pour RODIN, Techniques et sciences informatiques, vol.27, issue.8, pp.1065-1084, 2008.
DOI : 10.3166/tsi.27.1065-1084

P. Daviet, M. Et, and . Parent, Longitudinal and lateral servoing of vehicles in a platoon, Proceedings of Conference on Intelligent Vehicles, pp.41-46, 1996.
DOI : 10.1109/IVS.1996.566349

E. W. Dijkstra, A Discipline of Programming, 1976.

J. Ferber, Multi-Agent Systems : An Introduction to Distributed Artificial Intelligence, 1999.

J. Ferber, J. P. Et, and . Muller, Influences and reaction : a model of situated multiagent systems, 2nd Int. Conf. on Multi-agent Systems, pp.72-79, 1996.

A. Lanoix, Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles, 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, pp.297-304, 2008.
DOI : 10.1109/TASE.2008.39
URL : https://hal.archives-ouvertes.fr/hal-00260577

M. Leuschel, L. Adhianto, M. Butler, C. Ferreira, and E. L. Mikhailov, Animation and model checking of CSP and B using prolog technology, Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001, pp.97-109, 2001.

A. Mashkoor, J. Jacquot, and E. J. Souquières, Transformation heuristics for formal requirements validation by animation, 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems -SafeCert 2009, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00374082

H. N. Nguyen, J. Et, and . Jacquot, A Tool for Checking CSP||B Specifications, Proc. Workshop on Tool Building in Formal Methods, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00463422

J. Rehm, Gestion du temps par le raffinement, 2009.
URL : https://hal.archives-ouvertes.fr/tel-00441312

J. Rehm, D. Et, and . Cansell, Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method, ISoLA, pp.179-190, 2007.
DOI : 10.1007/s10009-009-0130-5
URL : https://hal.archives-ouvertes.fr/hal-00184837

J. Rushby, Formal Methods and the Certificaiton of Critical Systems, 1993.

A. Scheuer, O. Simonin, and E. F. Charpillet, Safe longitudinal platoons of vehicles without communication, 2009 IEEE International Conference on Robotics and Automation, pp.2835-2840, 2009.
DOI : 10.1109/ROBOT.2009.5152629
URL : https://hal.archives-ouvertes.fr/inria-00342719

R. Schmid, J. Ryser, S. Berner, M. Glinz, R. Reutemann et al., A survey of simulation tools for requirements engineering, 2000.

J. I. Siddiqi, I. C. Morrey, C. R. Roast, and M. B. Ozcan, Towards quality requirements via animated formal specifications, Annals of Software Engineering, vol.3, pp.131-155, 1997.
DOI : 10.1023/A:1018977602872

O. Simonin, A. Lanoix, S. Colin, A. Scheuer, and E. F. Charpillet, Generic Expression in B of the Influence/Reaction Model : Specifying and Verifying Situated Multi-Agent Systems, INRIA Research Report, vol.6304, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00173876

H. Treharne, Combining Control Executives and Software Specifications, 2000.

H. Treharne, S. Et, and . Schneider, Using a Process Algebra to control B OPERATIONS, 1st International Conference on Integrated Formal Methods (IFM'99), pp.437-457, 1999.
DOI : 10.1007/978-1-4471-0851-1_23

H. T. Van, A. Van-lamsweerde, P. Massonet, and C. Ponsard, Goal-oriented requirements animation, RE '04 : Proceedings of the Requirements Engineering Conference, pp.218-228, 2004.