Modelling Systems: Practical Tools and Techniques for Software Development

Modelling Systems
Mock Exam Questions
Specimen Answers

Introduction

These answers are only specimens. At some points I have indicated acceptable alternatives, but remember that there may be many more than we are able to show here.

Answer 1
Part 1

The start of this question carries more marks than is usual. This implies that a reasonable amount of detail is expected in answers. I would be looking for the following points:

An idealised software development process has the following principal phases, usually carried out in the order shown:

Requirements analysis phase:

produces a customer requirement,
customer requirement written in natural language,
customer requirement describes the system to be built using the vocabulary of the customer's domain.
typically ambiguous, incomplete and contradictory.

System Specification phase:

working from the customer requirement, produces a system specification
system specification describes system to be built using systems developer's terms
system specification in natural language.
may describe data, functionality, implementation restrictions or constrain performance

System Design phase:

produces description of system architecture

Software Design phase:

software design defines the computations performed by individual modules

Software implementation phase:

produces code accurately implementing modules in system design

A formal specification is typically:

abstract (the specification describes what the system must do not how it should be achieved),
formal (the notation used has a well-defined semantics),
open to analysis (can test a formal specification and conduct proofs of its properties, e.g. emergent safety properties).

Advantages of using a formal specification during the system specification phase are:

The developed specification is less open to argument as a result of ambiguity and incompleteness;
ambiguity and incompleteness in the customer requirements can be resolved during production of the formal spec.; and
the cost of error resolution at the system specification stage is lower than in later stages.

Part 2

The police vehicle database:

types

VehicleDetails :: model : token
colour : token;

RegNo = seq of char
inv r == len r = 6 and
(forall i in set {1,...,3} & r(i) in set {'a',...,'Z'}) and
(forall i in set {4,...,6} & r(i) in set {'0',...,'9'})

state Database of
vhs : map RegNo to VehicleDetails
end

operations

LookUp(r:RegNo)d:[VehicleDetails]
ext rd vhs : map RegNo to VehicleDetails
...

AddCar(r:RegNo, d:VehicleDetails)
ext wr vhs : map RegNo to VehicleDetails
...

DelCar(r:RegNo)
ext wr vhs : map RegNo to VehicleDetails
...

Match(m:token,c:token) ms:set of RegNo
ext rd vhs : map RegNo to VehicleDetails
...

Part 3

[Plenty of alternative answers here - just some are listed]

Ambiguity: sometimes the requirements refer to vehicles and sometimes to cars. Is there a difference? There are references both to users and police officers. Again is there a difference to be modelled?
Incompleteness: we can "guess" that details include colour and model, but is there anything else required?
Excess Detail: the structure of registration numbers does not appear to be used.

Answer 2
Part 1

The terms explicit and implicit relate to function definitions in VDM-SL specifications. A function

f : T1 * T2 * ... * Tn -> R

is explicitly specified if it is defined in terms of an expression over the inputs which, given any input satisfying the function's
precondition (if any), evaluates to a single result of the result type R. An implicit specification of the same function would be defined by means of a post-condition characterising the result in terms of the inputs, and not necessarily defining a unique output. Implicit specifications, in general, admit more implementations than explicit specifications unless let-be expressions are used.

Part 2

types

Position = <AISLE> | <WINDOW> | <MIDDLE>;

   Seat :: num : nat
           pos : Position
           pass: seq of char

If a seat is not allocated to a passenger, the pass field will be the empty string [] (also written as "").

[You could also choose to make the pass field optional and represent the absence of a passenger by the value nil.]

Part 3

types

Flight = set of Seat
inv f == not exists s1, s2 in set f & s1 <> s2 and s1.num = s2.num

functions

free_seats : Flight -> set of Seat
free_seats(f) == {s | s in set f & s.pass = []};

   good_seat(f:Flight, p:Position)r:Seat
   pre exists s in set f & s.pass = [] and s.pos = p
   post r in set f and r.pass = [] and r.pos = p

This definition of good-seat has a precondition recording an assumption that there exists a free seat in f which has the desired position. The function may not be called when such a seat does not exist.

[An alternative is to return an error value or nil in the case where no suitable seat can be found:

   good_seat(f:Flight, p:Position)r:[Seat]
   post if exists s in set f & s.pass = [] and s.pos = p
        then r in set f and r.pass = [] and r.pos = p
        else r = nil

]

Answer 3
Part 1

Consider a function f having signature

f : T1 * T2 * ... -> T

f is said to be explicitly specified if it is defined by means of a value expression of type T such that for any
input satisfying the precondition of f (if present), the value expression denotes a unique value. f is said to be implicitly
specified if it is defined by means of a logical expression (a post-condition) such that for any input satisfying the precondition of f (if present), the logical expression evaluates to true for those values which are acceptable results. Unlike an explicitly defined function, an implicitly defined one may leave a wide range of implementations open. For example, an implicit specification of a function to calculate the square root of a number may leave it unspecified whether the result is to be the positive root or the negative.

Part 2

types

Request :: description : seq of char
urgency : <non_urgent> | <urgent> | <emergency>;

List = seq of Request

functions

add_request : List * Request -> List
add_request(l,r) == l ^ [r];

Part 3

   first_emergency : List -> [Request]
   first_emergency(l) == if l = []
                         then nil
                         else first_emergency(tl l)

Part 4

An implicit specification of first-emergency would be defined by a post-condition giving the properties of the result. I want to say that if there is an emergency request in the list, then the result is such a request and it is the first such request; otherwise, the result is nil. Formalising the parts of this: first, to say that there is an emergency in the list:

exists i in set inds l & l(i).urgency = <emergency>

Then to say that the result is the earliest such request:

   exists i in set inds l &
             l(i).urgency = <emergency> and
             l(i) = r and
             forall j in set inds l & j<i => l(j).urgency <> <emergency>

Putting these together:

first_emergency(l:List)r : [Request]

   post If exists i in set inds l & l(i).urgency = <emergency>
        then exists i in set inds l &
                    l(i).urgency = <emergency> and
                    l(i) = r and
                    forall j in set inds l & j<i => l(j).urgency <> <emergency>
        else r = nil

[ I put all the text at the start of the answer to this last part to emphasise that you can still get marks for writing about the specification, even if you haven't got time to work out all the details. Of course, you don't have to write all the text, but you have a better chance of being understood than if you just submit a page of (possibly wrong) maths. Notice that the last part, although hard, doesn't add many marks to your total.
]

Answer 4
Part 1

Partial operators: An operator

op : A1 * A2 * ... * An -> B

is said to be partial if there is some a in A1 * A2 * ... * An such that op(a) is undefined.

For example, the head operator on sequences has the following signature:

hd : seq of A -> A

where A is some type. This operator is partial because it is undefined when applied to the empty sequence [].

The sequence concatenation operator, which has the following signature:

_^_ : seq of A * seq of A -> seq of A

where A is some type, is total, i.e. is defined for all possible sequences.

Part 2

types

Stream = seq of Reactor;

Reactor :: batches : set of Batch
limit : nat;

BatchId = token;

Batch :: batch_id : BatchId
contents_type : token

Part 3

functions

   batches_in_stream : Stream -> set of Batch
   batches_in_stream(s) ==
      dunion {r.batches | r : Reactor & r in set elems s }

[Alternative: use inds rather than elems:

   batches_in_stream : Stream -> set of Batch
   batches_in_stream(s) ==
      dunion {s(i).batches | i in set inds s }

Another alternative: don't use distributed union, just forming the set directly:

   batches_in_stream : Stream -> set of Batch
   batches_in_stream(s) ==
      { b | b:Batch & exists i in set inds s & b in set s(i).batches }
]

Part 4

types

Stream = seq of Reactor;
inv b == not (exists b1,b2 in set batches_in_stream(s) &
b1 <> b2 and b1.batch_id = b2.batch_id) and

           not (exists i,j in set inds s &
                         i <> j and
                         s(i).batches inter s(j).batches <> {}) and

forall i in set inds s & card s(i).batches <= s(i)

Part 5

Move would be partial. There are a number of reasons why it would be partial - any one will do:

The given batch identifier might not be in the stream.
There might not be capacity in the destination reactor to permit the vessel to be accepted.

Answer 5
Part 1

Consider a function f having signature

f : T1 * T2 * ... -> T

Part 2

The optional type admits the special value nil, indicating the absence of a container for that location, i.e. the location is empty.

Part 3

types

Store = map Location to [Container]
inv s == not (exists c1,c2 in set rng s &
                  c1 <> nil and c2 <> nil and
                  c1<>c2 and c1.cid = c2.cid)
             and
             not (exists l1, l2 in set dom s &
                  s(l1) <> nil and s(l2) <> nil and
                  l1 <> l2 and s(l1) = s(l2))

Part 4

functions

   safe_store : Store -> bool
   safe_store(s) == (not exists l in set dom s &
                       (l.x = 0 or l.x = 10 or
                        l.y = 0 or l.y = 10 or
                        l.z = 0 or l.z = 5) and
                       s(l) <> nil and s(l).class = <HIGH>)
                    and
                    (not exists l1, l2 in set dom s &
                       adjacent(l1,l2,s) and l1 <> l2 and
                       s(l1) <> nil and s(l2) <> nil and
                       and s(l1).class = <HIGH> and s(l2).class = <HIGH>
                       and adjacent(l1,l2,s);

The addition to the invariant is just

... and safe-store(s)

Part 5

add_to_store : Container * Store * Location -> Store
add_to_store(c,s,loc) ==
s ++ { loc |-> c }
pre not (exists c1 in set rng s & c1.cid = c.cid) and
safe-store(s ++ { loc |-> c });

Part 6

add-to-store(c:Container, s:Store) r:Store
pre
post

The absence of an input location means that the postcondition should assert simply that there exists such a location, e.g.

post exists loc in set dom s & r = s ++ { loc |-> c }

However, the postcondition might now allow the invariant to be broken, because it does not constrain the choice of loc to one which respects the invariant, so additional conjuncts would have to be added here. The pre-condition would change similarly:

pre not exists c1 in set rng s & c1.cid = c.cid and
exists loc in set dom s & safe-store(s ++ { loc |-> c })

Answer 6
Part 1

Not yet available

Part 2

Not yet available

John.Fitzgerald@ncl.ac.uk

6 June 1999 ...

Introduction

Answer 1 Part 1

Part 2

Part 3

Answer 2 Part 1

Part 2

Part 3

Answer 3 Part 1

Part 2

Part 3

Part 4

Answer 4 Part 1

Part 2

Part 3

Part 4

Part 5

Answer 5 Part 1

Part 2

Part 3

Part 4

Part 5

Part 6

Answer 6 Part 1

Part 2

Answer 1
Part 1

Answer 2
Part 1

Answer 3
Part 1

Answer 4
Part 1

Answer 5
Part 1

Answer 6
Part 1