CM604 -- Examinable Reading List

The readings in this list are required, in the sense that the examiners will expect that you have read them and may test your understanding in the examination.

Please feel free to engage your tutors in conversation about any of the issues raised in these readings.

• [DAC99] Patterns for Property Specification in Finite State Verification

  Correctly capturing a requirement in temporal logic is often trickier than you'd think. One useful approach to the problem is to base your specifications on typical 'patterns' of expression. This paper was one of the first to develop extensively such an approach.

• [HOL01] Economics of Software Verification

  Gerard Holzmann is the inventor of the SPIN model checker and has worked for more than 20 years in the field of hardware and software verification. His recent paper on the economics of software verification gives a valuable insight into the reasons why formal approaches to system specification and design are increasingly recognised as worthwhile. Read this paper and make brief notes on the economic justification for the application of software verification techniques.

• [LEV95] Medical Devices: Therac 25

  THERAC 25 was a computer-controlled radiation therapy machine that massively overdosed six people between June 1985 and January 1987. The attached paper appears as an appendix in the book Safeware: System Safety and Computers by Nancy Leveson, Addison Wesley, 1995. The paper offers many lessons to the developers of embedded systems. Read the paper and make brief notes on the main principles of embedded systems specification and design that are highlighted by the shortcomings in the design and analysis of the THERAC 25 system. Note 1 A simpler statement of the basic facts appears here. A quicker, but probably less rewarding, approach would be to read this in conjunction with section 4 on Causal Factors in the main paper. Note 2 This case study will be used also in the module CM601 Applied Professionalism and Management.

• [RUS95] Formal Methods and their Role in the Certification of Critical Systems

  Rushby, J., Technical Report CSL-95-1, Computer Science Laboratory, SRI International, 1995 Very little technical detail (and what there is can be skimmed) but a good review of what we mean by 'formal methods' and how they can be incorporated into projects in the 'real world'.

• [SAC03] From Natural Language Requirements to Rigorous Property Specifications

  This paper attempts to make the work on specification patterns even more accessible to the practising system engineer.

• [STA95] Standish Report - CHAOS - 1995

  A survey of software successes and failures and an analysis of the causes of each. Published by the Standish Group and reproduced on the SPIN web site.