This Article 
 Bibliographic References 
 Add to: 
Specifying a Safety-Critical Control System in Z
February 1995 (vol. 21 no. 2)
pp. 99-106
This paper presents a formal specification in the Z notation for a safety-critical control system. It describes a particular medical device but is quite generic and should be widely applicable. The specification emphasizes safety interlocking and other discontinuous features that are not considered in classical control theory. A method for calculating interlock conditions for particular operations from system safety assertions is proposed; it is similar to ordinary Z precondition calculation, but usually results in stronger preconditions. The specification is presented as a partially complete framework that can be edited and filled in with the specific features of a particular control system. Our system is large but the specification is concise. It is built up from components, subsystems, conditions and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The specification illustrates several useful idioms of the Z notation, and demonstrates that an object-oriented specification style can be expressed in ordinary Z.

[1] D. Craigen,“FM89: Assessment of formal methods for trustworthy computer systems,”in12th Int. Conf. Software Engineering Proc.,1990, pp. 233–235.
[2] K. L. Heninger,“Specifying software requirements for complex systems: New techniques and their application,”IEEE Trans. Software Eng.,vol. SE-6, no. 1, pp. 2–13, 1980.
[3] D. Garlan and N. Delisle,“Formal specifications as reusable frameworks,”inVDM '90, 3rd Int. Symp. VDM Europe Proc.New York: Springer-Verlag, 1990.
[4] G. F. Franklin, J. D. Powell, and A. Emami-Naeini,Feedback Control of Dynamic Systems,2nd ed. Reading, MA: Addison-Wesley, 1991.
[5] M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. E. Melhart,“Software requirements analysis for real-time process control systems,”IEEE Trans. Software Eng.,vol. 17, no. 3, pp. 241–258, Mar. 1991.
[6] D. L. Parnas and J. Madey,“Functional Documentation for Computer Systems Engineering, Version 2,”Tech. Rep., CRL Report no. 237, Telecommun. Res. Inst. Ontario (TRIO), McMaster University, Hamilton, Ontario, L8S 4K1, Sept. 1991.
[7] J. Jacky,“Formal specifications for a clinical cyclotron control system,”inProc. ACM SIGSOFT Int. Workshop Formal Methods Software Develop.(Napa, CA,) May 9–11, 1990, pp. 45–54.
[8] ——,“Formal specification and development of control system input/output,”inZ User Workshop, London 1992,J. P. Bowen and J. E. Nicholls, Eds., pp. 95–108.
[9] R. Risler, J. Eenmaa, J. P. Jacky, I. J. Kalet, P. Wootton, and S. Lindbaeck,“Installation of the cyclotron based clinical neutron therapy system in Seattle,”inProc. Tenth Int. Conf. Cyclotrons, Applicat.(East Lansing, MI), May 1984, pp. 428–430.
[10] J. Jacky, R. Risler, I. Kalet, and P. Wootton,“Clinical neutron therapy system, control system specification, Part I: System overview and hardware organization,”Radiation Oncology Dep., Univ. Washington, Seattle, WA, Tech. Rep. 90-12-01, Dec. 1990.
[11] J. Jacky, R. Risler, I. Kalet, P. Wootton, and S. Brossard,“Clinical neutron therapy system, control system specification, Part II: User operations,”Radiation Oncology Dep., Univ. Washington, Seattle, WA, Tech. Rep. 92-05-01, May 1992.
[12] J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, Englewood Cliffs, N.J., 1992.
[13] B. Potter, J. Sinclair, and D. Till, An Introduction to Formal Specification and Z, Int'l Series in Computer Science, Prentice Hall, New York, 1991.
[14] J. B. Wordsworth,Software Development With Z: A Practical Approach to Formal Methods in Software Engineering,Reading, MA: Addison-Wesley, 1992.
[15] S. Stepney, R. Barden, and D. Cooper,“A survey of object orientation in Z,”Software Eng. J.,vol. 7, no. 2, pp. 150–160, Mar. 1992.
[16] C. Morgan and B. Sufrin,“Specification of the UNIX file system,”IEEE Trans. Software Eng.,vol. SE-10, pp. 128–142, Mar. 1984.
[17] R. Macdonald,“Z usage and abusage,”Royal Signals and Radar Establishment, St. Andrews Rd., Malvern, Worcestershire, WR14 3PS, Tech. Rep. 91003, Feb. 1991.

Index Terms:
Formal specification, process control, safety, medical applications, radiation therapy, cyclotron, Z
Jonathan Jacky, "Specifying a Safety-Critical Control System in Z," IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 99-106, Feb. 1995, doi:10.1109/32.345826
Usage of this product signifies your acceptance of the Terms of Use.