# 系统验证代写 | COM3028: Systems Veriﬁcation Coursework 2 – LSA

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

Instructions

• Answer the following questions on systems veriﬁcation. 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 trafﬁc-light system;

– the NuSMV ﬁle;

– 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 ﬁnal 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 trafﬁc 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 trafﬁc-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 trafﬁc 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-

speciﬁcationmeets these properties, usingNuSMV’s LTLmodel checking facilities. [30 marks]