Project topics and materials
Get Complete Project Material File(s) Now! »
Model Checking
Model Checking is a verification technique that is used to check that a model (of the system to be verified) complies with, or implements a, desired behavior. For computer programs, model checking takes as input a description of the computer program and a desired property to be checked. The model checking tool can result in two kinds of outputs. It can guarantee that the desired property holds or it can give a counter example or trace if the desired property is not satisfied. Returning a counter example when the desired property is not satisfied is an appealing feature of model checking that helps a lot in identifying as well as in fixing errors. In computer systems, the correctness of a software application can be represented in the form of various properties. These properties can be divided into two main categories so that most interesting properties can be classified in one of these two categories. The first category of properties is the one of safety properties where nothing bad ever happens. For example, that air traffic control never allows two airplanes to land at the same track at the same time. Another example is that a coffee machine pours coffee when there is no cup. A safety property is violated whenever a bad configuration is reached. The second category of properties is the one of liveness properties specifying that good things ultimately happen. For example, when the appropriate button of a coffee machine is pressed then coffee is eventually produced. A liveness property is violated when the system is running and it does not come across a good configuration. The verification tools implemented at ESLAB perform model checking on over-approximations of parameterized systems to check safety properties. These tools are quite complex to manipulate. Our verifier that we implemented in this thesis to experiment with interacting with a verification tool, pretends to perform model checking of a parameterized system.
Parameterized Systems
The tool developed in this thesis work allows exploring behaviors of parameterized systems and can interact with verification tools in such a way that one can plug in several independent verification tools for different classes of parameterized systems.“Parameterizedsystemsare composed of an arbitrary number of identical state machines runninginparallel”[3,4]. Each state machine has local variables and can have access to a number of shared variables. Transitions of a state machine can also depend on the state of other state machines. State machines are also referred to as processes or components. Parameterized systems are widely used in cache coherence protocols, mutual exclusion algorithms, sensor systems, telecommunication protocols and bus protocols.
More formally, a parameterized system P is a triple (Q, X, T) where Q represents the states of one process, X is the set of local variables and T represents the transitions. A particular transition can be of the following form.
q
t: guard assignment q’
In this transitionrulet,qisthecurrentstate,q‟isthenextstateandbothq,q‟∈ Q. A guard is a predicate that depends on the values of the current states and variables. If all the guards are satisfied, the assignments to the variables will be applied and the state machine will go from the current state q to the next state q‟. A configuration is a snapshot of the parameterized system at some time that has information about the states and values of all variables and processes in the system. A component can have local and global transitions. A local transition does not depend on or change the state and variables of the other processes in the configuration. A global transition depends on, and may change, the states and variables of the other processes in the configuration. In the beginning, we initialize all the processes and that state of the system is called an initial configuration. A transition can change the state of a single process or many other processes. One objective of this work is to simplify the interaction with tools that verify the correctness of such systems irrespective of the size of the considered configurations. The size of an instance of the parameterized system, or of a configuration, is the number of processes in the instance, or configuration.
Example:
Parameterized systems can be organized into trees, linear array structures or unstructured. They can involve variables of different types: Booleans, integers or arrays. They can communicate using different kinds of transitions. For example, linear parameterized systems organize there processes in a linear array. Consider the instance of a linear parameterized system depicted in Figure 2.1. This instance has five processes, each with only two possible states, idle and critical. In the beginning all state machines are in the idle state. A state machine can change the state by following one of the two transition rules. First one is the global transition that says a state machine can move from the idle state to the critical state if and only if all other state machines are in their idle state. This condition is denoted by LR (idle) that says that transition can only occur if all the state machines on the left of the current state machine and all the state machines on the right of the current state machine are in idle state. The second transition is a local transition rule that says a state machine can also come to idle from critical state at any time. A state machine in this linear parameterized system can only be in one state at a time either idle or critical.
An example of a safety property for such a simple parameterized system is mutual exclusion. It specifies that, in any case, no two state machines can be simultaneously in their critical section. A state machine can access shared resource only when it is in critical section. There are many mutual exclusion algorithms (Burns [3, 4], Dijkstra [3, 4] and Szymanski [4]) that can be modeled as linear parameterized systems.
Design
In this chapter, we will focus on the design aspects of the tool developed in this project. First we will introduce our design choices. Then we will explain how we designed a mockup verifier that allowed us to experiment with different strategies to plug in verifier. This mockup verifier allowed us to focus on how to plugin general verifier instead of focusing on particular ones. Also this saved a lot of time and helped in implementing as well as testing several of the functionalities that were expected from this tool. We will also define the communication between the tool and the verifier. At the end of this chapter we will talk about the development environment and tools used in this project.
The objective of this thesis work is to develop a user friendly tool with an intuitive Graphical User Interface that allows exploring behaviors of parameterized systems and should allow to interact with various verification tools in such a way that one can plug in several independent verification tools.
ensure that it is independent of the verifier. The intuition behind separating the interface and theverifieristhatourinterfacedoesn‟tneedtoknow anything about the verifier. Anything in the sense that, interface does not care in which programming language the verifier is implemented. These verification tools can be written in any language. For example, the tool is designed to work perfectly even if verifier 1 is implemented in java, verifier 2 is implemented in C++. It is the responsibility of the verifier to parse the input given by the user, so that the verifier knows everything about the description of the system. For now, the interface is totally unaware about the class of parameterized systems being handled. The interface will perform three different types of simulations: random simulation, interactive simulation and guided simulation. The disadvantage of separating description from the tool is that we cannot have pretty nice printing for configurations and transitions. As the tool is unaware about the description so the transitions cannot be visually seen using arrows and ovals in a graphical manner.
Simulation Algorithm
Figure 3.2 shows the simulation algorithm that takes parameterized system P(Q, X, T) plus trace for guided simulation as input. Here, Q represents the states of one process, X is the set of local variables and T represents the transitions.
Random Simulation
The algorithm in figure 3.2 takes the description of the parameterized systems as input. Then, it will get initial configuration and will store it. The simulation loop will start and will continue execution until there is no enabled transition. We will pass that configuration and parameterized system to a function get_enabled that will return us all the enabled transitions. After getting enabled transitions, we will check if enabled set is not empty. In random simulation, simulation choices are randomly selected using a random number generator. We will randomly choose one enabled transition and will fire it on the configuration to get the new configuration. Now, the simulation process will be repeated within the loop with new configuration.
Interactive Simulation
The algorithm shown in figure 3.2 takes the description of the system as input. After having description, it gets initial configuration and stores it. Simulation loop will start execution until there are enabled transitions. The configuration and the parameterized system is passed as an argument to a function get_enabled and this function will return all the enabled transitions. We will check that if we have enabled transitions and then we will ask from the user to choose one transition from these enabled transitions. Once the user has chosen one transition, we will fire that transition on the configuration and will get next configuration. Now, the simulation loop will be executed using this updated configuration. Figure 6.11 shows you the choices printed in the popup dialog box titled Interactive Simulator.
Guided Simulation
Guided Simulation requires a trail to carry out simulation. Whenever you perform random or interactive simulation,you can save the trail by pressing „Save Trail‟button and this will store simulation results in a file. This trail file can be used later to perform guided simulation. An example of a very small trail file can be seen below in figure 3.3.
Each row contains a record and this trail file has only two records. The verifier will first parse this trail file and then for each record it will fire transition on the configuration using the choice and will match the resulting configuration. Like interactive simulation, you can also control the speed of guided simulation by entering iterations in a popup dialog box that appears when you click simulate button after choosing guided simulation.
We considered two design choices for our tool. In the first choice the tool parses the description of the system and thus knows everything about the system. The advantage is that the tool would be rich enough to print the transitions in a nice way. For example, use of different colors to highlight various type of transitions. Moreover, have ovals to represent local variables and squares to represent shared variables. The disadvantage of this design choice is that the tool would require an important adaptation effort in order to plug in a new verifier targeting a new class of parameterized systems. In the second design choice, it is the responsibility of the verifier to parse the description of the system and it is only the verifier who knows everything about the system, thus our tool is unaware about the description of the system. Whenever the tool requires successors, transitions or initial configuration, it requests the verifier and the verifier provides the required output in desired format. We have adopted this design choice because in this way we can plug in more than one independent verifier. Moreover, we have made communication between the tool and the verifier clear. For instance, observe that the simulation algorithm given in figure 3.2 has various functions. During simulation, the tool will ask the verifier to give back initial configuration and transition pattern and these values will be printed in the tool. Now the tool will ask the verifier
(currently our mockup verifier) to give back enabled transitions and one of the transitions is fired on the configuration to get next configuration (computation of successors). Choosing one transition depends upon the mode of the simulation, in random simulation a random number generator is used to randomly choose one transition while in interactive simulation all the choices are printed to the user and user choses one transition. All the core functionality are requested from the verifier and the tool is unaware about the implementation details. This next configuration is used to repeat the whole process and the tool will stop until there is no enabled transition on the given configuration.
We can plug in any type of the verifier with the tool but the verifier has to follow the communication protocol and should provide the required functionality as explained in next section.
Contract between tool and verifier
As explained in previous section that only the verifier knows all the description about the system and the tool is unaware about the description. Thus the tool will request verifier for various functionalities and the verifier has to provide these functionalities. In order to plug in a verifier, it has to respect the contract and has to provide the functionalities mentioned in the contract. Interaction between the tool and verifier is based upon a contract. Verifier is required to have some functions to be used by the tool. Following are the functions this tool expects from the verifier.
1. getChoices(String configurationString)
This function takes a configuration in the form of string and returns a list of choices in the form of string
2. fire(String stepString)
This function fires the transition on the configuration to get next configuration. In firing, it applies all the assignments.
3. getNextConfiguration(String stepString)
This function returns next configuration. The function fires the transition on the Configuration and returns the new configuration in the form of string.
4. getInitialConfiguration()
This function returns initial configuration.
5. showStringTransitions()
This function returns all the transitions (present in the description of the system).
Mockup design
A mockup verifier is developed to perform the functionality of the verifier and to test the application. Developing a mockup verifier saved a lot of time as developing a new verifier can take much time. Mockup verifier knows all about the system description and has the appropriate functionality for carrying out random, interactive or guided simulation. It first parses the description of the system and then interacts with the tool using the protocol introduced in the previous section.
Table of contents :
Abstract
Acknowledgements
Table of Contents
List of Figures
1 Introduction
1.1 Background: Testing and Verification
1.2 Problem statement
1.3 Targeted Readers
1.4 Objectives
1.5 Development Methodology
1.6 Organization of the Thesis
2 Background
2.1 Model Checking
2.2 Parameterized Systems
3 Design
3.1 Simulation Algorithm
3.1.1 Random Simulation
3.1.2 Interactive Simulation
3.1.3 Guided Simulation
3.2 Contract between tool and verifier
4 Mockup design
5 Development environment and tools
5.1 IDE language environment
5.2 ANTLR
5.3 Documentation development
6 Results
6.1 Screenshots
6.1.1 Random Simulation
6.1.2 Interactive Simulation
6.1.3 Guided Simulation
6.1.4 Verification
7 Future work
8 Bibliography
