Modelling Systems
Mock Examination Questions

The questions were drawn from past resit papers and mock papers used at the University of Newcastle upon Tyne from 1996 to 1998. In 1999 the course changed radically and the style of examination question changed with it. We will be posting examples of the newer questions soon. Teaching colleagues may like to note that these questions assume "closed book" style of examination whereas we ave now moved to an "open book" exam in which there is much less credit for knowing standard definitions and much more stress placed on the writing of correct specifications.

Each question should take about 45 minutes for Newcastle University students who have studied CSC208 (before Michaelmas term 1998) and CSC227 (from Michaelmas Term 1998 onwards). Naturally the level of expertise for your own students may be very different. However, we hope that it can be used as inspiration as to how exam questions can be constructed.

Each question is divided into a number of parts and for each part the relative weight of that part is given. The normal style is to begin with a piece of bookwork (definition, comparison of concepts) that relates to the main subject of the question. The central parts of the question involve writing or modifying some VDM-SL. The last part of each question is called the "sting in the tail" and is intended to give the better students an opportunity to show deeper understanding.

Question 1
Part 1

It has been suggested that many of the benefits of formal methods can be gained by applying them in the early stages of the software development process. Describe the structure of a typical software development process, identifying the main phases and their products.

Describe the characteristics of a formal specification. What are their advantages of using such a specification during the system specification phase of software  development?

Part 2

Read the following informal requirements for a computing system to help police identify stolen vehicles. Then anaswer the questions following. Provide the outline of a VDM-SL specification for the system described above. You need only give type definitions, the state definition, and the headers of operation specifications.

Part 3

Describe any two cases of ambiguity, incompleteness or excess implementation detail in the requirements which you would wish to resolve with the customer before your specification could be completed.

Question 2
Part 1

Describe the differences between explicit and implicit specification styles in VDM-SL.

Part 2

An airline is introducing a new computing system for allocating seats to passengers when the passengers arrive at the airport. The rest of this question concerns the formal specification of the system.

Each seat on a flight has a seat number, a position (either by a window, by the aisle, or in the middle) and a passenger name (a character string). Define a composite type Seat to represent seats. How do you represent a seat that is not allocated to a passenger?

Part 3

For the purposes of this system, a flight is a collection of seats with no two distonct seats on the flight having thr same seat number. Define a type Flight, with an invariant, which records this requirement.

Give an explicit definition of a function free_seats which, given a flight, f, returns the set of unallocated seats in f.

The passenger will be asked which seat position (aisle, window or middle) they prefer. They will be allocated a seat which matches their preference, provided one is available. Give an implicit specification of a function good_seat which, given a flight f and a preferred position p, returns an unallocated seat in f with the preferred position.

Does your specification of  good_seat deal with the possibility that there may be no unalloctaed seats in the preferred position? If so, describe how you deal with this possibility. If not, provide a modified version of good_seat which does deal with his case, and explain how it works.

Question 3
Part 1

Briefly contrast explicit and implicit styles of specifications for functions in VDM-SL.

Part 2

A hospital uses a computer-based system to send ambulances to incident scenes. The system maintains lists of requests for ambulances. A request consists of a description of the incident (a character string) and a fild indicating the level of urgency of the request: a request may be non-urgent, urgent or emergency.

Give VDM-SL definitions of data types Request and List to represent requets and lists of requests respectively.

Define a function with the following signature which adds a request to the tail end of a list, returning the updated list.

add_request : List * Request  ->  List

Part 3

Give an explicit definition of a function called first_emergency whcih, given a list, returns the first emergency request in the list and returns nil if no such
request is present in the list. (Note: the "first" emergency request is the one closest to the head end of the list.)

Part 4

Give an implicit specification of  first_emergency.

Question 4
Part 1

What is meant by the term partial operator in a formal specification language? Illustrate your answer with one example of a partial operator and one example of a total operator on sequences in VDM-SL. Give the signatures of both example operators and explain why the partial operator is partial.

Part 2

The rest of this question concerns the formal specification of part of the software controlling a chemical processing plant. The plant is divided into streams. Each stream is a sequence of reactors. Each reactor has a set of batches of chemicals currently in the reactor and a maximum number of batches allowed in the reactor at any time. Each batch has an identifier and contents type. The representations of identifiers and contents types are immaterial. Using VDM-SL, define:
  1.  a type Stream to represent streams;
  2. a type Reactor to represent reactors;
  3. a type BatchId to represent batch identifiers; and
  4. a type Batch to represent batches.

Part 3

Define a total function with the following signature whcih returns the set of batches in a given stream:

Part 4

Define an invariant on Stream expressing the following requirements formally:
 
  1. No two batches in the stream have the same identifier.
  2. No batch occurs in more than one reactor in the stream.
  3. No reactor has more batches than its maximum.

Part 5

The specifier considers defining a function move with the following signature: Given a batch identifier and stream, the function will update the stream by moving the identified batch from its current reactor to the next one in the stream. Would you expect move to be partial?
Explain your answer.

Question 5
Part 1

Contrast the terms explicit and implicit specification as they apply to function definitions in VDM-SL.

Part 2

In the remainder of this question consider the following scenario:
    A computing system is to be developed to control the placement of containers of hazardous waste in a storage building. Each container has a unique identifier which is recorded along with an indication of the class of waste (high-level or low-level) stored in the container.
    A formal specification of the system is under development. The enumerated type WasteClass models the two classes of waste, while the composite type Container models containers:
     types

      WasteClass = <HIGH> | <LOW>;

      Container :: cid  : token
                   class: WasteClass;

    The store consists of a three-dimensional array of storage locations. Each location is modelled by an x-coordinate, a y-coordinate and a z-coordinate, giving a location's position with respect to an origin (0,0,0). The array is 10 locations long in the x and y directions and 5 locations long in the z direction.

    The composite type Location models locations. The type Store is defined to model the overall store. It maps locations to the containers stored at each location:

      Location :: x : nat
                  y : nat
                  z : nat
      inv l == x >= 0 and x <= 10 and
               y >= 0 and y <= 10 and
               z >= 0 and z <= 5;

      Store = map Location to [Container]

Why has the optional type [Container]been used?

Part 3

Define an invariant for Store which records the restrictions that no two containers in the store have the same identifier and that no two locations hold the same container.

Part 4

Assume you are given the a function adjacent, with the following signature, which returns the true if and only if its first two arguments are adjacent locations in the third argument (a store).
      adjacent : Location * Location * Store -> bool
A store is said to be safe if the following conditions are satisfied:
  1. No containers containing high-level waste are located around the outside of the store (i.e. in locations which have x-coordinate 0 or 10, or y-coordinate 0 or 10 or z-coordinate 0 or 5).
  2. No two containers of high-level waste are in adjacent locations.
Define a Boolean function safe_store which returns true if and only if the store is safe. Add a conjunct to the invariant on Store which records this constraint.

Part 5

Give an explicit definition of a function add_to_store which, given a container, a store and a location in the store, returns the updated store with the container placed at that location. Include a pre-condition to ensure that the resulting store will not break the invariant on Store.

Part 6

Sketch an implicit version of add_to_store which, given a container and a store, returns the updated store. You need
not give a full formal definition, but indicate how you would deal with the fact that you are not given a location at which the container should be placed.
 

Question 6

The following passage is an extract from a report written by a software engineer working for a company which recently
won the contract to supply a monitoring system for air traffic control. Read the passage carefully and answer EITHER
part 1 OR part 2.

We have been asked to develop a monitoring system for tracking air traffic. The system maintains a record of the structure
of the air space in a certain area, the flight plans of aircraft passing through the area and the progress of aircraft through
their planned flights.

The system has to be developed to a high level of integrity and a formal model of the system is to be constructed in order
to permit analysis of the safety requirements at an early stage in development through the validation process.

The airspace is divided into regions. Regions are linked together, so that aircraft pass from one region to another. The
following diagram shows an area consisting of 7 regions labelled 1-7. Aircraft travel through the area in one direction (from
left to right) and aircraft in a given region may only travel into a region to the right of the current one.

                   

Areas are labelled by numbers. In VDM-SL:

   RId = nat1

Each link is modelled as a pair of region identifiers. Aircraft using a link pass from the "from" region to the "to" region:

   Link :: fromlink : RId
           tolink   : RId

An area is modelled as a set of links. For example, the following set models the area shown in the figure above:

   {mk_Link(1,3), mk_Link(1,4), mk_Link(2,4), mk_Link(2,5),
    mk_Link(3,6), mk_Link(4,5), mk_Link(4,6), mk_Link(5,7),
    mk_Link(6,7)}

A flight plan is a sequence of regions through which an aircraft will fly. Flight plans are modelled as sequences of region
identifiers. For example, the plan [2,4,5,7] is a possible plan for aircraft flying through the area shown above. The
position of an aircraft, i.e. how far it has progressed through its plan is given as a natural number, i.e. the index of its current
section within its flight plan. In the plan shown above, position 2 would indicate that the aircraft is in region 4.

The plan and position of an aircraft is combined into a flight record:

   FlightRecord :: plan     : seq of RId
                   position : nat1
   inv mk_FlightRecord(plan, position) ==
          position in set inds plan;

Flights are identified by flight identifiers:

   Fid = token;

The system is modelled as a composite object containing the area and the flight records:

   ATCSystem :: area    : set of Link
                flights : map FId to FlightRecord;

In an ATCSystem sys, the current region of a flight identified by identifier f is given by the expression.

   sys.flights(f).plan(sys.flights(f).position)

Functions have been defined to add and remove flights from the system. The function which moves a flight forard one step
in its plan is shown below:

   move: ATCSystem * FId -> ATCSystem
   move(sys,f) ==
    mk_System(sys.area,
              sys.flights ++ {f |->
                              mk_FlightRecord(sys.flights(f).plan,
                                              sys.flights(f).position + 1)
                             }
             )
   pre f in set dom sys.flights and
       sys.flights(f).position <> len sys.flights(f).position

Part 1

Answer ALL parts(a-d) of this question
 
  1. The report refers to "the validation process" as an activity through which the safety requirements for the modelled system will be analysed. Briefly explain what is meant by "validation" of VDM-SL specifications. Include an explanation of proof obligations and validation conjectures.
  2. A flight plan is said to be feasible in a given system if it only involves the use of links in the space component of the system. In the example above, the plan [1,4,5,7] is feasible because it uses links in the space. The plan [2,4,3,6] is not feasible because there is no link from region 4 to region 3.

    3. Define a Boolean function which, given a set of links and a plan, returns true if and only if the plan is viable in the set of links. Write comments to explain how your function works.
  3. Define a function which adds a new aircraft to an ATCSystem, given the flight identifier and its flight plan. The function should place the new aircraft in the first region of its flight plan. Remember to ensure that the aircraft identifier is unique and that the plan is viable.
  4. Define a function which, given the identifier of a starting region and the identifier of a finishing region, returns a viable route from the starting region to the ending region. Your function should return a special error value if no viable route exists.

Part 2

Answer ALL parts (a-e) of this question.
 
  1. Briefly explain the purpose of preconditions in function definitions in VDM-SL. Illustrate your answer by describing the meaning of the precondition on the function move defined in the report.
  2. Define a function which, given an ATCSystem and a region identifer, returns the set of flight identifiers for aircraft currently in the given region. Explain how your frunction works.
  3. Current air traffic control regulations require that no more than ten aircraft should be any region at any time. Add an invariant which ensures that this condition is respected in the system.

    4. Show how you would modify the definition of the function move, given in the report above, so that it is satisfiable in the presence of the invariant introduced in part (c) above.
  4. Suppose that air traffic control regulations are modified so that a new safety regulation is introduced. For each region, the total number of airdraft within that region and all of the regions ahead of it must be less than 40. Give the signature of a function ahead which, given an ATCSystem and the identifier of a region, returns the set of identifiers of regions ahead of the given region. Note that the body of the function is not required.

    5. Define a function safe which, given an ATCSystem, returns true if and only if it satisfies the new safety constraint.
  5. The system is said to be deadlocked if it is not possible to move any aircraft forward through its flight plan without violating the safety policy described in part (d) above. Define a function which checks a system for deadlock
John.Fitzgerald@ncl.ac.uk 6 June 1999 ...