Tutorial 9: Formal Verification by Model Checking

Getting Started with UPPAAL

Download UPPAAL

1. Download the UPPAAL executable and jar from here. You will need to fill in some personal information (Name, Job title, University, E-mail). You must also accept the license agreement and the privacy policy.
2. Unzip the downloaded file.
3. You may run the program by running the executeable or through the .jar file.

You may find extensive documentation for UPPAAL here.

Simple Example

As a first step in our tutorial, we will go through a very simple UPPAAL example to better understand the things that UPPAAL is capable of doing. I have included some pictures in this wiki entry, however, if you would like further visual details, as well as some additional content and explanations, you may watch the related tutorial session recording (November 17th).

Creating the automaton

1. Start by running UPPAAL. Make sure that you are on the Editor tab.
2. Create a very simple automaton with 2 locations and one transition going from the initial location to the other location.
3. You may rename the initial state to start and the final state to end.
4. The automaton should look like this:

Using the Simulator

1. Move to the Simulator tab and load the newly created model.
2. You should see one instance of your model (shown below), which will be named Process by default.

3. Note that the location highlighted in red is the current location of the transition system.
4. The highlighted transition corresponds to the transition selected in the Enabled Transitions pane:

5. At this stage you may play around with your model and run some transitions (you do not have too many options for this specific example).
6. A trace of the taken simulations will be shown in the Simulation Trace pane on the left:

7. The same trace will also be shown in a more visual manner in the bottom pane (you may need to change its size to see something.

NOTE: In the current example, the simulation possibilities are very limited. However, for the following example, and for the assignment, I suggest you explore the Simulation workspace thoroughly, as it may be very helpful to find potential problems with your model.

Check if a certain property holds for our automaton

For our simple example, we want to check whether the following property holds for our automaton:

It is possible to reach the location end in our automaton

1. Open the Verifier tab.
2. Find a formalization for the above property. In this case, the formalization is E<> Process.end. For further details concerning the syntax of the formalization, you may refer to the section below, as well as to the UPPAAL documentation.
3. Write the formalizatin in the Query box.
4. You may add a comment containing the english language explanation of your query to make it easier to keep track of.
5. Check whether the query holds for our automaton by clicking on the Check button. You should receive an output like this:

6. You may look at the trace that lead to the SAT/UNSAT conclusion by clicking on the Get Trace button. This loads the trace into the Simulator tab, where you can replay it, visualise it and analyse it. Once again, for this specific example, the trace is very simple (just a single transition).

Query Syntax Reference

Here are some explanations for the common temporal logic operators in the query syntax handled by UPPAAL:

1. E<> p - Possibly : There exists at least one path that contains at least one state where p is satisfied.
2. E[] p - Potentially Always : There exists at least one path where all states satisfy p.
3. A<> p - Eventally: For all paths, there exists at least one state where p is satisfied.
4. A[] p - Invariantly: For all paths, all states satisfy p.

Traffic Lights Example

We will now discuss a more complex case study which corresponds to a traffic lights automaton. Despite this example being more complex, the basic steps that we need to take are the same as explained above, namely (1) Create an automaton, (2) Optionally play around with the simulation, and (3) Verify properties on the automaton.

DISCLAIMER: The example that I am proposing below does not adequately represent real Traffic Lights. Additionally, it has some issues that will be addressed later on. This is done on purpose in order to not give too many hints related to the assignment.

Problem Description

We are going to create automatons for traffic lights at an intersection according to the below code snippets.

In this specific intersection, we will try to create the automatons such that both traffic lights cannot be Green at the same time. However, as mentioned in the disclaimer, we will only provide a partial solution for this.

In order to prevent the dangerous case mentioned above, we have set up the code snippets below in such a way that each traffic light will request permission to become green, and will only do so if the other traffic light has not already requested permission.

1  // Traffic Light 1
2  
3  // Initially, the RED light is on
4  request_1 := 1;
5  while(request_2 != 0);
6  // GREEN light is on
7  // YELLOW light is on
8  request_1 := 0;
9  // return to RED light

1  // Traffic Light 2
2
3  // Initially, the RED light is on
4  request_2 := 1;
5  while(request_1 != 0);
6  // GREEN light is on
7  // YELLOW light is on
8  request_2 := 0;
9  // return to RED light

NOTE: As you may notice, both code snippets are symmetric. Therefore, instead of creating two separate automatons, we will create a single template automaton and we will include two instances of the template in our system.

Creating an automaton

Here is what the final template automaton should look like. For step-by-step instructions on how to create this automaton, you may watch the corresponding tutorial recording.

Additional details concerning locations:

• As you can see, the automaton contains 4 locations. Note that the RED LIGHT setting of the traffic light corresponds to two locations in the automaton (Red_idle, Red_requested). This is because in the above code snippets, there are two different actions that need to be performed subsequently before moving to the GREEN LIGHT setting.
• The other two locations (Green and Yellow) are seperated by a transition that does not have a label. This is because there is no line of code to be executed between these two locations.

Additional details concerning transitions:

• The transition between locations Red_idle and Red_requested corresponds to line 4 in the code snippets. It is decorated with an Update operation request_self:=1.
• The transition between locations Red_requested and Green corresponds to line 5 in the code snippets. It is decorated with an Guard condition request_other==0.
• The transition between locations Yellow and Red_idle corresponds to line 8 in the code snippets. It is decorated with an Update operation request_self:=0.

About transition label types: In our example, we only use Update operations and Guard conditions.

• Update operations are variable assignments that happen when a transition is traversed.
• Guard conditions are conditions that must be met before a transition can be traversed.

About variable naming: As you noticed, we have used the request_self and request_other variable names to address the request_1 and request_2 variables in the snippets. In fact, these variables will be passed as parameters to the automaton template when we will be instantiating it. Specifically, for the Traffic Light 1, the request_self and request_other variables will refer to the request_1 and request_2 variables respectively, while for the Traffic Light 2, they will refer to request_2 and request_1 variables respectively.

Setting up the system

1. Once the automaton is created, we must rename it and add the parameters. As mentioned, our automaton template has 2 parameters, and both are integers between 0 and 1 inclusively. Parameters may have other types as well.
   • Name: TrafficLight.
   • Parameters: int[0,1] &request_self, int[0,1] &request_other.
2. Now, let's define our system. We need to include two instances of the automaton template with the correct parameter values. Modify the System declarations file to contain the following lines:

// Place template instantiations here.
TL1 = TrafficLight(request_1, request_2);
TL2 = TrafficLight(request_2, request_1);
// List one or more processes to be composed into a system.
system TL1, TL2;

3. Finally, in order to use the request_1 and request_2, we must declare them as global variables. Therefore, the Declarations file should contain the following code snippet:

// Place global declarations here.
int[0,1] request_1, request_2;

Simulating your automatons

Once you have completed your automaton and your system setup, you should move to the Simulator tab. If you have done everything correctly, you should see two instances of your TrafficLight automaton template:

Notice the name of each instance indicated at the top left of the model. This will be important for the queries in the following step.

At this stage, I propose you start playing around with the simulation environment and observing the various traces and enabled transitions. You will soon find out that this transition system is susceptible to deadlock. This is expected, because our system is not designed well. Figuring out how to improve the system design will be left as an exercise to the reader.

Check if a certain property holds for our automaton

Our initial objective was to design a system that would not encounter any dangerous situations. Let's check if this is true for our automatons.

A dangerous situation in our case study is a situation where both traffic lights are Green. Therefore we need to make sure that the system never encounters a state where both traffic lights are green.

The above property is formalized as follows: A[] not (TL1.Green and TL2.Green). In the Verifier tab, we can check if this property holds for our automatons. As expected, this property does hold.