Project topics and materials
Get Complete Project Material File(s) Now! »
Temporal Logic and properties
Model checking consists in verifying with mathematical rigor the system model with respect to some properties of the system. Both the system model and the properties to verify need to be described in a precise and unambiguous manner. Temporal logic is a mathematical formalism tailored for statements and reasoning where time is involved. It oers special operators for time, fairly close to natural language statements (the adverbs \always », \until », etc). It also comes with a formal semantics, making temporal logic an indispensable tool for formalizing properties concerning dynamic behaviors of a system. The most common temporal logics are the LTL (Linear Time Logic) [142] and the CTL (Computation Tree Logic) [62]. Time can either be interpreted to be linear (LTL) or branching (CTL). Both logics are subsets of CTL*, introduced by Emerson and Halpern [75]. Most model checkers support either LTL or CTL, or sometimes both. Other temporal logics used for model checking are HML (Hennessy-Milner Logic) [104], Modal -calculus [119], and dierent avors of CTL such as timed [14], fair [76] or action [137] CTL. The logic CTL* served to formally state properties concerned with the executions of a transition system. It consists of the following elements:
1. Atomic propositions 2 AP.
2. Boolean operators:
Constants true and false.
Logical \not » :, logical \or » _, logical \and » ^.
Logical implication ) and double implication ,. For , 2 AP,
) means if then ; , states \if and only if ».
Temporal operators X, F, G and U. X states that holds for the next state; F states that a future state satises without specifying which state; and G that all the future states satisfy , i.e will always hold.
Model checking algorithms
Given a model M and a property of the system under consideration, the model checking algorithm answers the question \whether M satises the property ? » in a mathematically formal manner. Should a property violation detected, a model checker is capable to return a counterexample, illustrating how the violation occurs. Several dierent algorithms have been proposed, for property specication in dierent temporal logics, and using dierent data structures. As mentioned before, LTL formulas are considered to be path formulas as well as CTL formulas state formulas. Consequently, counterexamples for LTL formulas are also linear Explicit (state) model checking is the rst generation of successful model checking algorithms. Dierent approaches for LTL-based properties [124, 167] and CTLbased properties [63, 145] have been proposed. Explicit model checking explores explicitly the state space of a model and searches by forward exploration until a property violation is founded. In LTL model checking, the exploration algorithm can be depth-rst or breadth-rst: breadth-rst approach nds the shortest possible counterexamples but demands signicantly higher in memory use than depth-rst approach. In CTL model checking, the set of all the states satisfying the given property are determined by recursively calculating the satised subformulas for each state. If all states are visited and no violation is detected, the model is considered to satisfy the property.
Testing with model checkers
The main idea of testing with model checkers is to force model checkers to systematically generate counterexamples and then interpret these counterexamples as test cases. Model checking is originally proposed as a formal verication technique and a model checking problem is normally a property verication problem. On the other hand, test cases are related to certain test purposes, describing the desired characteristics of test cases. If the test purposes can be specied in temporal logic and then used as properties to force the model checker to generate counterexamples, the test generation problem is actually transformed to a \traditional » model checking problem (see Fig. 2.5).
Table of contents :
1 Introduction
1.1 Problem statement
1.2 Thesis contributions
1.3 Thesis organization
2 Model checking and its application
2.1 Model checking preliminaries
2.1.1 Transition systems
2.1.2 Temporal Logic and properties
2.1.3 Model checking algorithms
2.2 Testing with model checkers
2.3 Synchronous approach for real-time systems
2.3.1 Esterel
2.3.2 Signal
2.3.3 Lustre
2.3.4 A brief summary
2.4 The story of Lustre
2.4.1 SCADE and Lustre
2.4.2 Lustre versions
2.4.3 Model checking tools for Lustre
2.4.4 Lustre translators
3 Project \CONNEXION »: Towards a complete testing environement
3.1 Functional validation objectives
3.2 Unique and complete tool box
3.3 \CONNEXION »: challenges and constraints
3.4 Information system of traceability
4 Model-based testing for functional validation: Towards hybrid verication
4.1 Model-based testing process
4.1.1 Coverage criteria
4.1.2 A new MBT methodology for safety-critical systems
4.1.3 A heuristic: hybrid verication
4.1.4 An rst example: cruise control
4.2 Renement by gradually adding constraints in GATeL
4.2.1 Three categories of constraints
4.2.2 Renement by adding progressively the constraints
5 \CONNEXION » Case study: SRI
5.1 Description of SRI
5.2 Experimentation results of part 1
5.3 Lustre model checkers toward hybrid verication
6 Conclusion
Appendices
