The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - September/October (1990 vol.7)
pp: 21-28
ABSTRACT
<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>
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
CITATION
J. Michael Spivey, "Specifying a Real-Time Kernel", IEEE Software, vol.7, no. 5, pp. 21-28, September/October 1990, doi:10.1109/52.57889
61 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool