IFM’99 pp 395-414 | Cite as

Requirements for a Temporal B Assigning Temporal Meaning to Abstract Machines… and to Abstract Systems

  • Dominique Méry

Abstract

Abstract Machines Notation (AMN) is the notation of the B method for specifying systems and it is supported by tools providing editing, navigating, animating and proving facilities. AMN permits us to state invariance properties, based on safety conditions, but there are applications, such as telecom services or distributed systems, where fairness and eventuality properties must also be considered. We define a way to extend the B method expressivity by defining a semantics over traces, in the same spirit as the temporal logic of actions does and we provide a semantical framework for defining a extended B method that can exploit the B environments facilities. We analyse requirements for developing effective temporal facilities extending the scope of B and we found our experiment on case studies related to telecommunications services, which provide a framework for getting requirements on the expressivity of the description language for service properties.

Keywords

Dition Editing Suffix Dick 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    J.-R. Abrial. The B book - Assigning Programs to Meanings. Cambridge University Press, 1996.MATHCrossRefGoogle Scholar
  2. [2]
    J.-R. Abrial. Extending b without changing it (for developing distributed systems). In H. Habrias, editor, 1 st Conference on the B method, pages 169–190, November 1996.Google Scholar
  3. [3]
    J.R. Abrial. Cryptographic protocol specification and design. Steria Meeting on protocols, May 1997.Google Scholar
  4. [4]
    J.R. Abrial and L. Mussat. A problem to be studied in tla and in b (b solution). Private Meeting on B and TLA, September 1997.Google Scholar
  5. [5]
    J.R. Abrial and L. Mussat. Specification and design of a transmission protocol by sucessive refinements using B. Steria Meeting on Protocols, May 1997.Google Scholar
  6. [6]
    K. R. Apt and E. R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65–100, 1983.MathSciNetMATHCrossRefGoogle Scholar
  7. [7]
    M. Bonsangue and J. N. Kok. Semantics, orderings and recursion in the weakest precondition calculus. Technical report, CWI, 1992.Google Scholar
  8. [8]
    N. Brown and D. Méry. A Proof Environment for Concurrent Programs. In J. C. P Woodcock and P. G. Larsen, editors, FME93: Industrial-Strength Formal Methods. Springer Verlag, 1993. Lecture Notes in Computer Science 670.Google Scholar
  9. [9]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. Transactions On Programming Languages and Systems, 8(2):244–263, 1986.MATHCrossRefGoogle Scholar
  10. [10]
    J. Fiadeiro and T. Maibaum. Temporal theories as modularisation units for concurrent system specification. Formal Aspects of Computing, 4:239–272, 1992.MATHCrossRefGoogle Scholar
  11. [11]
    J.-P. Gibson, B. Mermet, and D. Méry, Feature interactions: A mixed semantic model approach. In Gerard O’Regan and Sharon Flynn, editors, 1st Irish Workshop on Formal Methods, Dublin, Ireland, July 1997. Irish Formal Methods Special Interest Group (IFMSIG), Springer Verlag.http://ewic.springer.co.uk/.Google Scholar
  12. [12]
    J.-P. Gibson and D. Méry. COTSR Proceedings, chapter Fair Objects, page ?? Computer Science and Electronic Engineering. Horwood Publishing Ltd, October 1998.Google Scholar
  13. [13]
    L. Lamport. A temporal logic of actions. Transactions On Programming Languages and Systems, 16(3):872–923, May 1994.CrossRefGoogle Scholar
  14. [14]
    K. Lano, J. Fiadeiro, and J. Dick. Extending B AMN with concurrency. In Oxford, editor, 3rd Theory and formal Methods Workshop, 1996.Google Scholar
  15. [15]
    B. Mermet and D. Méry. Safe combinations of services using b. In John McDermid, editor, SAFECOMP97 The 16th International Conference on Computer Safety, Reliability and Security, York, September 1997. Springer Verlag.Google Scholar
  16. [16]
    D. Méry. A proof system to derive eventuality properties under justice hypothesis. In J. Gruszka, editor, Mathematical Foundations of Computer Science, volume 233 of Lecture Notes in Computer Science, Bratislava, august 1986. Springer Verlag.Google Scholar
  17. [17]
    D. Méry. Méthode axiomatique pour les propriétés de fatalité des programmes parallèles. RAIRO Informatique Théorique et Application, 21(3):287–322, 1987.MATHGoogle Scholar
  18. [18]
    D. Méry and A. Mokkedem. Crocos: An integrated environment for interactive verification of sdl specifications. In G. Bochmann, editor, Computer-Aided Verification Proceedings, Lecture Notes in Computer Science. Springer Verlag, 1992.Google Scholar
  19. [19]
    D. Méry and J.-F. Pétin. Formal engineering methods for modelling and verification of control systems. In G. Morel and F. Vernadat, editors, 9th Symposium On Information Control in Manufacturing IN COM’9 8, June 24–26 1998.Google Scholar
  20. [20]
    S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. Transactions On Programming Languages and Systems, 4(3):455- 495, July 1982.MATHCrossRefGoogle Scholar
  21. [21]
    D. Park. A predicate transformer for weak fair iteration. In IBM, editor, Proceedings of the IBM conference, pages 259–275. IBM, IBM, 1981.Google Scholar
  22. [22]
    A. Pnueli. The temporal logics of programs. In Proceedings of 18th IEEE Symposium on Foundations of Computer Science, pages 46 – 57, Providence, 1977. IEEE.Google Scholar
  23. [23]
    B. A. Sanders. Eliminating the substitution axiom from unity logic. Formal Aspects of Computing, 3:189–205, 1991.CrossRefGoogle Scholar
  24. [24]
    Steria Méditerrannée.Atelier B, Version 3.2, Manuel de Référence du Langage B. GEC Alsthom Transport and Steria Méditerrannée and SNCF and INRETS and RATP, 1997.Google Scholar

Copyright information

© Springer-Verlag London Limited 1999

Authors and Affiliations

  • Dominique Méry
    • 1
  1. 1.University Henri Poincaré Nancy 1Vandoeuvre-lès-NancyFrance

Personalised recommendations