Vous êtes ici

Efficient Abstraction Techniques for Timed Automata Verification

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
http://www.irisa.fr/sumo/index.html
Directeur de thèse
Nicolas Markey
Co-directeur(s), co-encadrant(s)
Ocan Sankur
Contact(s)
Sujet de thèse
Descriptif

Context. Formal verification techniques have emerged as a need for proving the correctness of computer systems with increasing complexity. Among those techniques, model checking has gained significant attention both in academic and industrial contexts, as witnessed by the 2007 Turing Award won by its inventors. The first model-checking algorithms concentrated on proving logical correctness for finite-state systems, such as whether a given error state is reachable, or whether the sequence of visited states satisfies a given property. However, the correctness of numerous computer systems not only concerns functional correctness, i.e., whether the system computes the expected output, but also non-functional properties such as execution time or energy consumption. The importance of incorporating these quantitative aspects in the verification process for embedded systems is well recognized, and researchers have been pushing for the development of a strong theory and powerful tools to support such a shift. Although existing finite-state verification techniques might allow designers to model some real-time and quantitative aspects, these are usually not sufficient: the discretization of the quantities may lack precision in the modeling, and when it is precise enough it tends to produce large finite-state systems that even cutting-edge techniques cannot handle adequately. It is thus crucial to develop specialized techniques for real-time systems with such quantitative features with a focus on improving the expressiveness and the scalability of formal verification with respect to existing techniques.

Timed automata. Timed automata [AD94] are an extension of finite automata with a finite number of continuous clocks with identical rates. They are among several formalisms that have been developed to explicitly model quantitative features, and have become a standard formalism for modeling systems with strong timing constraints in order to take execution times, delays, and jitter into account. They have a simple yet expressive representation of timing constraints, and enjoy symbolic verification and synthesis algorithms that efficiently exploit the particular structure of such infinite-state models. Tools such as Uppaal [BDL+06] implementing these algorithms are available, and have been applied to numerous case studies from various application areas including communication protocols, clock synchronization algorithms, scheduling problems etc. Several extensions of this formalism has been studied. Among these, weighted timed automata [ATP01] are an extension with a cost function which allows one to solve optimization problems defined on timed systems. Controller synthesis has been modeled with timed games which are two-player games which model interactions between a controller and an adversarial environment. The success of this approach in the community is witnessed by two Computer-Aided Verification (CAV) awards; in 2008 for the formalism of timed automata, and in 2013 for the tool Uppaal.

State-of-the-art and Beyond. State-of-the-art algorithms are semi-symbolic: they explore the state space by enumerating the discrete states (of the underlying finite automaton) explicitly, while clock valuations are represented symbolically using zones, which are a special kind of polyhedra. The efficiency of these algorithms is due to the fact that for many systems, even complex timing constraints can be efficiently captured using zones. To ensure efficiency, current tools use extrapolation operators on zones which are abstraction operators that preserve reachability properties [BBLP06]. Recent results [HSW16] establish the theoretical limits of these operators and define the coarsest abstraction operators with this property. On weighted timed automata, not all extrapolation operators can be applied, and the analysis tends to be much more costly. Solving timed games with cost functions is especially challenging: basic questions such as optimal-cost reachability are undecidable [BBR05,BBM06], but approximation algorithms were given recently [BJM15].

Objectives in this PhD. In order to develop faster algorithms and make verification and synthesis algorithms scale, the principal idea to be pursued in this PhD will be to 1) consider incomplete abstraction methods, such as, abstraction operators that are sound but incomplete, 2) develop techniques to reduce the space of the discrete states. Both ideas can be applied to optimization problems on weighted timed automata and for (optimal) controller synthesis. During his PhD work, the candidate will implement newly developed algorithms in an existing model checker to which the supervisors are actively contributing. Case studies can also be done to demonstrate the applicability of the algorithms.

One of the main ingredients will be the counterexample guided abstraction refinement (CEGAR) framework [CGJLV03] applied to timed automata. Algorithms based on this approach starts by analyzing a very coarse abstraction of the given system. If the analysis proves the specification, then the specification holds for the concrete system as well so the algorithm stops. Otherwise, the algorithm analyzes the produced counterexample to check whether it is feasible in the concrete system. If it is feasible, this is a true counterexample and the algorithm stops. Otherwise, the abstraction is automatically refined in a minimal way, in order to exclude the said trace, and the analysis restarts. This approach has had a big impact in analyzing complex systems including synchronous systems and programs. Some preliminary work appeared for timed automata [DKL07] but considered abstractions simply consisted in removing clocks or collapsing discrete states.

We list possible directions we can follow during this PhD below. We expect at least the first three of them to be achieved. If they are achieved faster than expected, objectives 4 and 5 are possible continuations, which are also more open.

 

Objective 1: Incomplete Abstraction Methods. Developing more aggressive abstractions to improve over the work on extrapolation operators. This consists in defining an abstract domain of zones, thus restricting the search space of the model checking algorithm. If the analysis is too coarse and produces false negatives, then the abstract domain is automatically refined. This technique can be combined with existing extrapolation operators, removal of clocks or collapsing of discrete states.

Objective 2: Suboptimal Algorithms for Weighted Timed Automata. In weighted timed automata, algorithms and tools exist to solve the optimal reachability problem. These use priced zones, an extension of the zones with affine functions defined on zones to account for the cost function. However, the successor computation is more costly than for plain timed automata, and the number of zones tend to grow quickly (zone explosion) which limits the applicability of this technique. In order to develop faster algorithms, we suggest trading optimality against efficiency, and consider abstractions which limits the zone explosion with a less precise analysis.

Objective 3: Abstraction Techniques for Synthesis. Preliminary works on abstraction refinement applied to discrete states in timed games show promising results in experiments [EMP10]. We will push this idea further to study zone abstractions in timed games. Here, a crucial question is the synthesis of simple strategies; in fact, automatically synthesized strategies very tend to be too big and complex to represent. Synthesizing small strategies is an important challenge since the efficiency of automatic abstraction refinement depends on the simplicity of counterexamples; small strategies are also preferable for implementation purposes, and enabling designers to understand the synthesized system. 

Objevtive 4. Robustness in Distributed Systems. One of the uses of timed automata is the formal verification of distributed systems with local clocks and communication delays. While clocks of timed automata allow one to model such delays, the formalism does not allow multi-rate clocks or drifts. Although theoretical algorithms and some practical implementations exist for “small enough” clock drifts [P00,S15], the general question of practical model checking under a given assumption on clock precision is open. We suggest studying abstraction operators defined on zones that allow one to account for drifts within a given bound. The advantage of such operators is its adjustability: a different operator can be defined for different precision assumptions, and a different set of deviating clocks. This approach is to be compared with the quasi-synchronous approach which yields a finite-state abstraction [C00].

Objective 5. Fully Symbolic Algorithms. For timed automata models with large discrete spaces, fully symbolic algorithms based on binary decision diagrams (BDD) have been developed. This has the advantage of scaling to large systems although the performance is extremely sensitive to the presence of large constants in the models. As a rule of thumb, zone-based algorithms are efficient for systems with small discrete spaces but complex time constraints; while BDD algorithms have proven efficiently for large discrete spaces with simple time constraints. An important challenge in timed automata verification would be to mix both and develop scalable techniques for large and complex systems. We suggest exploring fully symbolic algorithms by exploiting clever abstractions.

Bibliographie

[ABM04] R. Alur, M. Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In ICALP’04, LNCS, p. 122–133. Springer, 2004.

[AD94] Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, April 1994.

[ATP01] R. Alur, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. In HSCC’01, LNCS 2034, p. 49–62. Springer, 2001.

[BBBR07] Patricia Bouyer, Thomas Brihaye, Veronique Bruyere, and Jean-Francois Raskin. On the optimal reachability problem on weighted timed automata. Formal Methods in System Design, 31(2):135– 175, October 2007.

[BBLP06] Gerd Behrmann, Patricia Bouyer, Kim G. Larsen and Radek Pelánek.  Lower and Upper Bounds in Zone-Based Abstractions of Timed Automata.  International Journal on Software Tools for Technology Transfer 8(3), pages 204-215

[BBM06] P. Bouyer, Th. Brihaye, and N. Markey. Improved undecidability results on weighted timed automata. Information Processing Letters, 98(5):188–194, 2006.

[BBR05] Thomas Brihaye, Véronique Bruyère, Jean-François Raskin: On Optimal Timed Strategies. Proceedings of FORMATS 2005: 49-64

[BCM16] Patricia Bouyer, Maximilien Colange, and Nicolas Markey. Symbolic optimal reachability in weighted timed automata. Proceedings of CAV’16, volume 9779 of LNCS, pages 513–530. 2016.

[BDL+06] Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Hakansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. Uppaal 4.0. In Proceedings of the 3rd International Conference on QuantitativEvaluation of Systems (QEST’06), pages 125–126. IEEE Comp. Soc. Press, September 2006.

[BJM15] Patricia Bouyer, Samy Jaziri and Nicolas Markey.  On the Value Problem in Weighted Timed Games.  In CONCUR'15, Leibniz International Proceedings in Informatics 42, pages 311-324. Leibniz-Zentrum für Informatik, 2015.

[C00] Paul Caspi. The quasi-synchronous approach to distributed control systems. Technical Report CMA/009931, Verimag, Crysis Project, 2000. “The Cooking Book”.

[CGJLV03] Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 5 (September 2003), 752-794. 

[DKL07] Henning Dierks, Sebastian Kupferschmid, and Kim G. Larsen. Automatic abstraction refinement for timed automata. In FORMATS'07, Springer-Verlag, Berlin, Heidelberg, 114-129.

[EMP10] Rudiger Ehlers, Robert Mattmuller, and Hans-Jorg Peter. Combining symbolic representations for solving timed games. In Proceedings of the 8th International Conferences on Formal Modelling and Analysis of Timed Systems, (FORMATS’10), volume 6246 of LNCS, pages 107–212. September 2010.

[HSW16] Frédéric Herbreteau, B. Srivathsan and Igor Walukiewicz. Better Abstractions for Timed Automata. Information and Computation 251, p. 67-90. Elsevier, 2016

[P00] Anuj Puri. Dynamical properties of timed automata. Discrete Event Dynamic Systems. 2000 Jan 1;10(1-2):87-113.

[S15] Ocan Sankur. Symbolic quantitative robustness analysis of timed automata. TACAS’15, volume 9035 of LNCS, pages 484–498. Springer-Verlag, April 2015.

 

 

Début des travaux: 
01/09/2017
Mots clés: 
formal verification, model checking, timed automata, controller synthesis, abstraction
Lieu: 
IRISA - Campus universitaire de Beaulieu, Rennes