Abstract
This paper describes techniques for specifying and designing reactive systems in the B Abstract Machine (AMN) language, using concepts from procedural process control. In addition, we consider what forms of concurrent extensions to B AMN would make it more effective in representing such systems.
Preview
Unable to display preview. Download preview PDF.
References
J-R Abrial. The B Book: Deriving Programs from Meaning, Cambridge University Press, 1996.
J Bowen and V Stavridou. Safety-critical systems, formal methods and standards, Software Engineering Journal, July 1993, pages 189–209.
M Butler. Combining Action Systems and B AMN in the Design of Distributed Systems. Dept. of Electronics and Computer Science, University of Southampton, 1996.
E Durr and E Dusink. The role of VDM++ in the development of a real-time tracking and tracing system. In J Woodcock and P Larsen, editors, FME '93, Lecture Notes in Computer Science. Springer-Verlag, 1993.
J Fiadeiro and T Maibaum. Temporal Theories as Modularisation Units for Concurrent System Specification, Formal Aspects of Computing 4(3), pp. 239–272, 1992
J Fiadeiro and T Maibaum. Interconnecting formalisms: supporting modularity, reuse and incrementality, in Proc. 3rd Symposium on the Foundations of Software Engineering, ACM Press, 1996.
C Fidge. Proof Obligations for Real-Time Refinement, Proceedings of 6th Refinement Workshop, Springer-Verlag Workshops in Computing, 1994.
D Harel. On Visual Formalisms, Communications of the ACM 31(5), pp. 514–530, May 1988.
H Haughton and K Lano. Testing and Safety analysis of AM specifications, in Proceedings of the 6th Refinement Workshop, City University, London. Springer-Verlag Workshops in Computing, 1994.
I Hayes and M Utting. Coercing Real-time Refinement: A Transmitter, Northern Formal Methods Workshop, Ilkley, 1996. To appear in Springer-Verlag EWICS, 1997.
J Hoare. The Use of B in CICS, in Applications of Formal Methods, M G Hinchey and J P Bowen (Eds.), Prentice Hall, 1995.
K Lano. The B Language and Method: A Guide to Practical Formal Development, FACIT Series, Springer-Verlag, 1996.
K Lano, J Fiadeiro and J Dick. Extending B AMN with Concurrency, 3rd Theory and Formal Methods Workshop, Oxford. Imperial College Press, 1996.
K Lano, J Bicarregui and A Sanchez. Using B to Design and Verify Controllers for Chemical Processing, Conference on B, IRIN, Nantes, 1996.
K Lano, J Bicarregui and S Kent. A Real-time Action Logic of Objects, ECOOP 96 Workshop on Proof Theory of Object-oriented Systems, Linz, Austria, 1996.
K Lano and S Goldsack. Refinement Rules for Concurrency and Real-time, MEDI-CIS Workshop, April 1996.
K Lano and A Sanchez. Specification of a Chemical Process Controller in VDM ++ and B, ROOS project document GR/K68783-11, Dept. of Computing, Imperial College, November 1996.
C Lewerentz and T Lindner (Eds.). Formal development of reactive systems: case study production cell, Berlin: Springer-Verlag, LNCS 891, 1995.
I Moon, G Powers, J R Burch and E M Clarke. Automatic Verification of Sequential Control Systems using Temporal Logic, AIChE Journal, 38(1):67–75, January 1992.
A Pnueli. Linear and Branching Structures in the Semantics and Logics of Reactive Systems, ICALP 85, Springer-Verlag LNCS Vol. 194, 1985.
A Sanchez and S Macchietto. Design of Procedural Controllers for Chemical Processes, ESCAPES Conference, June 1995, Slovenia.
A Sanchez, G E Rotstein, N Alsop and S Macchietto. Procedural Control of Chemical Processes, Chemical Process Control Conference, 1996.
J van de Snepscheunt. Trace Theory and VSLI Design, PhD thesis, Technische Logeschool Eindhoven, Eindhoven, The Netherlands, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lano, K. (1997). Specifying reactive systems in B AMN. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027292
Download citation
DOI: https://doi.org/10.1007/BFb0027292
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive