Abstract
In this report, we describe an approach that integrates a mathematical specification language with more traditional software design techniques to yield a practicable methodology for the specification of safety-critical control systems. To manage complexity and to foster separation of concerns, the system design model is divided into three views: the architectural view, specified with object and class diagrams; the reactive view, specified with statecharts; and the functional view, specified with Z. A systematic relationship between the reactive and the functional view entails proof obligations to guarantee semantic compatibility. We illustrate this approach with a case study on controlling a heavy hydraulic press.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. M. Barroca, J. S. Fitzgerald, and L. Spencer. The architectural specification of an avionics subsystem. In IEEE Workshop on Industrial-strength Formal Specification Techniques, pages 17–29. IEEE Press, 1995.
G. Booch. Object-Oriented Analysis and Design with Applications. Benjamin Cummings, second edition, 1994.
D. Craigen, S. Gerhart, and T. Ralston. An international survey of industrial applications of formal methods. Technical Report NISTGCR 93/626, National Institute of Standards and Technology, Gaithersburg, MD 20899, 1993.
Zentralstelle für Unfallverhütung und Arbeitsmedizin. Pressen — Sicherheitsregeln für Zweihandschaltungen an kraftbetriebenen Pressen der Metallbearbeitung. Hauptverband der gewerblichen Berufsgenossenschaften, Langwartweg 103, 5300 Bonn 1, 2nd edition, 1978.
D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231–274, 1987.
D. Harel and E. Gery. Executable Object-Modeling with Statecharts. In to appear, editor, Proc. ICSE 18, 1996.
M. Heisel, S. Jähnichen, M. Simons, and M. Weber. Embedding mathematical techniques into system engineering. In M. Wirsing, editor, ICSE-17 Workshop on Formal Methods Application in Software Engineering Practice, pages 53–60, 1995.
I. Houston and S. King. CICS Project Report: Experiences and Results from the Use of Z in IBM. In S.Prehn and W. J.Toetenel, editors, VDM'91 Formal Software Development Methods, volume 551 of LNCS, pages 588–596. Springer-Verlag, 1991.
Y. Kestens and A. Pnueli. Timed and Hybrid Statecharts and their Textual Representation, volume 299 of LNCS, pages 591–620. Springer-Verlag, 1992.
J. Rumbaugh et al. Object-Oriented Modeling and Design. Prentice-Hall, 1991.
B. Selic, G. Gullekson, and P. T. Ward. Real-Time Object-Oriented Modeling. John Wiley & Sons, 1994.
IEEE Software. Safety-Critical Systems. IEEE, January 1994.
M. Spivey. The Z Notation, A Reference Manual. Prentice Hall, 2nd edition, 1992.
M. von der Beeck. A comparison of Statecharts variants. In Symposium on Fault-Tolerant Computing, LNCS. Springer, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weber, M. (1996). Combining statecharts and Z for the design of safety-critical control systems. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_94
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_94
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive