The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (1995 vol.21)
pp: 99-106
ABSTRACT
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.
INDEX TERMS
Formal specification, process control, safety, medical applications, radiation therapy, cyclotron, Z
CITATION
Jonathan Jacky, "Specifying a Safety-Critical Control System in Z", IEEE Transactions on Software Engineering, vol.21, no. 2, pp. 99-106, February 1995, doi:10.1109/32.345826
19 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool