Abstract
A B event systems is supposed to specify a closed system, i.e., the system is meant to be specified in isolation. So, the specifi- cation includes the specification of the system of interest and of its environment. Often, the environment supposes fairness constraints. Therefore, classically in a B system approach, we express the fairness of the environment by the specification of fair scheduler together with the events of the system of interest. This leads to an infinite state model even when the system is finite state by nature. This does not facilitate PLTL properties verification by model checking which is only effective on finite state models. In this paper, we propose to keep separate the fairness of the environment from the specification of the system of interest by a B event system. Then, the fairness is expressed as events which have to be fairly fired. So, a finite state system of interest has a finite state model. The chosen model is a finite labeled transition system which allows the model checking of PLTL properties using the fair events as assumptions. In the paper, we make diverse proposals-some of them are proposed as perspectives-for a verification under fairness assumptions. We use the protocol T=1 as a running example.
Submission to the B program committee
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. R. Abrial. The B Book. Cambridge University Press — ISBN 0521-496195, 1996.
J. R. Abrial and L. Mussat. Introducing dynamic constraints in B. In Second Conference on the B method, France, volume 1393 of LNCS, pages 83–128. Springer Verlag, April 1998.
R. J. Back and R. Kurki-Sunio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symposium on principles of distributed computing, pages 131–142, 1983.
F. Bellegarde, S. Chouali, J. Julliand, and O. Kouchnarenko. Comment limiter la spécification de l’équité dans les systèmes d’événements B. In Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL’01), pages 205–219, Nancy, France, 2001.
D. Bert. Preuve de propriétés d’équité en B: étude du protocole du bus SCSI-3. In Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL’01), pages 221–241, Nancy, France, 2001.
D. Bert and F. Cave. Construction of finite labelled transition systems from B abstract systems. In In proc. of IFM’2000, volume 1945 of LNCS, pages 235–254. Springer Verlag, November 2000.
R. Bharadwaj and J. I. Zucker. Direct model checking of temporal properties (version 2). Technical Report CRL Report 317, Communications Research Laboratory, jan 1996.
M. J. Butler. Stepwise re.nement of communicating systems. Science of Computer Programming, 27(2):139–173, 1996.
M. J. Butler. An approach to the design fo distributed systems with B amn. In J. P Brown and D. Till, editors, 10th International Conference of Z Users (ZUM’97), volume LNCS 1212, pages 223–241. Springer-Verlag, April 1997.
M. J. Butler and M. Walden. Distributed system development in B. In H. Habrias, editor, First B Conference, pages 155–168, November 1996.
E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275–306, 1987.
K. Etessami and G. Holzmann. Optimizing Büchi automata. In Proceedings of 11th Int. Conf. on Concurrency Theory (CONCUR), pages 153–167, 2000.
Comité européen de Normalisation. En27816-3. European standard — identification cards — integrated circuit(s) card with contacts-electronic signal and transmission protocols. Technical Report ISO/CEI 7816-3, 1992.
R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. IFIP-WG6.1 Symposium On Protocols Specification, Testing and Verification (PSTV95), pages 2–21, Warsaw-Poland, 1995.
G. Holzmann. Design and validation of protocols. Prentice hall software series, 1991.
J. Julliand, P.A. Masson, and H. Mountassir. Vérification par model checking modulaire des propriétés dynamiques introduites en B. In Technique et Science Informatiques, 2001. to appear.
Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In REX WorkshopA Decade of Concurrency, volume 803 of Lecture Notes in Computer Science, pages 273–346. Springer Verlag, 1993.
L. Lamport. A temporal logic of actions. ACM Transactions On Programming Languages And Systems, TOPLAS, 16(3):872–923, May 1994.
Z. Manna and A. Pnueli. A hierarchy of temporal properties. In Proceedings of the 9th ACM Symposium on Principles of Distributed Computing (PODC), pages 377–408, New York, NY, 1990. ACM Press.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag-ISBN 0-387-97664-7, 1992.
Zohar Manna and Amir Pnueli. Models for reactivity. Acta Informatica, 30(7):609–678, 1993.
Steria Méditerranée. Le langage B. Manuel de référence version 1.5. S.A.V. Steria, BP 16000, 13791 Aix-en-Provence cedex 3, France.
B. Parreaux. Vérification de systèmes d’événements B par model-checking PLTL. PhD thesis, U.F.R. des Sciences et Techniques, Université de Franche-Comté, Décembre 2000.
R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput, 1:146–160, 1972.
M. Vardi and P. Wolper. An automata-theoric approach to automatic program verification. In 1 st IEEE Symp. Logic in Computer Science (LICS’86), pages 332–344, Cambridge, MA, USA, june 1986.
M. Y. Vardi and P. Wolper. Reasonning about infinite computations. Information and Computation, 115(1):1–37, 1994.
P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Int. Workshopon Automatic Verification Methods for Finite State Systems, LNCS 407, pages 68–80, Grenoble, France, june 1989. Springer Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bellegarde, F., Chouali, S., Julliand, J. (2002). Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds) ZB 2002:Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol 2272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45648-1_25
Download citation
DOI: https://doi.org/10.1007/3-540-45648-1_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43166-4
Online ISBN: 978-3-540-45648-3
eBook Packages: Springer Book Archive