Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions

  • Françoise Bellegarde
  • Samir Chouali
  • Jacques Julliand
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


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.


B event systems1 fairness hypotheses specification PLTLverification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. R. Abrial. The B Book. Cambridge University Press — ISBN 0521-496195, 1996.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    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.Google Scholar
  4. 4.
    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.Google Scholar
  5. 5.
    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.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    R. Bharadwaj and J. I. Zucker. Direct model checking of temporal properties (version 2). Technical Report CRL Report 317, Communications Research Laboratory, jan 1996.Google Scholar
  8. 8.
    M. J. Butler. Stepwise re.nement of communicating systems. Science of Computer Programming, 27(2):139–173, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    M. J. Butler and M. Walden. Distributed system development in B. In H. Habrias, editor, First B Conference, pages 155–168, November 1996.Google Scholar
  11. 11.
    E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275–306, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    K. Etessami and G. Holzmann. Optimizing Büchi automata. In Proceedings of 11th Int. Conf. on Concurrency Theory (CONCUR), pages 153–167, 2000.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    G. Holzmann. Design and validation of protocols. Prentice hall software series, 1991.Google Scholar
  16. 16.
    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.Google Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    L. Lamport. A temporal logic of actions. ACM Transactions On Programming Languages And Systems, TOPLAS, 16(3):872–923, May 1994.CrossRefGoogle Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag-ISBN 0-387-97664-7, 1992.Google Scholar
  21. 21.
    Zohar Manna and Amir Pnueli. Models for reactivity. Acta Informatica, 30(7):609–678, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    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.Google Scholar
  23. 23.
    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.Google Scholar
  24. 24.
    R. E. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput, 1:146–160, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    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.Google Scholar
  26. 26.
    M. Y. Vardi and P. Wolper. Reasonning about infinite computations. Information and Computation, 115(1):1–37, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Françoise Bellegarde
    • 1
  • Samir Chouali
    • 1
  • Jacques Julliand
    • 1
  1. 1.Université de Franche-ComtéLaboratoire d’Informatique de l’Université de Franche-ComtéBesançon CedexFrance

Personalised recommendations