This Article 
 Bibliographic References 
 Add to: 
Specifying a Real-Time Kernel
September/October 1990 (vol. 7 no. 5)
pp. 21-28

The application of formal methods to a safety-critical system is illustrated. The objective of the study was to improve the existing documentation of a diagnostic X-ray machine to serve later reimplementations. The separation of the kernel from applications helped identify a design flaw in the kernel that could have caused damage by the X-ray application. The case study which shows that mathematical techniques have an important role to play in documenting systems and avoiding design flaws, is a good example of the use of the Z (pronounced 'Zed') notation and its methods for modeling systems. The limitations of this specification are delineated, showing that there is a need for other specification techniques to tackle the remaining properties, like real-time performance, for completeness and comparison.

Index Terms:
real-time kernel; safety-critical system; documentation; diagnostic X-ray machine; design flaw; X-ray application; case study; mathematical techniques; Z; specification techniques; real-time performance; completeness; formal specification; medical diagnostic computing; safety; software reliability; X-ray applications
J. Michael Spivey, "Specifying a Real-Time Kernel," IEEE Software, vol. 7, no. 5, pp. 21-28, Sept.-Oct. 1990, doi:10.1109/52.57889
Usage of this product signifies your acceptance of the Terms of Use.