A Distributed Algorithm for the Validation of Timed State Machines
Résumé
In this paper, we propose an a priori validation technique for time critical systems modelized thanks to timed automata. We validate the model of a given system using a hybrid method combining exhaustive exploration and simulation. For critical parts of the state machine, the exhaustive exploration produces a deterministic proof and a symbolic computation of the resulting clocks and constraints with regard to the initial ones. We can perform simulations of the complete state machine substituting these critical parts with the corresponding symbolic computation. In this paper, we propose an algorithm to automatically partition the automata into independent parts. Therefore, it is possible to parallelize the exhaustive analysis. || Dans ce papier, nous proposons une technique de validation a priori pour les systèmes temps critiques modélisés par des automates temporisés. Nous validons le modèle d'un système en utilisant une méthode hybride qui combine l'exploration exhaustive et la
Loading...