Project Topics
Get Complete Project Material File(s) Now! »
Formal verification (or model checking)
The domain of verification is concerned with proving or disproving that systems behave as required under all possible circumstances. In fact, a model checker uses an algorithm to check if a logical formula holds in a system. A system can be represented by an automaton containing some states and transitions. Thus, the set of all paths in the transition graph of the automaton represents the set of all possible behaviors of the system. So the problem of verification can be reduced to the problem of checking the existence of certain paths in the transition graph. Reachability properties are a type of the properties to which verification is applied; they are verified by a path to know whether or not it reaches some specific states. In some cases it should be checked if all behaviors avoid a set of “forbidden” states, e.g. a state where the system is in the risk of failure, and in some others behaviors should be found that proceed to a desired final state, e.g. a state where all tasks have terminated. Such properties are examples of safety and liveness properties, respectively. If the system fails to meet a specific property, the model checker can be asked to generate a counterexample to show how the property was violated. Furthermore if the system meets the property, the model checker can be also asked to generate a witnessing trace to illustrate one of the possible paths for which the property holds.
By assigning numerical weights to the automaton transitions, one can associate real numbers with paths and search for paths that have minimum weight, using fastest path algorithms. Therefore by performing reachability analysis along with using shortest path algorithms, the minimum makespan can be found.
Property-specification language
In this section required formalisms for expressing properties of timed systems is presented. There exist two types of formalisms, linear-time and branching-time. In linear time, properties are interpreted as sets of executions and specifications are evaluated on runs. While in branching time, properties are validated on sets of execution trees and specifications are checked on semantic graphs (Tripakis 1998).
Since branching time properties are used by powerful tools such as UPPAAL and Kronos, in this thesis, only this kind of properties is considered.
Compositional model checking
The state space explosion occurs in systems with many concurrent components where most of the model checking techniques are inefficient or impossible. A solution in this case is to decompose the system into components and then to verify them individually (Berezin, Campos, and Clarke 1998). If the all the components satisfy the properties properly, it is concluded that the system behaves correctly. The main difficulty is to find if after the parallel composition, all properties still remain satisfied. In fact, in some example, different processes of the system need to interact with each other to satisfy a property and hence cannot be verified individually (Al-Bataineh 2015).
General principle of modeling procedure
The scheduling problem statement needs to capture four features: task triggering, simultaneity, mutual exclusion and timing. For this purpose, a semi-formal model based on WA is proposed. Inspired from the (max, +) automata formalism, they offer an intuitive way of modeling the behavioral features mentioned above. Thus, each scheduling problem considered in this work is defined as a collections of WAs. The actual scheduling should comply with the WA problem statement. As explained in the introduction, the existing synchronous compositions for WA cannot be used for the scheduling purpose. Since they either don’t contain a trajectory with the optimum makespan to be used as the optimal schedule or are not capable of illustrating simultaneous execution of tasks which is a non-separable issue from scheduling. Hence, there are two possible solutions for solving a scheduling problem that is modeled by WA. The first solution is to employ timed model checking techniques (Baier and Katoen 2008) which are defined for timed automata. To this end, each WA model of the problem statement is systematically translated into a Timed Automaton (TA), according to specific rules defined in the sequel. The resulting model is directly usable by a timed model checking tool. The second solution is to define a new synchronous composition for WA in order to compose WA models directly and solve the scheduling problem without translating to timed automata.
In the next section the scheduling problem is modeled by WA.
Solving MRS scheduling problem by means of translating weighted automata models into timed automata models
The previous section defines WA modeling frameworks for defining scheduling problems. In the introduction section, it is explained that for obtaining a schedule, it is needed to perform a parallel composition on automata models of the scheduling problem, Parallel composition of a set of automata enables us to compose and explore them. Whereas, the existing parallel composition definitions for WA either don’t contain a trajectory with the optimum makespan to be used as the optimal schedule or are not capable of illustrating simultaneous execution of tasks which is a non-separable issue from scheduling. Therefore, WA models cannot be explored and analyzed directly. Hence, after modeling the problem by WA, one solution is to translate the WA model to another type of automata for which an efficient definition of parallel composition exists. Then, compose the automata model through that definition and analyze the new model. Timed automata formalism has this characteristic and furthermore, there exist formal verification tools for timed automata that can be used to compose and analyze timed models automatically. Thus, in this thesis, the WA models are translated into timed automata. Thence, after translating the WA models to timed automata model, they are implemented in a formal verification tool named UPPAAL and the optimum makespan are found automatically. Translation of the models in the previous section are done through certain rules that are expressed in this section.
Finding the optimal schedule
In order to find the minimum makespan through synchronous composition of WA, an optimal time trajectory should be found from the initial state of the synchronous composition to its marked state.
Let 1/ 1 / be a finite run of a weighted automaton = 0 ⎯⎯ 1 … ⎯⎯⎯.
where is a set of actions executing during th transition and denotes the duration of th transition of the run. The duration of , ( ), is the sum ∑ ∈[1, ] .
For a state , the minimal duration for reaching , ( ), is the infimum of the durations of the finite trajectories which end in (Behrmann, Fehnker, Hune, Larsen, Pettersson, Romijn, et al. 2001): ( ) = inf{( )| :} (3.1).
Gerd Behrmann et al. (2001) suggest an algorithm for determining the minimum cost for reaching a target state satisfying a property in a priced time automata. Inspired from their algorithm, Algorithm 3.9 is presented that minimizes time of reaching a marked state from the initial state in a WA and yields the fastest trajectory.
In this algorithm, all encountered states are included in two data structures and that store explored and unexplored states, respectively. Initially, is empty and includes the initial state. The global variable , which is initially set to ∞, stores the lowest duration achieved so far for reaching the marked state. The optimum schedule is a trajectory from the initial state 0 to the marked state with the minimal duration that is initially empty.
In each iteration, a state is taken from and is checked if it corresponds to the marked state . If it was the marked state and ( ) was less than , it stores ( ) as the minimum and its related trajectory as the optimal schedule ℎ . Then it adds the state to and its successors to . In this algorithm, → ′ means ′ is reachable from .
Table of contents :
1 GENERAL INTRODUCTION
1.1 INTRODUCTION
1.2 STATE OF THE ART
1.2.1 State of the art on general scheduling problems
1.2.2 State of the art on scheduling problems modeled by automata
1.2.3 State of the art on synchronous composition of weighted automata
1.2.4 State of the art on MRS scheduling considering uncontrollable environment
1.2.5 Synthesis of the state of the art
1.3 RESEARCH QUESTION
1.4 CONTRIBUTION
1.4.1 Chapter 2: MRS scheduling through translation of weighted to timed automata
1.4.2 Chapter 3: Multi-resource sharing scheduling by using synchronous composition of weighted automata
1.4.3 Chapter 4: Multi-resource sharing scheduling considering uncontrollable environment
1.5 BACKGROUND
1.5.1 Formal verification (or model checking)
1.5.2 Property-specification language
1.5.3 The branching time logic TCTL
1.5.4 TCTL properties
1.5.5 Techniques for constructing reachability graph of systems
1.5.6 Digraph traversal algorithms
1.6 CONCLUSION
2 MULTI-RESOURCE SHARING SCHEDULING THROUGH TRANSLATION OF WEIGHTED TO TIMED AUTOMATA
2.1 INTRODUCTION
2.1.1 State of the art
2.1.2 Synthesis of the state of the art
2.2 MRS SCHEDULING PROBLEM DESCRIPTION
2.3 MODELING MRS SCHEDULING PROBLEM BY WEIGHTED AUTOMATA
2.3.1 General principle of modeling procedure
2.3.2 Problem statement by weighted automata
2.4 SOLVING MRS SCHEDULING PROBLEM BY MEANS OF TRANSLATING WEIGHTED AUTOMATA MODELS INTO TIMED AUTOMATA MODELS
2.4.1 Translating transitions of the WA model to TA
2.4.2 Translating WA models to TA models
2.4.3 Scheduling approach
2.4.4 Complexity
2.5 CONCLUSION
3 SYNCHRONOUS COMPOSITION OF WEIGHTED AUTOMATA – APPLICATION TO MRS SCHEDULING
3.1 INTRODUCTION
3.1.1 State of the art on synchronous composition of weighted automata
3.1.2 State of the art on time-optimal reachability analysis
3.1.3 Synthesis of the state of the art
3.2 SYNCHRONOUS COMPOSITION FOR WEIGHTED AUTOMATA
3.2.1 Example 2
3.2.2 Algorithmic steps to reach synchronous composition
3.2.3 Synchronous composition of DSDA weighted automata
3.2.4 A simple example of synchronous composition (Example 2-continue)
3.3 FINDING THE OPTIMAL SCHEDULE
3.4 CONCLUSION
4 MULTI-RESOURCE SHARING SCHEDULING CONSIDERING UNCONTROLLABLE ENVIRONMENT
4.1 INTRODUCTION
4.1.1 State of the art
4.1.2 Synthesis of the state of the art
4.2 BACKGROUND
4.2.1 Timed Game Automata
4.2.2 Safety and reachability games
4.2.3 Winning games
4.2.4 Strategy
4.2.5 Synthesis tool TIGA
4.2.6 Winning/losing conditions
4.2.7 Partially Cooperative Games
4.2.8 Time Optimal Strategy Synthesis
4.2.9 Example of timed game automata
4.2.10 On-the-fly algorithm for timed games
4.2.11 Interval weighted automata
4.3 PROBLEM DESCRIPTION
4.4 DIFFERENT TYPES OF UNCONTROLLABLE PARAMETERS
4.5 MODELING THE SCHEDULING PROBLEM THROUGH TGA CONSIDERING UNCONTROLLABLE PARAMETERS
4.6 EXAMPLE 3
4.7 SOLVING APPROACH
4.8 EXAMPLE 3 (CONTINUE)
4.9 CONCLUSION
5 CONCLUSION AND PERSPECTIVES
5.1 GENERAL CONCLUSION
5.2 GENERAL PERSPECTIVES
5.3 RELATED PUBLICATION
REFERENCES
