代写Programming留学生编程、代做c++，Python程序设计

日期：2021-03-02 11:09

Programming Assignment I: CTL Model Checking + NuSMV

Due-date: Mar 15 at 11:59PM (via Canvas). If you submit by Mar 12 at 11:59PM, you can earn

20% extra credit. Submissions after the deadline will not be graded unless explicit prior permission

is granted.

Homework must be individual’s original work. Collaborations of any form with any students (except

our TA) or other faculty members are not allowed. If you have any questions/doubts/concerns, post

your questions/doubts/concerns on Piazza and/or directly ask our TA or me.

Learning Outcomes.

1. Ability to encode design specification in NuSMV.

2. Ability to abstract specification details that are irrelevant in the context of verification of

desirable properties/requirements.

3. Ability to apply formal methods (interpret model checking results, apply/encode temporal

logic).

1 Problem 1: Verification

1.1 Specification

A train is controlled by a driver using two levers: a motion-lever and a door-lever. The driver can

control the speed of the train using the motion-lever with the signals: accelerate, break. Similarly

the doors of the train are controlled using the door-lever using the signals: open, close.

The states of the train are as follows:

? stopped: when its speed is 0 kmph.

? accelerating: when the speed goes up till it reaches 100 kmph.

? steady: when the speed of the train remains at 100 kmph.

? decelerating: when the speed goes down till it reaches 0 kmph.

The specification of the train movement is described as follows:

? if the train is stopped, the doors are closed and the driver accelerates, then the train goes to

the accelerating state.

? If the train is accelerating and

– the driver breaks, then the train goes to the decelerating state

– the driver does nothing or accelerates, the train keeps accelerating till it reaches steady

state.

? If the train is decelerating and

1

– the driver accelerates, then the train starts accelerating

– the driver does nothing or breaks, then the train keeps decelerating till it reaches stopped

state.

? If the train is in steady state and

– the driver breaks, then the train starts decelerating

– the driver does nothing or accelerates, then the train remains in steady state.

The doors of the train can be in the following states: open, opening, closing and closed. The

specification of the door functionality is described as follows:

? If the doors are closed, the train is not moving and the driver sends open signal via the

door-lever, then the doors go to opening state.

? If the doors are opening and

– the driver sends close signal, then the doors go to closing state

– the driver does nothing, then the doors go to open state.

? If the doors are closing and

– the driver sends open signal, then the doors go to opening state

– the driver does nothing, then the doors go to closed state.

? If the door is open and the driver sends a close signal, then the doors go to closing state.

1.2 To Do

Use SMV model checker to prove/disprove that the doors are always closed unless the train is

stopped.

1.3 To Submit

1. Submit one file: PA1-P1-hyour-net-idi.txt. It should contain the encoding of the specification

and the CTL property that you used to prove/disprove the above property.

2. At the top of the file, in comments, write the result of your verification. If verification result

is true, then write the following:

-- Property is proved to be satisfied

If verification result is false, then write the following:

-- Property is proved to be violated

followed by multiple comment lines, where you will need to explain why the property is

violated. That, what sequence of events as per the specification leads to the violation of the

property. Do not simply copy-paste the counter-example generated by NuSMV, rather interpret

the counter-example.

2

2 Problem 2: Planning

2.1 Specification

Fett sisters Xoba, Yoba and Zoba are accompanying three padawans (student or learner) to planet

Tatooine. Each sister is responsible for taking care of her padawan. The Fetts do not trust each

other and as a result, none of the sisters can leave her padawan with any one of the other sisters

(for example, if Xoba leaves her padawan unattended with either Yoba or Zoba or both, then Xoba’s

padawan may be in mortal danger - grim situation it is).

On their way to Tatooine, the Fetts and their padawans need to move through hyperspace

between two deserted planets: Isi and Iju. They have been able to “get” one lightspeed vessel,

which can take them from planet Isi to planet Iju. Unfortunately, the vessel is a two-person vessel

(for example, at a time two sisters or one sister and one padawan or two padawans can use the

vessel). To further complicate the situation, the vessel is not equipped with Alset auto-drive, which

implies someone needs to drive it. The Fetts (and padawans) need to strategize a way to use the

vessel multiple times such that they can all safely escort their padawans from Isi to Iju.

2.2 To do

Model all possible movements between the planets and use a “safety” property to verify whether

there exists a plan (sequence of movements) that will enable the Fett sisters to take their respective

padawans from Isi to Iju.

2.3 To Submit

1. Submit one file: PA1-P2-hyour-net-idi.txt. It should contain your encoding along with the

property you used. (Follow the same technique as the farmer-goat-wolf-cabbage problem

discussed).

2. At the top of the file, in comments, write the result of your finding. If there is no plan, then

write

-- No plan exists.

and explain why (also in comments). If there is a plan, then write the steps in the plan as

part of the comments.

3 Subscript

Before you start with this assignment, you will need to (a) download NuSMV, (b) get familiar

with how NuSMV works and (c) know how to encode in NuSMV and interpret its outputs. Late

start and/or commencing with the assignment without completing these tasks may result is less than

satisfactory score for this assignment.

3