Abstract
Reachability analysis has been one of the most successful methods for automated analysis of concurrent and reactive systems. It is based on an exhaustive enumeration of states and implemented in several tools of verification. However, the major problem in applying this technique is the potential combinatorial explosion of the states space. To deal with this problem, various reduction and symbolic techniques have been developed. In this paper, we first present an extension of the B language in order to express dynamic properties using logic formulas in LTL. After this, we introduce an approach of verification performed on modules obtained by refinement rather than on the full specification. The number of states on which the verification is performed is then grandly reduced. Some patterns of properties are discussed and verified using the model-checking on each module. To illustrate the idea we give the known BRP example (Bounded Retransmission Protocol) described with B. We then show that under some considerations we are able to decide whether a given property is false or true, or should have been established at a higher level of abstraction.
This is a preview of subscription content, log in via an institution to check access.
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
R. Milner, Communication and concurrency, Prentice-hall series in computer sciences, C.A.R. Hoare editor, 1989.
A. Arnold, Systèmes de transitions finis et sémantique des processus communicants, Masson, 1992.
A. Arnold, S.Brlek, Automatic Verification of Properties in Transition Systems, Software-Practice and Experience, vol n° 25, n° 6, pp. 579–596, 1995.
Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: specification, Springer Verlag, ISBN 0–387-97664–7, 1992.
Z. Manna, A. Pnueli, Temporal verification of reactive systems, Springer Verlag - ISBN 0–387-94459–1, 1995.
L. Lamport, The temporal logic of actions, Technical report, Digital Systems Research center, Palo Alto, California, Dec. 1991.
J.R. Abrial, The B Book, Cambridge University Press, - ISBN 0521–496195, 1996.
J.R. Abrial, Extending B without Changing it (for Developing Distributed Systems), 1st Conference on the B method, pp. 169–190, Nantes, November 1996.
J.R. Abrial, L. Mussat, Introducing dynamic constraints in B, 2nd Conference on the B method, Montpellier, LNCS n°1393, pp. 83–128, April 1998.
G.J. Holzmann, Design and validation of protocols, Prentice hall software series, 1991.
G.J. Holzmann, The model-checker SPIN, IEEE Trans. On Software Engineering, Vol. 23, n° 5, 1996.
G J. Holzmann, Basic Spin manual, Bell laboratories- Murray hill, NJ 07974.
G.J. Holzmann, Overview of the Spin model-checker, Technical Report, Computing Principles Research Department, Bell Laboratories.
J.R. Burch, E.M. Clarke, K.L. Mc Millan, D.L.Dill and L.J. Hwang, Symbolic model checking: 1020 states and beyond, Logic in Computer Science, 1990.
J. Julliand, B. Legeard, T. Machicoane, B. Parreaux, B. Tatibouet, Specification of an integrated circuits card protocol application using B and Linear Temporal Logic, 2nd Conference on the B method, LNCS n°1393, pp. 273–292, Montpellier, April 1998.
Comité européen de normalisation, “Norme Européenne-Carte d’identification- cartes à circuits intégrés à contacts-Patis 3: Signaux électriques et protocoles de transmission”, ISO/CEI 78–2:1989, Avril 1992.
J.R. Abrial, Steam-boiler control specification problem, Formal methods for industrial applications, LNCS n° 1165, pp. 500–510, 1996.
J.R. Abrial, L. Mussat, Specification and Design of a transmission protocol by successive refinements using B, Ecole d’été de Marketoberdorf, LNCS, 1997.
G J. Holzmann, State compression in SPIN, Proc. 3rd Spin Workshop, Twente University, April 1997.
P. Godefroid and G J. Holzmann, On the verification of temporal properties, Proc. IFIP/WG6.1 Symp. On Protocols Specification, Testing and Verification, PSTV93, Liege, Belgium, June 1993.
C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, Memory efficient algorithms for the verification of temporal properties, Formal Methods in System Design I, pp. 275–288, 1992.
D.A. Peled, Combining partial order reduction with on-the-fly model-checking, Proc. 6th Int. Conf. On Computer Aided Verification, CAV’94, LNCS n°818, pp. 377- 390, Stanford, Ca., June 1994.
P. Godefroid, Partial-Order methods for the verification of concurrent systems, LNCS 1032, Springer-Verlag, 1996.
J. Cuéllar, I. Wildgruber, D. Barnard, Combining the design of industrial systems with effective verification techniques, FME’94, LNCS n°873, pp. 639–658, 1994.
K. Laster, O. Grumberg, Modular model-checking of software, the international conference on tools and algorithms for the construction and analysis of systems (TACAS’ 98), March-April 1998.
J.-F. Groote and J.-C. van de Pol, A bounded retransmission protocol for large data packets, Technical Report Logic Group Preprint Series 100, Utrecht University, October 93.
K. Havelund and N. Shankar, Experiments in Theorem Proving and Model Checking for Protocol Verification, Proceedings of FME ’96, 1996.
P. d’Argention, et al., Modeling and Verifying a Bounded Retransmission Protocol, Technical Report, University of Twente, 1997.
J.R. Abrial, Constructions d’Automatismes Industriels avec B, Congrès AFADL ’97, ONERA-CERT, Toulouse, Mai 1997.
J. Julliand, Spécifications par raffinement en B et en logique temporelle linéaire: étude du cas d’un robot de transport de pièces, rapport interne du Laboratoire d’Informatique, Université de Franche-Comté, 1998.
F. Bellegarde, J. Julliand, Verifying properties of reactive systems with refinement patterns, Rapport de recherche interne, Université de Franche-Comté, LIB 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag London Limited
About this paper
Cite this paper
Julliand, J., Masson, PA., Mountassir, H. (1999). Modular Verification of Dynamic Properties for Reactive Systems. In: Araki, K., Galloway, A., Taguchi, K. (eds) IFM’99. Springer, London. https://doi.org/10.1007/978-1-4471-0851-1_6
Download citation
DOI: https://doi.org/10.1007/978-1-4471-0851-1_6
Publisher Name: Springer, London
Print ISBN: 978-1-85233-107-8
Online ISBN: 978-1-4471-0851-1
eBook Packages: Springer Book Archive