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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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.
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.
Jean-Raymond Abrial. The B Book. Cambridge University Press, 1996.
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.
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.
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.
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.
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.
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.
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.
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.
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
Papatsaras, A., Stoddart, B. (2002). Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study. 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_24
Download citation
DOI: https://doi.org/10.1007/3-540-45648-1_24
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