PAPER CODE NO. EXAMINER: Martin Zimmermann Tel. No. 58860
COMP313 DEPARTMENT: Computer Science
SECOND SEMESTER EXAMINATIONS 2020/21
Formal Methods
Expected Writing Time : TWO HOURS
INSTRUCTIONS TO CANDIDATES
• The exam consists of TWO Sections, each with THREE questions. Answer the ALL
questions in Section A and TWO OUT OF THREE questions in Section B.
• The expected writing time for the exam is TWO hours.
• You may write your answers using a word processor (please export the document to pdf
before submitting), or you may write your answers by hand and either scan them, or take
photos of them. If you write your answers by hand, then both the handwriting and the
scanned copy must be legible in order to be accepted.
• The exam will be released at Friday 21 May, 9am. You will then have 24 hours in which to
prepare your answers, and the final deadline for submissions is Saturday 22 May, 9am.
• Submit your answers to CANVAS, via the “Assignment” tab of the COMP313 course.
• Late submissions will not be accepted.
PAPER CODE COMP313 page 1 of 6 Continued
Section A
Attempt ALL questions from this section. Section A is worth 30 marks.
1. This question concerns the basic structures used within Z specifications.
(a) Give a total surjection from the set {−1,−2,−3,−4, ...} of negative integers to the set
{1, 4, 9, 16, ...} of squares. Justify your answer. [5 marks]
2. This question concerns the foundations of LTL.
(a) Give a model of the LTL formula [5 marks]
(aU c) ∧ (b U d) ∧ (¬(c ∧ d)).
Justify your answer.
PAPER CODE COMP313 page 2 of 6 Continued
3. This question concerns the foundations of model checking.
For Parts (a), (b), and (c) consider the following Bu¨chi automaton over the alphabet IP{p, q}.
ℓ
t
b
r
¬q
q
q
q
p ∧ ¬q¬p ∧ ¬q
q
¬q
(a) Give a trace over IP {p, q} that is accepted by the Bu¨chi automaton above. Justify your
answer. [3 marks]
(b) Give a trace over IP {p, q} that is not accepted by the Bu¨chi automaton above. Justify
your answer. [3 marks]
(c) Let A be the Bu¨chi automaton above. Do we have L(A) ⊆ Models( q)? Justify your
answer. [4 marks]
(d) Give a Bu¨chi automaton accepting exactly the models of the LTL formula [4 marks]
p ∧ (p U ¬p).
Argue informally why your answer is correct.
(e) Give a Bu¨chi automaton accepting exactly the models of the LTL formula [6 marks]
( p) ∧ (q U r ).
Argue informally why your answer is correct.
PAPER CODE COMP313 page 3 of 6 Continued
Section B
Attempt TWO questions from this section. Each question is worth 20 marks. If you attempt
all three questions, the lowest mark will be discarded.
4. This question concerns specification in Z.
We want to specify a database for a delivery company assigning routes (sequences of ad-
dresses) to drivers. To this end, we have already developed the following partial state space
schema:
Assignment
active : IP DRIVERS
customers : IP ADDRESSES
route : DRIVERS $→ seq ADDRESSES
· · ·
Here, DRIVERS is a given set of drivers and active is the set of active drivers. Further,
ADDRESSES is a given set of addresses, and customers is the set of addresses of cus-
tomers. Finally, route assigns routes (sequences of addresses) to drivers.
(a) Add an invariant expressing that only active drivers have a route assigned to them.
[2 mark]
(b) Add an invariant expressing that only the addresses of customers appear in routes. Ex-
plain your answer. [3 marks]
(c) Add an invariant expressing that no address appears on the routes assigned to two
different drivers. Explain your answer. [4 marks]
(d) Write a robust schema [7 marks]
AddAddress(driver? : DRIVERS, address? : ADDRESSES, report ! : REPORTS)
that adds the address address? to the end of the route assigned to driver?. Use the
output report ! to give appropriate error messages in case this is not possible. Explain
your answer.
(e) Write a schema [4 marks]
Filter (area? : IP ADDRESSES, out ! : IP DRIVERS)
that outputs the set of drivers with routes that contain an address from area?. Explain
your answer.
PAPER CODE COMP313 page 4 of 6 Continued
5. This question concerns specification in LTL.
Below is a temporal specification for a simple message-passing system consisting of two
components, S and R.
SpecS:
!""""""""""#
¬(a ∧ b)
∧ start → a
∧ a → (aU b)
∧ b → (¬a ∧ ¬b)
∧ (¬a ∧ ¬b) → (¬a ∧ ¬b)
∧ b → snd msg
∧ ¬b → ¬snd msg
∧ rcv rcpt → z
$%%%%%%%%%%&
SpecR:
!# rcv msg → x∧ x → x
∧ x → snd rcpt
$&
(a) Explain the behavior of SpecS. In particular, how often does snd msg hold in a model of
SpecS? [6 marks]
(b) Explain why [6 marks]
SpecS ∧ SpecR ∧ (snd msg → rcv msg) ∧ (snd rcpt → rcv rcpt)
implies z.
(c) Is the LTL formula [3 marks]
ϕ = ( q) ∨ ( r )
a safety property? Justify your answer.
(d) Is the LTL formula [5 marks]
ψ = ( q) → ( (r ∧ r ))
a liveness property? Justify your answer.
PAPER CODE COMP313 page 5 of 6 Continued
6. Consider the following Promela program.
int x;
int y = 2;
init{
atomic{
run A();
run B();
}
}
proctype A(){
if
:: true -> x = y;
:: true -> x = y + 1;
fi
x = x + 1;
}
proctype B(){
if
:: x == 2 -> x = x + 4;
:: x == 3 -> x = x - 1;
:: x == 4 -> x = 5;
fi
}
(a) Construct the Bu¨chi automaton representing the behavior of the Promela program. Ex-
plain your answer. [11 marks]
(b) We modify proctype B by adding an assertion, leaving the rest of the code, i.e., init and
A, unchanged:
proctype B(){
if
:: x == 2 -> x = x + 4;
:: x == 3 -> x = x - 1;
:: x == 4 -> x = 5;
fi
assert(x <= 6);
}
Explain why the assertion is violated. [5 marks]
(c) Explain how to modify the original program to reduce the size of its state vector without
changing the behavior of the program. [4 marks]
PAPER CODE COMP313 page 6 of 6 End

欢迎咨询51作业君