Logic Verification of Real Time Systems in the Context of the Maximality Semantics

The verification by model checking has been widely studied for the timed automata model. This technique is used for automatically verifying correctness properties of finite-state systems based on interleaving semantics. Therefore, the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). The state space of transitions system associated to a durational actions timed automata model is infinite. To verify this model, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics-based verification provides new class of properties related to simultaneous progress of actions at different states. A method that is based on another abstraction of the state space, uses a symbolic representation called zone. We have designed a new zone graph under the maximality semantics, named Maximality-based Zone Graph (MZG), for describing symbolic execution of daTA. An algorithm based on the symbolic and an on-the-y forwards reachability analysis algorithm for durational actions timed automata is proposed. We use Difference Bounded Matrices (DBM), which are one of the most effective data structures for representing zones.La vérification par model checking a été largement étudiée pour le modèle des automates temporisés. C’est une technique de validation pour vérifier automatiquement la correction des propriétés des systèmes états finis, qui sont basées sur la sémantique d’entrelacement, car les actions sont supposées instantanées. Pour échapper l’hypothèse d’atomicité temporelle et structurelle des actions, nous utilisons le modèle des automates temporisés avec durées d’actions (daTA). Ce modèle est basé sur la sémantique de maximalité. Les propriétés vérifier sont exprimées, en utilisant la logique temporelle arborescente temporisée (TCTL). L’espace d’état du système de transitions associé à un automate temporisé avec durées d’actions, est infini. Pour vérifier ce modèle, le graphe des régions basé sur la maximalité (MRG) est déni et une adaptation de l’algorithme de model checking est proposée. L’utilisation de la vérification basée sur la sémantique de maximalité fournit une nouvelle classe de propriétés liées au progrès simultané des actions dans les différents états. Une méthode qui est basée sur une autre abstraction de l’espace d’état, utilise une représentation symbolique appelée zone. Nous avons connu un nouveau graphe des zones sous la sémantique de maximalité, nommé graphe des zones basé sur la maximalité (MZG), pour décrire l’exécution symbolique du daTA. Un algorithme d’analyse d’accessibilité en avant la volée, basé sur la représentation symbolique, pour les automates temporisés avec durées d’actions est proposé. Nous utilisons une structure de données permettant d’implémenter facilement les zones, en l’occurrence les matrices différences bornées (DBM)