Vérification formelle de systèmes : contribution à la réduction de l'explosion combinatoire
Institution:
Toulouse, INSADisciplines:
Directors:
Abstract EN:
Formal verification technique often runs up against the combinatorial explosion problem: the number of states of the transitions system grows in an exponential way with respect to the component count of the system. This thesis study two causes:- For untimed systems, concurrency is represented by actions interleaving which produces a lot of combinations. This thesis investigates partial-order approaches to compute a reduced graph. Techniques based on “transitions step” are proposed for different properties classes. - For timed systems, time constraints can produce explosion of the exploration. This thesis proposes to compute an over-approximation of the system, in order to build a smaller behavior graph. The property is checked on the over-approximation. If the analysis of the over-approximation doesn't allow to conclude, the system behavior is checked, guided by results founded on the over-approximation.
Abstract FR:
La vérification formelle de systèmes concurrents temps réels se heurte au problème de l'explosion du nombre d'états à explorer. Ce problème connu sous le nom ``d'explosion combinatoire'' à plusieurs causes. Cette thèse s'intéresse à deux d'entre-elles. Pour lutter contre l'explosion due à la représentation du parallélisme par l'entrelacement d'actions, cette thèse propose des techniques basées sur l'approche des ordres-partiels pour construire un graphe réduit. Pour exploiter les ordres-partiels, les techniques proposées utilisent la construction de " pas de transitions " afin de limiter le nombre d'états explorés. Différentes constructions des " pas de transitions " sont proposées en fonction de la classe de propriétés que l'on souhaite préserver (Blocages, Équivalence de traces, LTL). Pour lutter contre l'explosion due aux contraintes temporelles, cette thèse propose une approche par sur-approximation du comportement. L'objectif est d'avoir un graphe abstrait du comportement de la sur-approximation plus petit que celui du système. Comme classiquement, les techniques d'abstractions permettent d'obtenir une procédure de décision semi-effective. Lorsque l'analyse de la sur-approximation ne permet pas de conclure, la thèse propose une méthode effective permettant de conclure pour les formules de LTL: le système est analysé, guidé par les résultats obtenus sur la sur-approximation. Cette thèse présente les algorithmes de ces différentes techniques de réduction et l'outil tina (http://www. Laas. Fr/tina) dans lequel ils ont été implémentés.