Abstract
When specifying a reactive system, we need to consider both the system itself, and the environment it operates in. A suitable formalism for such a task is the Event Calculus, a theory of synchronised state machines which lends itself to diagrammatic representation and which can be conveniently formulated in Z. In this paper we describe an approach to behavioural refinement in the Event Calculus. We consider a gas burner, starting with an outline description of its physical behaviour, then refining this by adding additional details and constraints. Each refinement step is achieved by adding a new (and simple) state machine to our existing model.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R.: Extending B without Changing it (for Developing Distributed Systems). In: Habrias, H. (ed.) Proc. 1st B Conference (1996) ISBN: 2-906082-25-2
Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)
Back, R.J.R.: Correctness preserving program refinements. Tract 131, Mathematish Centrum (1980)
Butler, M., Waldén, M.: Distributed System Development in B. In: Habrias, H. (ed.) Proc. 1st B Conference (1996) ISBN: 2-906082-25-2
Butler, M.: An approach to the design of distributed systems with B AMN. In: Till, D., P. Bowen, J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)
Derrick, J., Boiten, E., Bowman, H., Steen, S.: Weak Refinement in Z. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 369–388. Springer, Heidelberg (1997)
Engel, M.: Specifying Real Time Systems with Z and the Duration Calculus. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge, pp. 282–294. Springer, Heidelberg (1994)
Evans, A.S.: Visualising Concurrent Z Specifications. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop. Workshops in Computing, Cambridge, pp. 269–281. Springer, Heidelberg (1994)
Evans, A.S.: Specifying and Verifying Concurrent Systems Using Z. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 366–380. Springer, Heidelberg (1994)
Evans, A.S.: An Improved Recipe for Specifying Reactive Systems in Z. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 275–294. Springer, Heidelberg (1997)
Fencott, P.C.: Formal Methods for Concurrency. Chapman and Hall, Boca Raton (1995)
Galloway, A.J., Stoddart, W.J.: An Operational Semantics for ZCCS. In: Hinchey, M.G., Liu, S. (eds.) Proc. International Conference of Formal Engineering Methods (ICFEM). IEEE Computer Society Press, Los Alamitos (1997)
Galloway, A.J., Stoddart, W.J.: Comparative Formal Methods. In: Proc. INFORSID (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International Series in Computer Science (1985)
Lano, K.: Specifying Reactive Systems in B AMN. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 242–274. Springer, Heidelberg (1997)
Mahoney, B., Hayes, I.: A Case Study in Timed Refinement: A Mine Pump. IEEE Transactions on Software Engineering 18(9), 817–826 (1992)
Milner, R.: Communication and Concurrency. Prentice Hall International Series in Computer Science (1989)
Morgan, C.C.: Programming from Specifications. Prentice Hall International Series in Computer Science (1990)
Stoddart, W.J.: An Event Calculus Treatment of the Invoicing of Orders. In: Habrias, H., Galloway, A.J. (eds.) International Workshop on Comparing System Specification Techniques. IRIN, Université de Nantes, France (1998) ISBN: 2-906082-29-5
Stoddart, W.J., Knaggs, P.: The Event Calculus (formal specification of real time systems by means of Z and diagrams). In: Habrias, H. (ed.) 5th International Conference on putting into practice methods and tools for information system design, University of Nantes, France (1992)
Stoddart, W.J.: The Event Calculus, extensions for modelling hybrid systems. Technical Report tees-scm-2-96, University of Teesside, UK (1996)
Stoddart, W.J.: The Event Calculus, vsn 2. Technical Report tees-scm-1-96, University of Teesside, UK (1996)
Stoddart, W.J.: An Introduction to the Event Calculus. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212. Springer, Heidelberg (1997)
Stoddart, W.J., Dunne, S.E., Fencott, P.C.: Modelling Hybrid Systems in Z. In: Habrias, H. (ed.) Z Twenty Years on: What is its Future?, IRIN, Université de Nantes, France, pp. 11–25 (1995)
Stoddart, W.J., Dunne, S.E., Galloway, A.J., Shore, R.: Abstract state machines: Designing distributed systems with state machines and B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 226. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stoddart, B. (1998). The Specification and Refinement of an Environmental Model. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive