Aller au contenu principal
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