TChecker

Description
TChecker est un outil de vérification de modèles temporisés open-source. Il est développé en C++17 et propose une bibliothèque de classes permettant de décrire un système temporisé, de calculer la l'automate temporisé correspondant et sa sémantique sous forme symbolique et d'y appliquer des algorithmes de vérification de propriétés. Un outil en ligne de commandes est directement utilisable.

TChecker est destiné à servir de plateforme d'expérimentation de nouvelles structures de données et algorithmes pour la vérification et la synthèse de systèmes temporisés. L'objectif du projet est d'implémenter dans cet outil l'état de l'art des algorithmes de vérification des systèmes temporisés, d'évaluer leurs performances et de les mettre à disposition de la communauté.
Domaines d'utilisation
Modélisation et vérification de systèmes temporisés
Contributeurs LaBRI
Frédéric Herbreteau, Gérald Point
Dépôt du code source
https://github.com/ticktac-project/tchecker
Licence(s) de distribution
MIT License
OS supportés
Linux, MacOS
Plus d'informations
https://tchecker.labri.fr

Précédent