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).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
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)