Présentation
|
|
|
|
|
Nous étudions la vérification de propriétés TCTL dans les réseaux de Petri temporels à chronomètres (SwPN), en utilisant une sémantique temps discret, puisque la vérification de propriété TCTL en temps dense est non décidable
Nous étudions les automates temporisés et la propriété de non interférence. Nous voulons développer une méthode qui, à partir d'un automate A, génère un contrôleur C tel que l'automate A|C soit non interférant. Un système non interférent est un système pouvant être utilisé par des utilisateurs de haut niveau et de bas niveau, tel que les utilisateurs de bas niveau ne soient pas en mesure de deviner qu'une action de haut niveau a été effectuée.
Romeo est un outil permetant l'analyse des réseaux de Petri T-temporels ainsi que celle d'une de leur extension à l'ordonnancement. Il permet de calculer l'espace d'état, via 2 modules de calcul codés en C++, et dispose d'une interface graphique, codée en TCL/TK.
