Abstract
We present our experiences in developing and using the specification for a safety-critical system. This system is an experimental medical device that is designed to perform robotic human neurosurgery. Our goal is to use this system as a case study to examine the role of software in such systems and the role of specification in achieving safe operation. Our experience with this case study has taught us that although formal specifications are of great value, their use alone is not sufficient to achieve high levels of safety. Required in addition are a clear definition of software safety and a rigorous process for developing the necessary specifications. We present, in addition, some observations on the use of Z in safety-critical applications.
Sponsored in part by NASA under grant number NAG-1-1123.
This is a preview of subscription content, log in via an institution to check access.
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
Siewiorek DP, Swarz RS. The theory and practice of reliable system design. Digital Press, Bedford, Massachusetts 1982
Spivey M. The Z notation: a reference manual. Prentice Hall International 1989
Wika KG, Lawson MA, Gillies GT, Ritter RC. A user interface and control algorithm for the video tumor fighter. Technical Report UVA/640419/NEEP91/112, Department of Nuclear Engineering and Engineering Physics, University of Virginia, 1991
Knight JC, Kienzle DM. Safety-critical computer applications: the role of software engineering. Technical Report TR-92–23, Department of Computer Science, University of Virginia, 1992
Schlichting RD, Schneider FB. Fail-stop processors: an approach to designing fault-tolerant computing systems. ACM Trans on Comp Sys 1983; 1(3)
Green A. Safety systems reliability. John Wiley & Sons, New York 1983
Thomson J. Engineering safety assessment. John Wiley & Sons, New York 1987
Leveson N, Harvey P. Analyzing software safety. IEEE Trans on Soft Eng 1983; SE-9(5)
Anderson T, Witty R. Safe programming. Bit 1978; 18
Boehm BW. A spiral model of software development and enhancement. IEEE Computer 1988; 21(5)
Basili VR, Turner AJ. Iterative enhancement: a practical technique for software development. IEEE Trans on Soft Eng 1975; SE-1(4)
Diller A. Z: an introduction to formal methods. John Wiley & Sons, New York 1990
Ince DC. An introduction to discrete mathematics and formal system specification. Oxford University Press, New York 1988
Potter B, Sinclair J, Till D. An introduction to formal specification and Z. Prentice Hall, New York 1991
Woodcock JCP, Loomes M. Software engineering mathematics. Addison-Wesley, Reading, Massachusetts 1988
Heninger KL. Specifying software requirements for complex systems: new techniques and their application. IEEE Trans on Soft Eng 1980; SE-6(1)
Tracz W (editor). Software reuse: emerging technology. IEEE Computer Society Press, 1988
Duke D, Duke R. Towards a semantics for Object-Z. VDM ‘80: VDM and Z - formal methods in software development. Proceedings, 3rd VDMEurope symposium 1990, Kiel, FRG, Springer-Verlag 1990
Delisle N, Garlan D. Formal specifications as reusable frameworks. VDM ‘80: VDM and Z - formal methods in software development. Proceedings, 3rd VDM-Europe symposium 1990, Kiel, FRG, Springer-Verlag 1990
Hall A. Using Z as a specification calculus for object-oriented systems. VDM ‘80: VDM and Z - formal methods in software development. Proceedings, 3rd VDM-Europe symposium 1990, Kiel, FRG, Springer-Verlag 1990
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Knight, J.C., Kienzle, D.M. (1993). Preliminary Experience Using Z to Specify a Safety-Critical System. In: Bowen, J.P., Nicholls, J.E. (eds) Z User Workshop, London 1992. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3556-2_8
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3556-2_8
Publisher Name: Springer, London
Print ISBN: 978-3-540-19818-5
Online ISBN: 978-1-4471-3556-2
eBook Packages: Springer Book Archive