Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study
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.
KeywordsState Machine Global Model Parallel Composition Signal Setting Speed Controller
Unable to display preview. Download preview PDF.
- 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.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.Jean-Raymond Abrial. The B Book. Cambridge University Press, 1996.Google Scholar
- 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.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
- 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