UNIVERSITY OF EDINBURGH

FACULTY OF SCIENCE AND ENGINEERING

COMPUTER SCIENCE THREE

PROGRAMMING METHODOLOGY

Wednesday 30 May 2001 14:00 to 15:30

Examiners: K. Turner (External) G. Plotkin (Chairman)

INSTRUCTIONS TO CANDIDATES

Answer any TWO questions. All questions carry equal weight.

1. Following a number of fatal accidents caused by car airbags inflating without a collision having occurred, your firm is developing a new ultra-reliable airbag release system. Five pairs of sensors will be deployed in various parts of the car, registering impact, abrupt changes of momentum, etc. In each pair of sensors, the outputs will be compared with each other, with disagreement causing the output of both to be vetoed until a reset button is pressed. The airbag will be released only if at least two non-vetoed sensor pairs are triggered simultaneously.

The airbag release system is modelled by the following signature:

     signature RELEASE =
       sig
         type sensors
         val mksensors : bool * ... * bool -> sensors  (* one input per sensor *)
         type state
         val init : state
         val readsensors : sensors * state -> state
         val isvetoed : int * state -> bool
         val resetveto : int * state -> state
         val release : state -> bool
       end

The state of the system incorporates the current state of each sensor, whether or not a pair of sensors has been vetoed (isvetoed(n,s)=true means that sensor pair n is vetoed) and the state of the airbag (release(s)=true means that the airbag will be released). The mksensors function models the values of the sensors; in the actual system, the values are not inputs but are supplied by the sensors themselves. The resetveto function causes the veto on a given pair of sensors, if any, to be cancelled.

(a) Explain the difference between verification and validation, and between static and dynamic methods. What is stress testing? [5 marks ]

(b) Describe two methods for dynamic verification of this system and highlight the differences between them. Give an example test set and justify your choice of tests. [15 marks ]

(c) Describe one technique for static verification and indicate what information you would require to apply the technique to this system. [5 marks ] 2. (a) You are revising for an exam. Reading, thinking, understanding and the

state of your brain before you begin revising are modelled by the following signature:

    signature REVISING =
      sig
        eqtype note
        type brain
        val read : note * brain -> brain
        val think : brain -> brain
        val understand : note * brain -> bool
        val start : brain
      end

In order to understand a lecture note, you need to read it and then think. If you read two lecture notes in a row without thinking in between, the first one is forgotten. Understanding of a lecture note, once attained, is a permanent state. When you start revising, you understand nothing. Provide axioms that formalise this informal description. [10 marks ]

(b) A higher-level view of the same process is provided by the following signature:

    signature REVISING' =
      sig
        eqtype note
        type brain
        val learn : note * brain -> brain
        val understand : note * brain -> bool
        val start : brain
        axiom not understand(n,start)
        axiom understand(n,learn(n,b))
        axiom n<>m implies understand(n,learn(m,b)) = understand(n,b)
      end

Consider the problem of implementing REVISING' in terms of a structure matching REVISING. Express this as an EML functor. Don’t give the body yet. [2 marks ]

(c) Suggest a refinement step that provides an SML implementation of this functor. [3 marks ]

(d) Say what the proof obligations are for that refinement step: what do you have to prove, and what assumptions are you allowed to use? [3 marks ]

(e) Give proofs of these proof obligations. [7 marks ] 3. You are developing an integrated software system for managing all aspects of a

medical practice. It will store patient records, help doctors to select treatment via access to a database of drugs, print prescriptions, keep track of appointments, and play music in the waiting room chosen to suit the age profile of its current occupants. It will also handle all financial aspects of the business including ordering supplies and keeping track of inventory, and processing salaries and taxes for staff. In future, when advances in genetics permit, it will be expanded to store each patient’s DNA sequence; then the assistance it provides with the choice of treatment will take the patient’s genetic makeup into account.

(a) Identify at least three different classes of users of the system and give a brief summary of the needs of each class. [5 marks ]

(b) Choose one of the classes of users you outlined above and describe a set of functions that would meet their needs. [4 marks ]

(c) Choose one of the functions you have described and provide a detailed specification of this function. [5 marks ]

(d) What attributes do you think would be important in the requirements specification of this system? Justify your choice and suggest appropriate measures of these attributes. [4 marks ]

(e) You need to select a lifecycle model to use. Outline two lifecycle models and compare their suitability for developing this system. [7 marks ]