Advertisement

Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study

  • Antonis Papatsaras
  • Bill Stoddart
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)

Abstract

We present a case study of a simple railway system to investigate and compare two ways of modelling a system in “event driven B”. We are interested in the specification of a system as a global model as well as the formulation of a distributed state machine model where individual components exchange information by means of shared events. In this paper we investigate the issues of “parameter hiding” and “scaling” as well as the parameterisation of events of the communicating components of such systems. We use two methods for expressing a class of components; we either create indexed B machines that can be instantiated or we represent the state of all components within a given class by means of a function.

Keywords

State Machine Global Model Parallel Composition Signal Setting Speed Controller 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J R Abrial. Extending B without Changing it (for Developing Distributed Systems). In H Habrias, editor, The First B Conference, ISBN: 2-906082-25-2, 1996.Google Scholar
  2. 2.
    J R Abrial and L Mussat. Introducing Dynamic Constraints in B. In Bert D, editor, B98: Recent Developments in the Use of the B Method., number 1393 in Lecture Notes in Computer Science, 1998.Google Scholar
  3. 3.
    Jean-Raymond Abrial. The B Book. Cambridge University Press, 1996.Google Scholar
  4. 4.
    M Butler. csp2B: A practical approach to combining CSP and B. In J M Wing, Woodcock J, and Davies J, editors, FM99vol 1, Lecture Notes in Computer Science, no 1708. Springer Verlag, 1999.Google Scholar
  5. 5.
    M Butler and M Waldén. Distributed System Development in B. In H Habrias, editor, The First B Conference, ISBN: 2-906082-25-2, 1996.Google Scholar
  6. 6.
    M J Butler. An approach to the design of distributed systems with B AMN. In J P Bowen, M J Hinchey, and Till D, editors, ZUM’ 97: The Z Formal Specification Notation, number 1212 in Lecture Notes in Computer Science, 1997.CrossRefGoogle Scholar
  7. 7.
    Treharne H and Schneider S. How to Drive a B Machine. In Bowen J P, Dunne S, Galloway A, and King S, editors, ZB 2000: Formal Speci.cation and Development in Z and B, Lecture Notes in Computer Science, no 1878. Springer Verlag, 2000.CrossRefGoogle Scholar
  8. 8.
    K Robinson. Reconciling Axiomatic and Model-Based Specifications Using the B Method. In Bowen J P, Dunne S, Galloway A, and King S, editors, ZB 2000: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, no 1878. Springer Verlag, 2000.CrossRefGoogle Scholar
  9. 9.
    W J Stoddart. An Introduction to the Event Calculus. In J P Bowen, M J Hinchey, and Till D, editors, ZUM’ 97: The Z Formal Specification Notation, number 1212 in Lecture Notes in Computer Science, 1997.CrossRefGoogle Scholar
  10. 10.
    W J Stoddart, S E Dunne, Galloway A J, and Shore R. Abstract State Machines: Designing Distributed Systems with State Machines and B. In Bert D, editor, B98: Recent Developments in the Use of the B Method., number 1393 in Lecture Notes in Computer Science, 1998.CrossRefGoogle Scholar
  11. 11.
    W J Stoddart and P K Knaggs. The Event Calculus, (formal specification of real time systems by means of Z and diagrams). In H Habrias, editor, 5th International Conference on putting into practice methods and tools for information system design. University of Nantes, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Antonis Papatsaras
    • 1
  • Bill Stoddart
    • 1
  1. 1.School of Computing and MathematicsUniversity of TeessideMiddlesbroughEngland

Personalised recommendations