Abstract
In areas like manufacturing, communications, transportation or aerospace, the increasing size and complexity of reactive systems make their verification difficult to handle. Compositional reasoning is a way to master this problem. In this paper, we propose an approach based on a constraint synchronized product to specify and to verify such systems. This approach supports a compositional refinement for both labelled transition systems and their composition. In this framework, we show how to verify local and global invariance properties during a refinement verification. Thus, these properties are preserved through refinement.
The different aspects of our work are illustrated on the example of a communication protocol between an integrated chip card and a reader interface device.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996) ISBN 0521-496195
Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Alur, R., de Alfaro, L., Grosu, R., Henzinger, T.A., Kang, M., Majumdar, R., Mang, F., Kirsch, C.M., Wang, B.Y.: Mocha: A model checker that exploits design structure. In: 23rd International Conference on Software Engineering (ICSE 2001) (May 2001)
Andrade, H.A., Sanders, B.: An approach to compositional model checking. In: International Parallel and Distributed Processing Symposium (IPDPS 2002) Workshops: FMPPTA 2002, Fort Lauderdale, Florida, April 2002, IEEE, Los Alamitos (2002)
Arnold, A.: Systèmes de transitions finis et sémantique des processus communicants. Collection Etudes et Recherches en Informatiques. Masson, Paris (1992)
Arnold, A., Nivat, M.: Comportements de processus. In: Actes du Colloque AFCET - Les Mathématiques de l’Informatique, pp. 35–68 (1982)
Bellegarde, F., Darlot, C., Julliand, J., Kouchnarenko, O.: Reformulation: a way to combine dynamic properties and B refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 2–19. Springer, Heidelberg (2001)
Bellegarde, F., Julliand, J., Kouchnarenko, O.: Ready-simulation is not ready to express a modular refinement relation. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 266–283. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Cobleigh, J.-M., Giannakopoulou, D., Pasareanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Darlot, C., Julliand, J., Kouchnarenko, O.: Refinement preserves PLTL properties. In: Bert, D., Bowen, P., King, J. (eds.) ZB 2003. LNCS, vol. 2651, pp. 408–420. Springer, Heidelberg (2003)
European Normalisation Committee. En27816-3. European standard - identification cards - integrated circuit(s) card with contacts - electronic signal and transmission protocols. Technical Report ISO/CEI 7816-3 (1992)
Kouchnarenko, O., Lanoix, A.: Refinement and verification of synchronized component-based systems. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 341–358. Springer, Heidelberg (2003)
Kouchnarenko, O., Lanoix, A.: Refinement and verification of synchronized component-based systems. INRIA Research Report 4862 (June 2003)
Kouchnarenko, O., Lanoix, A.: SynCo: a refinement analysis tool for synchronized component-based systems. In: Margaria, T. (ed.) FM 2003 Tool Exhibition Notes, Pisa, Italy, September 2003, pp. 47–51 (2003)
Lind-Nielsen, J., Andersen, H.R., Hulgaard, H., Behrmann, G., Kristoffersen, K., Larsen, K.G.: Verification of large state/event systems using compositionality and dependency analysis. Formal Methods in System Design 18(1), 5–23 (2001)
Masson, P.-A., Mountassir, H., Julliand, J.: Modular verification for a class of PLTL properties. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 398–419. Springer, Heidelberg (2000)
McMillan, K.L.: A methodology for hardware verification using compositional model-checking. Science of Computer Programming 37, 279–309 (2000)
Tsay, Y.-K.: Compositional verification in linear-time temporal logic. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 344–358. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kouchnarenko, O., Lanoix, A. (2004). Verifying Invariants of Component-Based Systems through Refinement. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-27815-3_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22381-8
Online ISBN: 978-3-540-27815-3
eBook Packages: Springer Book Archive