The Community for Technology Leaders
Green Image
Issue No. 05 - September/October (1990 vol. 7)
ISSN: 0740-7459
pp: 21-28
<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. Michael Spivey, "Specifying a Real-Time Kernel", IEEE Software, vol. 7, no. , pp. 21-28, September/October 1990, doi:10.1109/52.57889
94 ms
(Ver 3.3 (11022016))