Abstract
This paper presents an experience report on the specification and the validation of a real case study in the context of the industrial CRISTAL project. The case study concerns a platoon of a new type of urban vehicles with new functionalities and services. It is specified using the combination, named CSP||B, of two well-known formal methods, and validated using the corresponding support tools. This large – both distributed and embedded – system typically corresponds to a multi-level composition of components that have to cooperate. We identify some lessons learned, showing how to develop and verify the specification and check some properties in a compositional way using theoretical results and support tools to validate this complex system.
This work has been partially supported by the French National Research Agency TACOS project, ANR-06-SETI-017 (http://tacos.loria.fr) and by the pôle de compétitivité Alsace/Franche-Comté 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
References
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)
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)
Schneider, S.A., Treharne, H.E.: CSP theorems for communicating B machines. In: Formal Aspects of Computing, Special issue of IFM 2004 (2005)
Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
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 (2007)
Colin, S., Lanoix, A., Kouchnarenko, O., Souquières, J.: Towards Validating a Platoon of Cristal Vehicles using CSP||B. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 139–144. Springer, Heidelberg (2008)
Lanoix, A., Hatebur, D., Heisel, M., Souquières, J.: Enhancing dependability of component-based systems. In: Abdennahder, N., Kordon, F. (eds.) Ada-Europe 2007. LNCS, vol. 4498, pp. 41–54. Springer, Heidelberg (2007)
Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334–354. Springer, Heidelberg (2005)
Roscoe, A.W.: The theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)
Treharne, H., Schneider, S.: Using a Process Algebra to Control B OPERATIONS. In: 1st International Conference on Integrated Formal Methods (IFM 1999), pp. 437–457. Springer, New York (1999)
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)
Evans, N., Treharne, H.E.: Investigating a file transfer protocol using CSP and B. Software and Systems Modelling Journal 4, 258–276 (2005)
Schneider, S., Cavalcanti, A., Treharne, H., Woodcock, J.: A layered behavioural model of platelets. In: 11th IEEE International Conference on Engieerging of Complex Computer Systems, ICECCS (2006)
Carcenac, F., Boniol, F.: A formal framework for verifying distributed embedded systems based on abstraction methods. Int. J. Softw. Tools Technol. Transf. 8(6), 471–484 (2006)
Bontron, P., Potet, M.-L.: Automatic Construction of Validated B Components from Structured Developments. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 127–147. Springer, Heidelberg (2000)
Abrial, J.R.: Discrete System Models, Version 1.1 (2002)
Attiogbé, C.: Communicating B Abstract Systems, Research Report RR-IRIN 02.08 (2002) (updated July 2003)
Bellegarde, F., Julliand, J., Kouchnarenko, O.: Synchronized parallel composition of event systems in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 436–457. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colin, S., Lanoix, A., Kouchnarenko, O., Souquières, J. (2009). Using CSP||B Components: Application to a Platoon of Vehicles. In: Cofer, D., Fantechi, A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2008. Lecture Notes in Computer Science, vol 5596. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03240-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-03240-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03239-4
Online ISBN: 978-3-642-03240-0
eBook Packages: Computer ScienceComputer Science (R0)