Global and communicating state machine models in event driven B: a simple railway case study  

Hdl Handle:
http://hdl.handle.net/10149/58310
Title:
Global and communicating state machine models in event driven B: a simple railway case study  
Book Title:
ZB 2002: formal specification and development in Z and B
Authors:
Stoddart, W. J. (Bill); Papatsaras, A. (Antonis)
Editors:
Bert, D. (Didier); Bowen, J. P. (Jonathan); Henson, M. C. (Martin); Robinson, K. (Ken)
Affiliation:
University of Teesside. School of Computing and Mathematics.
Citation:
Stoddart, W. J. and Papatsaras, A. (2002) 'Global and communicating state machine models in event driven B: a simple railway case study', 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B. Grenoble, France, 23 - 25 January, in Bert, D. et al. (eds) ZB 2002: formal specification and development in Z and B, Lecture notes in computer science. Heidelberg: Springer Berlin, pp.77-100.
Publisher:
Springer Berlin / Heidelberg
Conference:
2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, 2002, Grenoble, France, 23 - 25 January, 2002.
Issue Date:
Jan-2002
URI:
http://hdl.handle.net/10149/58310
DOI:
10.1007/3-540-45648-1_24
Additional Links:
http://www.springerlink.com/content/5q6lcnbt6btuhh1e/
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.
Type:
Meetings and Proceedings; Book Chapter
Keywords:
event driven B; global model; state machine model; parameter hiding; scaling
Series/Report no.:
Lecture notes in computer science; 2272
ISBN:
978-3-540-43166-4

Full metadata record

DC FieldValue Language
dc.contributor.authorStoddart, W. J. (Bill)-
dc.contributor.authorPapatsaras, A. (Antonis)-
dc.contributor.editorBert, D. (Didier)-
dc.contributor.editorBowen, J. P. (Jonathan)-
dc.contributor.editorHenson, M. C. (Martin)-
dc.contributor.editorRobinson, K. (Ken)-
dc.date.accessioned2009-04-01T10:48:41Z-
dc.date.available2009-04-01T10:48:41Z-
dc.date.issued2002-01-
dc.identifier.isbn978-3-540-43166-4-
dc.identifier.doi10.1007/3-540-45648-1_24-
dc.identifier.urihttp://hdl.handle.net/10149/58310-
dc.description.abstractWe 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.-
dc.publisherSpringer Berlin / Heidelberg-
dc.relation.ispartofseriesLecture notes in computer science-
dc.relation.ispartofseries2272-
dc.relation.urlhttp://www.springerlink.com/content/5q6lcnbt6btuhh1e/-
dc.subjectevent driven B-
dc.subjectglobal model-
dc.subjectstate machine model-
dc.subjectparameter hiding-
dc.subjectscaling-
dc.titleGlobal and communicating state machine models in event driven B: a simple railway case study  -
dc.typeMeetings and Proceedings-
dc.typeBook Chapter-
dc.contributor.departmentUniversity of Teesside. School of Computing and Mathematics.-
dc.title.bookZB 2002: formal specification and development in Z and B-
dc.identifier.conference2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, 2002, Grenoble, France, 23 - 25 January, 2002.-
ref.assessmentRAE 2008-
or.citation.harvardStoddart, W. J. and Papatsaras, A. (2002) 'Global and communicating state machine models in event driven B: a simple railway case study', 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B. Grenoble, France, 23 - 25 January, in Bert, D. et al. (eds) ZB 2002: formal specification and development in Z and B, Lecture notes in computer science. Heidelberg: Springer Berlin, pp.77-100.-
prism.startingPage77-
prism.endingPage100-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.