Issue No. 05 - September/October (1990 vol. 7)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/52.57889
<p>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.</p>
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. M. Spivey, "Specifying a Real-Time Kernel," in IEEE Software, vol. 7, no. , pp. 21-28, 1990.