系统验证代写 | COM3028: Systems Verification Coursework 2 – LSA

本次英国代写主要为系统验证相关的assignment

Instructions

• Answer the following questions on systems verification. Write clearly, motivating your an-
swers mathematically as was done during the lectures and tutorials. You are not required to
typeset your answers in LaTeX or Word. However, please take care that handwritten answers
are readable; if they are not, then your solution cannot be marked. The submission is electronic
via SurreyLearn.

• W.r.t. the NuSMV part, the submission should include:
– a print out of both of your NuSMV model for the traffic-light system;
– the NuSMV file;
– statistics about each of your SMV model (e.g., the number of reachable states, the number
of Boolean variables required, etc.);
– a counterexample for any formula which is not valid in your model.

• There is 2 questions in total.

• The coursework will count towards 50% of your final grade.

1. Consider the formula ‘ = (x1 ^ x2) _ (y1)

(a) calculate the BDT (binary decision tree) for ‘ [2 marks]

(b) calculate the ROBDD (reduced ordered binary decision diagram) for ‘ under the ordering
[x1; x2; y1] [10 marks]

(c) calculate the ROBDD (reduced ordered binary decision diagram) for ‘ under the ordering
[x1; y1; x2] [10 marks]

(d) discuss how different orderings may impact the resulting ROBDD size. [8 marks]

For Parts (b) and (c), you should show at each stage which rule (C1–C3) you are applying to
minimise the decision diagram and each intermediate decision diagram.

2. In the UK, most traffic lights progress from red (meaning stop), to red-amber (meaning prepare
to go), to green (meaning go), to amber (meaning prepare to stop), back to red. [Total: 70 marks]

(a) Model this traffic-light system in NuSMV, using the SMV modelling language. Argue
why your formal model correctly captures the scenario described above, and describe the
assumptions made when modelling the traffic lights in NuSMV, if any. [40 marks]

(b) Translate two of the natural-language properties holding on your model into LTL (which
can be even the transitions between stop-prepareToGo-go-stop), and showthat your system-
specificationmeets these properties, usingNuSMV’s LTLmodel checking facilities. [30 marks]