Validation de spécifications RT-LOTOS : une interface vers l'outil TINA

Abstract

RT-LOTOS est une algèbre de processus temporisée supportée par RTL, outil de validation formelle utilisant l'analyse d'accessibilité. La recherche de meilleures performances en termes d'exploration de l'espace d'états et le besoin d'étendre les classes de propriétés vérifiées, ont motivé le développement d'une interface entre RTL et l'analyseur de réseaux de Petri temporels TINA. Cette interface repose sur des schémas de traduction de RT-LOTOS vers les RdPT. Ces schémas ont fait l'objet d'une preuve. Cet article met l'accent sur les premiers résultats expérimentaux obtenus avec RTL2TPN, un traducteur qui a vocation à intégrer la chaîne d'outils développés pour le profil UML temps réel TURTLE (Timed UML and RT-LOTOS Environment).