|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| J. Michael Spivey, "Specifying a Real-Time Kernel," IEEE Software, vol. 7, no. 5, pp. 21-28, September/October, 1990. | |||
| BibTex | x | ||
| @article{ 10.1109/52.57889, author = {J. Michael Spivey}, title = {Specifying a Real-Time Kernel}, journal ={IEEE Software}, volume = {7}, number = {5}, issn = {0740-7459}, year = {1990}, pages = {21-28}, doi = {http://doi.ieeecomputersociety.org/10.1109/52.57889}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - MGZN JO - IEEE Software TI - Specifying a Real-Time Kernel IS - 5 SN - 0740-7459 SP21 EP28 EPD - 21-28 A1 - J. Michael Spivey, PY - 1990 KW - 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 VL - 7 JA - IEEE Software ER - | |||
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.