Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

Safety-critical systems, formal methods and standards

Safety-critical systems, formal methods and standards

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Add to cart
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)
Add to cart

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
Software Engineering Journal — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

© The Institution of Electrical Engineers
Published

Standards concerned with the development of safety-critical systems, and the software in such systems in particular, abound today as the software crisis increasingly affects the world of embedded computer-based systems. The use of formal methods is often advocated as a way of increasing confidence in such systems. This paper examines the industrial use of these techniques, the recommendations concerning formal methods in a number of current and draft standards, and comments on the applicability and problems of using formal methods for the development of safety-critical systems on an industrial scale. Some possible future directions are suggested.

Inspec keywords: safety; formal specification; software reliability; real-time systems; standards

Other keywords: embedded computer-based systems; formal methods; software crisis; real-time systems; standards; safety-critical systems

Subjects: Software engineering techniques

References

    1. 1)
      • Mukherjee, P., Stavridou, V.: `The formal specification of safety requirements for the storage of explosives', DITC 185/91, Technical Report, August 1991.
    2. 2)
      • I. Page , W. Luk , W. Moore , W. Luk . (1991) Compiling Occam into field-programmable gate arrays, FPGAs, Oxford Workshop on Field Programmable Logic and Applications.
    3. 3)
      • D. Bjørner . A ProCoS project description: ESPRIT BRA 3104. Bull. Eur. Assoc. Theor. Comput. Sci , 60 - 73
    4. 4)
      • `Z base standard', Draft ISO IEC JTC1/SC22, 1993, available from D. Andrews.
    5. 5)
      • Rushby, J., von Henke, F.: `Formal verification of algorithms for critical systems', Proc. ACM SIGSOFT 91 Conf. on Software for Critical Systems, 1991, 16, SIGSOFT Softw. Eng. Notes, p. 1–15, (5).
    6. 6)
      • P.A.V. Hall . Software development standards. Softw. Eng. J. , 3 , 143 - 147
    7. 7)
      • (1987) , Programmable electronic systems in safety related applications: 1. an introductory guide.
    8. 8)
      • Tierney, M.: `The evolution of Def Stan 00-55 and 00-56: an intensification of the “formal methods debate” in the UK', Proc. Workshop on Policy Issues in Systems and Software Development, Science Policy Research Unit, July 1991, Brighton, UK.
    9. 9)
      • : `Safety of Computer Control Systems 1992', SAFECOMP ′92, Computer Systems in Safety-critical Application, Proc. IFAC Symp., 28–30 October 1992, Zürich Switzerland, Pergamon Press, 1992.
    10. 10)
      • Bjørner, D.: `Trusted computer systems: the ProCos experience', Proc. 12th Int Conf. on Software Engineering, 11–14 May 1992, Melbourne, Australia.
    11. 11)
      • W. Myers . Can software for the strategic defense initiative ever be error-free?. Computer , 11
    12. 12)
      • C.A.R. Hoare , D. Bjørner , H. Langmaack , C.A.R. Hoare . (1993) Algebra and models, Provably correct system.
    13. 13)
      • P.G. Neumann . Illustrative risks to the public in the use of computer systems and related technology. SIGSOFT Softw. Eng. Notes , 1 , 23 - 32
    14. 14)
      • Leveson, N.G., Turner, C.T.: `An investigation of the Therac-25 accidents', 92-108, UCI Technical Report, 1992, (University of Washington, TR 92-11-05).
    15. 15)
      • R.K. Iyer , P. Verlardi . Hardware-related software errors: measurement and analysis. IEEE Trans. , 2
    16. 16)
      • N.G. Leveson . Software safety in embedded computer systems. Commun. ACM , 2 , 34 - 46
    17. 17)
      • Ravn, A.P., Rischel, H.: `Requirements capture for embedded real-time systems', Proc. IMACS-MCTS Symp., May 1991, Lille, France, 2, p. 147–152.
    18. 18)
      • (1991) , The programmable gate array data book.
    19. 19)
      • `Z base standard', Draft ISO IEC JTC1/SC22, 1993, available from the Secretary, ZIP Project.
    20. 20)
      • : `Software for computers in the application of industrial safety related systems', Technical Committee 65, 1 August 1991, International Electrotechnical Commission, Working Group 9 (WG9), IEC 65A (Secretariat) 122, Version 1.0.
    21. 21)
      • J.C. Laprie . (1991) , Dependability: basic concepts and terminology.
    22. 22)
      • Special issue on reliability. IEEE Spectr. , 10
    23. 23)
      • D. Craigen . (1990) , Formal methods for trustworthy computer systems.
    24. 24)
      • `Standard for software engineering of safety critical software', 982 C-H 69002-0001, 21 December 1990.
    25. 25)
      • W.J. Cullyer , M. Joseph . (1988) High integrity computing, Formal techniques in real-time and fault-tolerant systems.
    26. 26)
      • R.W. Selby , V.R. Basiu , F.T. Baker . Cleanroom software development: an empirical evaluation. IEEE Trans. , 9 , 1027 - 1037
    27. 27)
      • A.J. Cohn . (1988) , Correctness properties of the Viper block model: the second level.
    28. 28)
      • Z. Manna , A. Pnueli . (1992) , The temporal logic of reactive and concurrent systems: specification.
    29. 29)
      • Brown, M.J.D.: `Rationale for the development of the UK defence standards for safety-critical computer software', Proc. COMPASS ′90, June 1990, Washington, DC.
    30. 30)
      • (1992) , Software considerations in airborne systems and equipment certification.
    31. 31)
      • Hill, J.V.: `The development of high reliability software—RR&A's experience for safety critical systems', 290, Second IEE/BCS Conf., Software Engineering ′88, July 1988, IEE Conf. Publ., p. 169–172.
    32. 32)
      • Technical Report, 1964, UN Committee for the Transport of Dangerous Goods.
    33. 33)
      • Jacky, J.: `Verification, analysis and synthesis of safety interlocks', 91-04-01, Technical Report, April 1991, Department of Radiation Oncology RC-08.
    34. 34)
      • C. Reade , P. Froome , P. Rook . (1990) Formal methods for reliability, Software reliability handbook.
    35. 35)
      • I. Sommerville . (1992) , Software engineering.
    36. 36)
      • J.P. Bowen , V. Stavridou , J.C.P. Woodcock , P.G. Larsen . (1993) The industrial take-up of formal methods in safety-critical and other areas: a perspective, FME ′93:Industrial-strength Formal Methods, First Int Symp. on Formal Methods Europe.
    37. 37)
      • P.S. Babel . (1987) , Software integrity program.
    38. 38)
      • J.S. Ostroff . Formal methods for the specification and design of real-time safety critical systems. J. Syst. Softw. , 1 , 33 - 60
    39. 39)
      • B.P. Mahony , I.J. Hayes . A case-study in timed refinement: a mine pump. IEEE Trans. , 9 , 817 - 826
    40. 40)
      • Archinoff, G.H., Hohendorf, R.J., Wassyng, A., Quigliey, B., Borsch, M.R.: `Verification of the shut-down system software at the Darlington nuclear generating station', Int Conf. on Control and Instrumentation in Nuclear Installations, May 1990, Glasgow, UK, The Institution of Nuclear Engineers.
    41. 41)
      • D.L. Parnas , G.J.K. Asmis , J. Madey . Assessment of safety-critical software in nuclear power plants. Nucl. Saf. , 2 , 189 - 198
    42. 42)
      • D. Mackenzie . (1991) Negotiating arithmetic, constructing proof: the sociology of mathematics and information technology, Programme on Information & Communication Technologies, Working Paper Series 38.
    43. 43)
      • D.R. Wallace , D.R. Kuhn , L.M. Ippolito . An analysis of selected software safety standards. IEEE Aerosp. Electron. Syst. Mag. , 3 - 14
    44. 44)
      • A. Burns . The HCI component of dependable real-time systems. Softw. Eng. J. , 4 , 168 - 174
    45. 45)
      • M. Dyer . (1992) , The Cleanroom approach to quality software development.
    46. 46)
      • Buth, B., Buth, K-H., Fränzle, M., von Karger, B., Lakhneche, Y., Langmaack, H., Müller-Olm, M.: `Provably correct compiler development and implementation', Compiler Construction ′92, 4th Int. Conf., 1992, Paderborn Germany, 641, Lect. Notes Comput. Sci..
    47. 47)
      • Shostak, R.E., Schwartz, R., Melliar-Smith, P.M.: `STP: a mechanized logic for specification and verification', CADE-6, 6th Int Conf. on Automated Deduction, 1982, 138, Lect. Notes Comput. Sci..
    48. 48)
      • R.E. Bloomfield , J. Brazendale . (1990) SafelT2 — a framework for safety standards, Safety-Related Working Group (SRS-WG).
    49. 49)
      • Wallace, D.R., Kuhn, D.R., Cherniavsky, J.C.: `Report of the NIST workshop of standards for the assurance of high integrity software', August 1991, (available from the Superintendent of Documents, Government, US Printing Office, Washington, DC 20402, USA).
    50. 50)
      • D.I. Good , W.D. Young , S. Prehn , W.J. Toetenel . (1991) Mathematical methods for digital system development, Formal Software Development Methods.
    51. 51)
      • J. Davies . (1991) Specification and proof in real-time systems, Technical Monograph PRG-93.
    52. 52)
      • C.L. Smith . Digital control of industrial processes. Comput. Surv. , 3 , 211 - 241
    53. 53)
      • R. Barden , S. Stepney , D. Cooper , J.E. Nicholls . (1992) The use of Z, Z User Workshop.
    54. 54)
      • J.C. Laprie , T. Anderson . (1989) Dependability: a unifying concept for reliable computing and fault tolerance, Dependability of resilient computers.
    55. 55)
      • J.R. Abrial , M.K.O. Lee , D.S. Neilson , P.N. Scharbach , I.H. Sørensen , S. Prehn , W.J. Toetenel . (1991) The B-method, VDM '91, Formal Software Development Methods.
    56. 56)
      • M. Tierney . (1991) , Some implications of Def Stan 00.55 on the software engineering labour process in safety critical developments.
    57. 57)
      • `Standard for software safety plans', Draft P1228, 11 February 1993, Software Safety Plans Working Group, Draft J.
    58. 58)
      • W.J. Cullyer , C.H. Pygott . Application of formal methods to the VIPER microprocessor. IEE Proc. E , 3 , 133 - 141
    59. 59)
      • S. Bear , S. Prehn , W.J. Toetenel . (1991) An overview of HP-SL, VDM ′91, Formal Software Development Methods.
    60. 60)
      • Craigen, D., Gerhart, S., Ralston, T.J.: `An international survey of industrial applications of formal methods', FME ′93, Industrial-strength Formal Methods, First Int Symp. on Formal Methods, 19–23 April 1993, Odense, Europe Denmark, Lect. Notes Comput. Sci., p. 250–267, 1993, 331.
    61. 61)
      • Rushby, J., von Henke, F., Owre, S.: `An introduction to formal specification and verification using EHDM', SRI-CSL-91-02, Technical Report, February 1991.
    62. 62)
      • Butler, R.W., Finelli, G.B.: `The infeasibility of experimental quantification of life-critical software reliability', Proc. ACM SIGSOFT ′91 Conf. on Software for Critical Systems, 1991, 16, SIGSOFT Softw. Eng. Notes, p. 66–76, (5).
    63. 63)
      • J. Reason . (1990) , Human error.
    64. 64)
      • (1982) , System design analysis.
    65. 65)
      • Hansen, K.M., Ravn, A.P., Rischel, H.: `Specifying and verifying requirements of real-time systems', Proc. ACM SIGSOFT ′91 Conf. on Software for Critical Systems, 1991, 16, SIGSOFT Softw. Eng. Notes, p. 44–54, (5).
    66. 66)
      • Guiho, G., Hennebert, C.: `SACEM software validation', Proc. 12th Int Conf. on Software Engineering, March 1990, IEEE Computer Society Press, p. 186–191.
    67. 67)
      • J. He , I. Page , J.P. Bowen . Towards a provably correct hardware implementation of Occam. Lect. Notes Comput. Sci. , 214 - 225
    68. 68)
      • I. Pyle . Software engineers and the IEE. Softw. Eng. J. , 2 , 66 - 68
    69. 69)
      • Parnas, D.L., Madey, J.: `Functional documentation for computer systems engineering', 237, CRL Report, September 1991, Version 2.
    70. 70)
      • P.J. Probert , D. Djian , H. Huosheng . Transputer architectures for sensing in a robot controller: formal methods for design. Concurrency: Pract. Exp. , 4 , 283 - 292
    71. 71)
      • D.J. Smith , K.B. Wood . (1989) , Engineering quality software: a review of current practices, standards and guide lines including new methods and development tools.
    72. 72)
      • Canning, A.: `Assessment at the requirements stage of a project', 2nd Safety Critical Systems Club Meeting, October 1991, Beaconsfield UK, Advanced Software Department, ERA Technology Ltd, , available from.
    73. 73)
      • R.N. Charette . (1990) , Applications strategies for risk analysis.
    74. 74)
      • de Champeaux, D.: `Formal techniques for OO software development', OOPSLA ′91 Conf. on Object-Oriented Programming Systems, Languages, and Applications, 1991, 26, SIGPLAN Notices, p. 166–170, (11).
    75. 75)
      • W.A. Halang , B. Krämer . Achieving high integrity of process control software by graphical design and formal verification. Softw. Eng. J. , 1 , 53 - 64
    76. 76)
      • J.L. Cyrus , J.D. Bledsoe , P.D. Harry . Formal specification and structured design in software development. Hewlett-Packard J. , 6 , 51 - 58
    77. 77)
      • J.A. McDermid , P.A. Bennett . (1991) Formal methods: use and relevance for the development of safety critical systems, Safety aspects of computer control.
    78. 78)
      • S. Anderson , G. Cleland , F. Redmill . (1992) Adopting mathematicalry-based methods for safety-critical systems production, Safety systems: the safety-critical systems club newsletter.
    79. 79)
      • J.M. Spivey . Specifying a real-time kernel. IEEE Softw. , 5 , 21 - 28
    80. 80)
      • Coleman, D.: `The technology transfer of formal methods: what's going wrong?', Proc. 12th ICSE Workshop on Industrial Use of Formal Methods, March 1990, Nice, France.
    81. 81)
      • (1992) , Risk: analysis, perception and management.
    82. 82)
      • B. Littlewood , D. Miller . (1991) , Software reliability and safety.
    83. 83)
      • S.J. Goldsack , A.C.W. Finkelstein . Requirements engineering for real-time systems. Softw. Eng. J. , 3 , 101 - 115
    84. 84)
      • Waldinger, R.J., Stickel, M.E.: `Proving properties of rule-based systems', Proc. 7th Conf. on Artificial Intelligence Applications, February 1991, IEEE Computer Society, p. 81–88.
    85. 85)
      • C. Neesham . Safe conduct. Computing , 18 - 20
    86. 86)
      • `ESA software engineering standards', ESA PSS-05-0, February 1993, Issue 2.
    87. 87)
      • Hill, J.V.: `Software development methods in practice', Proc. 6th Annual Conf. on Computer Assurance, 1991, COMPASS.
    88. 88)
      • J.M. Spivey . (1992) , The Z notation: a reference manual.
    89. 89)
      • C.L. WrightM , A.J. Zawilski . (1991) , Existing and emerging standards for software safety.
    90. 90)
      • Mayger, E.M., Fourman, M.P.: `Integration of formal methods with system design', Proc. Conf. on Very Large Scale Integration, (VLSI ′91), 1991, Edinburgh, UK, p. 3a.2.1–3a.2.11.
    91. 91)
      • M.D. Harrison , J.E. Nicholls . (1992) Engineering human error tolerant software, Z User Workshop.
    92. 92)
      • Chapront, P.: `Vital coded processor and safety related software design', Proc. IFAC Symp., 28–30 October 1992, Zurich, Switzerland, Pergamon Press, p. 141–145, Safety of Computer Control Systems 1992, Computer Systems in Safety-critical Applications, 1992 SAFECOMP ′92.
    93. 93)
      • (1990) , SafeIT: overall approach.
    94. 94)
      • `Military standard : system safety program requirements', MIL-STD-882B, 30 March 1984.
    95. 95)
      • A.J. Cohn . (1988) A proof of correctness of the Viper microprocesor: the first level, VLSI specification, verification and synthesis.
    96. 96)
      • Thomas, M.C.: `The future of formal methods', Proc. 3rd Annual Z Users Meeting, December 1988, Oxford University Computing Laboratory, , p. 1–3.
    97. 97)
      • D. May , C.A.R. Hoare . (1990) Use of formal methods by a silicon manufacturer, Developments in Concurrency and Communication.
    98. 98)
      • (1987) , Programmable electronic systems in safety related applications: 2. general technical guidelines.
    99. 99)
      • L.E. Moser , P.M. Melliar-Smith . Formal verification of safety-critical systems. Softw.—Pract. Exp. , 8 , 799 - 821
    100. 100)
      • (1992) Safety related computer controlled systems market study, Review for the Department of Trade and Industry by Coopers & Lybrand.
    101. 101)
      • (1991) , The procurement of safety critical software in defence equipment.
    102. 102)
      • P.A. Bennett , J.A. McDermid . (1991) Safety, Software engineer's reference book.
    103. 103)
      • H. Kopetz , R. Zainlinger , G. Fohler , H. Kantz , P. Puschner . The design of realtime systems: from specification to implementation and verification. Softw. Eng. J. , 3 , 73 - 82
    104. 104)
      • J.C. Knight , D.M. Kienzle , J.P. Bowen , J.E. Nicholls . (1993) Preliminary experience using Z to specify a safety-critical system, Z User Workshop.
    105. 105)
      • Parnas, D.L.: `Proposed standard for software for computers in the safety systems of nuclear power stations', 2.117.1, Final Report for Contract, March 1991, (based on IEC Standard 880 [166]).
    106. 106)
      • P.A. Lindsay . A survey of mechanical support for formal reasoning. Softw. Eng.J. , 1 , 3 - 27
    107. 107)
      • D. Gries , E.W. Dijkstra . (1990) Influences (or lack thereof) of formalism in teaching programming and software engineering, Formal development of programs and proofs.
    108. 108)
      • J. Wensley . SIFT: design and analysis of a fault-tolerant computer for aircraft control. Proc. IEEE , 10 , 1240 - 1254
    109. 109)
      • W.J. Cullyer . Hardware integrity. Aeronaut. J. , 263 - 268
    110. 110)
      • Z. Chaochen , C.A.R. Hoare , A.P. Ravn . A calculus of durations. Inf. Process. Lett. , 5 , 269 - 276
    111. 111)
      • : `Software for computers in the safety systems of nuclear power stations', IEC 880, International Electrotechnical Commission, 1986.
    112. 112)
      • Srivas, M., Bickford, M.: `Verification of the FtCayuga fault-tolerant microprocessor system, vol. 1: a case study in theorem prover-based verification', 4381, Contractor Report, July 1991, (work performed by ORA Corporation.).
    113. 113)
      • N. Wirth . Towards a discipline of real-time programming. Commun. ACM , 8 , 577 - 583
    114. 114)
      • Humphrey, W.S., Kitson, D.H., Casse, T.C.: `The state of software engineering practice: a preliminary report', Proc. 11th Int Conf. on Software Engineering, May 1989, Pittsburgh, Pennsylvania, p. 277–288.
    115. 115)
      • Brock, B., Hunt, W.A.: `Report on the formal specification and partial verification of the VIPER microprocessor', 46, Technical Report, January 1990.
    116. 116)
      • J. Jacky , C. Dunlop , R. Kling . (1991) Safety-critical computing: hazards, practices, standards and regulation, Computerization and controversy.
    117. 117)
      • J.P. Bowen , V. Stavridou , H.H. Frey . (1992) Formal methods and software safety, Safety of Computer Control Systems 1992 (SAFECOMP′92).
    118. 118)
      • M.C. Thomas . Development methods for trusted computer systems. Form. Asp. Comput. , 5 - 18
    119. 119)
      • J.R. Abrial . (1991) , The B reference manual.
    120. 120)
      • O. Maler , Z. Manna , A. Pnueli , J.W. de Bakker , C. Huizing , W.P. de Roever , W. Rozenberg . (1992) From timed to hybrid systems, Real-Time: Theory in Practice.
    121. 121)
      • Littlewood, B.: `The need for evidence from disparate sources to evaluate software safety', Proc. Safety-critical Systems Symp., February 1993, Springler-Verlag, , Directions in safety-critical systems.
    122. 122)
      • Subsection on certification of profession. SIGSOFT Softw. Eng. Notes , 1 , 24 - 32
    123. 123)
      • (1989) , ISO 8807: information processing systems — open systems interconnection — LOTOS — a formal description technique based on the temporal ordering of observational behaviour.
    124. 124)
      • R.S. Boyer , J.S. Moore . (1988) , A computational logic handbook.
    125. 125)
      • S. Stepney , R. Barden , D. Cooper . (1992) , Object orientation in Z.
    126. 126)
      • N.G. Leveson . Software safety: why, what and how. Comput. Suru. , 2 , 125 - 163
    127. 127)
      • J.C. Knight , N.G. Leveson . A reply to the criticisms of the Knight & Leveson experiment. SIGSOFT Softw. Eng. Notes , 1 , 25 - 35
    128. 128)
      • R.E. Bloomfield , P.K.D. Froome , B.Q. Monahan . Formal methods in the production and assessment of safety critical software. Reliab. Eng. Syst. Saf. , 1 , 51 - 66
    129. 129)
      • A. Kandel , E. Avni . (1988) , Engineering risk and hazard assessment.
    130. 130)
      • Curzon, P.: `Of what use is a verified compiler specification?', 274, Technical Report, 1992.
    131. 131)
      • Fenton, N., Littlewood, B.: `Evaluating software engineering standards and methods', Proc. 2èmes Rencontres Qualiteé Logiciel & Eurometrics ′91, March 1991, p. 333–340.
    132. 132)
      • Rushby, J.: `Formal specification and verification of a fault-masking and transient-recovery model for digital flight control systems', SRI-CSL-91-3, Technical Report, January 1991, (also available as NASA Contractor Report 4384.).
    133. 133)
      • W. Hammer . (1972) , Handbook of system and product safety.
    134. 134)
      • Boehm, B.: `Software risk management tutorial', TRW-ACM Seminar, April 1988.
    135. 135)
      • D.L. Parnas , A.J. von Schouwen , Shu Po Kwan . Evaluation of safety-critical software. Commun. ACM , 6 , 636 - 648
    136. 136)
      • : `Safety-related systems: a professional brief for the engineers', IEE, January 1992, Savoy Place London, UK, WB2R 0BR.
    137. 137)
      • J.S. Moore . Special issue on system verification. J. Autom. Reasoning , 4 , 409 - 530
    138. 138)
      • D.P. Youll . (1988) , Study of the training and education needed in support of Def Stan 00.55.
    139. 139)
      • A.J. Cohn . The notation of proof in hardware verification. J. Autom. Reasoning , 2 , 127 - 139
    140. 140)
      • D. Mackenzie . The fangs of the VIPER. Nature , 467 - 468
    141. 141)
      • J.A. Hall . Seven myths of formal methods. IEEE Softw. , 5 , 11 - 19
    142. 142)
      • K.A. Helps . Some verification tools and methods for airborne safety-critical software. Softw. Eng. J. , 6 , 248 - 253
    143. 143)
      • Natsume, T., Hasegawa, Y.: `A view on computer systems and their reliability in Japan', SAFECOMP ′92, Computer Systems in Safety-critical Application, Proc. IFAC Symp., 28–30 October 1992, Zürich Switzerland, Pergamon Press, p. 45–49, Safety of Computer Control Systems 1992.
    144. 144)
      • (1990) , Minimum operational performance standards for traffic alert and collision avoidance system (TCAS) airborne equipment—consolidated edition.
    145. 145)
      • A.P. Ravn , V. Stavridou , D. Bjørner , H. Langmaack , C.A.R. Hoare . (1993) Project organisation, Provably correct systems. ProCos Project Report.
    146. 146)
      • J. von Neumann . (1961) Probabilistic logics and synthesis of reliable organisms form unreliable components, Collected works.
    147. 147)
      • G. Normington , J.P. Bowen , J.E. Nichols . (1993) Cleanroom and Z, Z User Workshop.
    148. 148)
      • I. Houston , S. King , S. Prehn , W.J. Toetenel . (1991) CICS project report: experiences and results from the use of Z in IBM, Formal Software Development Methods.
    149. 149)
      • Peleaz, E.: `A gift from Pandora's box: the software crisis', 1988, Ph.D. Thesis, Edinburgh University, UK.
    150. 150)
      • P.K. Joannou , J. Harauz , D.R. Tremaine , N. Ichiyen , A.B. Clark . (1991) , The Canadian nuclear industry's initiative in real-time software engineering.
    151. 151)
      • D. Swade . (1991) , Charles Babbage and his calculating engines.
    152. 152)
      • : `Functional safety of programmable electronic systems : generic aspects', Technical Committee 65, February 1992, International Electrotechnical Commission, Working Group 10 (WG10), IEC 65A (Secretariat) 123.
    153. 153)
      • R.M. Stein . Safety by formal design. BYTE , 8
    154. 154)
      • B. Littlewood , L. Strigini . The risks of software. Sci. Am. , 5 , 38 - 43
    155. 155)
      • Pasquine, A., Rizzo, A.: `Risk perception and acceptance of computers in critical applications', SAFECOMP ′92, Computer Systems in Safety-critical Application, Proc. IFAC Symp., 28–30 October 1992, Zürich Switzerland, Pergamon Press, p. 293–298, Safety of Computer Control Systems 1992.
    156. 156)
      • R.M. Stein . (1992) Software safety, Real-time multicomputer software systems.
    157. 157)
      • Hoare, C.A.R., He, J., Bowen, J.P., Pandya, P.K.: `An algebraic approach to verifiable compiling specification and prototyping of the ProCoS level 0 programming language', ESPRIT ′90 Conf. Proc., 1990, Brussels, Kluwer Academic Publishers B.V., p. 804–818.
    158. 158)
      • C.B. Jones . (1990) , Systematic software development using VDM.
    159. 159)
      • R. Malcolm , F. Redmill . (1992) Safety critical systems research programme: technical workplan for the second phase, Safety systems: the safety-critical systems club newsletter.
    160. 160)
      • Redmill, F.: `Dependability of critical computer systems 1 & 2', European Workshop on Industrial Computer Systems Technical Committee 7 (EWICS TC7), 1988/1989, London, Elsevier Applied Science.
    161. 161)
      • B.R. Ladeau , C. Freeman . Using formal specification for product development. Hewlett-Packard J. , 6 , 62 - 66
    162. 162)
      • (1991) , Safety related software for railway signalling.
    163. 163)
      • W.E. Boebert . Formal verification of embedded software. SIGSOFT Softw. Eng. Notes , 3 , 41 - 42
    164. 164)
      • Goguen, J., Winkler, T.: `Introducing OBJ3', SRI-CSL-88-9, Technical Report, August 1988.
    165. 165)
      • `Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment', 00-56, 5 April 1991, Interim Defence Standard, Issue 1, Bristol, UK.
    166. 166)
      • (1989) , Software in safety-related systems.
    167. 167)
      • C.T. Sennett . (1989) , High-integrity software.
    168. 168)
      • J.T. Webb , D. Ince . (1991) The role of verification and validation tools in the production of critical software, Software quality and reliability: tools and methods.
    169. 169)
      • M.J.C. Gordon , G. Birtwistle , P.A. Subramanyam . (1988) HOL: a proof generating system for higher-Order Logic, VLSI specification, verification and synthesis.
    170. 170)
      • I. Craig . (1991) , The formal specification of advanced Al architectures.
    171. 171)
      • Rushby, J., Whitehurst, R.A.: `Formal verification of Al software', 181227, Contractor Report, February 1989.
    172. 172)
      • L. Barroca , J. McDermid . Formal methods: use and relevance for the development of safety critical systems. Comput. J. , 6
    173. 173)
      • S. Augarten , S. Augarten . (1984) The Whirlwind project, Bit by bit: an illustrated history of computers.
    174. 174)
      • D. Clutterbuck , B.A. Carré . The verification of low-level code. Softw. Eng. J. , 3 , 97 - 111
    175. 175)
      • B. Cohen , D.H. Pitt . (1990) The identification and discharge of proof obligations, Testing large software systems.
    176. 176)
      • : `Peer review of a formal verification/design proof methodology', 2377, NASA Conf. Publ., July 1983.
    177. 177)
      • J. Palfreman , D. Swade . (1991) , The dream machine.
    178. 178)
      • Scholefield, D.J.: `The formal development of real time systems: a review', YCS 145, Technical Report, 1990.
    179. 179)
      • J.P. Bowen , P.T. Breuer , H. van Zuylen . (1992) Decompilation, The REDO compendium of reverse engineering for software maintenance.
    180. 180)
      • Jacky, J.: `Formal specifications for a clinical cyclotron control system', Proc. ACM SIGSOFT Int Workshop on Formal Methods in Software Development, 1990, 15, SIGSOFT Softw. Eng. Notes, p. 45–54, (4).
    181. 181)
      • R.L. Glass . Software vs. hardware errors. Computer , 12
http://iet.metastore.ingenta.com/content/journals/10.1049/sej.1993.0025
Loading

Related content

content/journals/10.1049/sej.1993.0025
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
Print this page
This is a required field
Please enter a valid email address