Abstract
A model-based formal specification of the steam boiler problem is presented, using VDM-SL. The development of the specification follows an environment-based approach. First, the physical boiler is specified, then its interface with the control system and finally, the control system itself. The integrations of the interface and of the controller in the specification of the boiler take the form of successive refinements. The approach has several advantages: it provides a methodological guidance to the specification activity and tends to avoid over-specification and premature design decisions, by focusing later on the control aspects of the problem.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
D.J. Andrews, H. Bruun, B.S. Hansen, P.G. Larsen, N. Plat, et al. Information Technology — Programming Languages, their environments and system software interfaces — Vienna Development Method-Specification Language Part 1: Base language. ISO, 1995.
J.R. Abrial. The B-Book. Cambridge University Press, to appear in 1996.
D. Craigen, S. Gerhart, and T. Ralston. An international survey of industrial applications of formal methods. Technical Report NISTGCR 93/626, U.S. National Institute of Standards and technology, 1993.
R. Elmstrom, P. G. Larsen, and P. B. Lassen. The IFAD VDM-SL tool-box: a practical approach to formal specifications. ACM SIGPLAN Notices, 29(9):77–80, 1994.
M.A. Jackson. System development. Prentice-Hall, 1983.
C. B. Jones. Systematic Software Development Using VDM (Second Edition). Prentice-Hall, London, 1990.
L. Lamport. The temporal logic of actions. Technical Report SRC-79, DEC Systems Research Center, Palo Alto, december 1991.
Y. Ledru and P. Collette. Environment-based development of reactive systems. In D. Till, editor, Sixth BCS-FACS Refinement Workshop, London, Workshops in Computing. Springer Verlag, 1994.
Y. Ledru. Towards the formal development of terminating reactive systems. PhD thesis, Université Catholique de Louvain, Unité d'Informatique, 1991.
Y. Ledru. Developing reactive systems in a VDM framework. Science of Computer Programming, 20(1–2):51–71, 1993.
J.M. Spivey. The Z notation — A Reference Manual (Second Edition). Prentice Hall, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ledru, Y., Potet, ML. (1996). A VDM specification of the steam-boiler problem. In: Abrial, JR., Börger, E., Langmaack, H. (eds) Formal Methods for Industrial Applications. Lecture Notes in Computer Science, vol 1165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027242
Download citation
DOI: https://doi.org/10.1007/BFb0027242
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61929-1
Online ISBN: 978-3-540-49566-6
eBook Packages: Springer Book Archive