• 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
• 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]
本网站支持 Alipay WeChatPay PayPal等支付方式
E-mail: email@example.com 微信号:vipnxx