Finite State Machines and Kripke Structures
Networks of Finite State Machines
Temporal Logics, CTL
Finite State Model Checking
JPK chapter 3: sections 3.0, 3.1, 3.2, 3.4, 3.6, 3.8 (you may skip pp 155-156, 162-164).The alternative algorithm mentioned on page 171 by Clarke, Emerson and Sistla for checking EG (and EU) formulae can be found here.
Finish Exercise 1 from last time (Lecture 1).Exercise 2 (Modeling)
In this exercise you are to model, validate and verify a simple data link protocol, where some unrealistic assumptions will be made in order to keep the exercise simple.
The protocol specification is as follows: there are a Sender, a Receiver and a Medium. The medium can after reception of a message from the sender, do one of two things: either the message is delivered to the receiver, or it is lost. The loss of a message should be modeled by an internal transition (unlabelled transition in UPPAAL), since the loss itself does not constitute an observable event. When a message is lost a time-out in the sender will occur - model this time-out as a communication signal sent from the medium (in case of message loss) to the sender. In case of a time-out, the sender will retransmit the message. When the receiver gets a message an acknowledgment is sent to the sender. Assume that the acknowledgment is sent directly to the sender and not through any medium.
Task 1: Model the above protocol in UPPAAL, and validate using the simulator that it is functionally correct.
Redefine the protocol by modifying the receiver so that it reports to the layer above when a message is receive. Add a test process (to model the above layer) that receives the messages from the receiver. Modify the sender to receive messages from the layer above. Add another test process that generates messages to the sender (modeling the above layer).
Task 2: Validate that the functionality of the refined protocol is correct using the simulator.
Now modify the test environment so that the test sender increments a shared integer variable i whenever a message is sent. Modify the test receiver so that it decrements the variable i whenever a message is received.
Task 3: Validate the protocol and verify that the value of the variable i is always one or zero.
Task 4: What happens if the protocol is redefined in the following way: acknowledgments are not sent at all from the receiver to the sender? What happens if additionally the sender never expects acknowledgments? Validate, verify and describe in words the behavior of the resulting protocol.
Model the content of messages as (bounded) integer values and change the models of the protocol and the test environment consequently.
Task 5: Validate and afterwards verify, that the content of a message when sent equals the content of the message when received.
Exercise 3 (Theory)
JPK exercises 17, 18, 22.