An effective fixed point calculus for deterministic systems applied to model checking

Julien Musset 1 Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Transition systems has been intensively applied to the modeling of complex systems, for example they have been used for giving semantics to synchronous languages such as Lustre or Signal, or to hybrid automata. Properties of their behavior can be verified using model checking procedures, which rely on an iterative computation of least or greatest fixed points. For instance, safety properties can be proved by a fixed point computation of the set of all the states that can access to the forbidden states and verifying that it does not contain an initial state. This approach has to face two main difficulties : the complexity of the data types domain and the termination of the iterative algorithm. They are solved by approximation heuristics such as abstract interpretations and widening operators. However, in many cases, a sharper analysis of the transition system can be exploited to speed up the calculus. Consequently, we propose an other algorithm to compute this fixed point taking advantage of the decomposition of the relation in an union of simpler relations. If the transition system is deterministic, then our algorithm computes the exact fixed point, otherwise it computes an over approximation. We have implemented this algorithm on top of a linear constraint solver over real number and applied it to the proof of a safety property of a reactive system and we compare with the model checker Hytech.
Type de document :
Communication dans un congrès
First International Workshop on Automated Verification of Infinite-State Systems - AVIS'01, Mar 2001, Berlin, Germany, 4 p, 2001
Liste complète des métadonnées

https://hal.inria.fr/inria-00100501
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:46:20
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100501, version 1

Collections

Citation

Julien Musset, Michaël Rusinowitch. An effective fixed point calculus for deterministic systems applied to model checking. First International Workshop on Automated Verification of Infinite-State Systems - AVIS'01, Mar 2001, Berlin, Germany, 4 p, 2001. 〈inria-00100501〉

Partager

Métriques

Consultations de la notice

169