ASTD (Algebraic State-Transition Diagrams) [ISSE2008,TR-25] est un langage graphique de modélisation de systèmes permettant de combiner des machines à états hiérarchiques (à la Statechart) avec des opérateurs d’algèbre de processus à la CSP (Communicating Sequential Processes). Une extension récente, appelée TASTD, permet de modéliser le temps et de prendre en compte des contraintes temporelles des systèmes temps réel, tout en conservant une approche algébrique. Les TASTD supportent tous les opérateurs temporels usuels que l’on retrouve dans des langages comme Stateflow, Stateful Timed CSP et UPPAAL. Les spécifications ASTD et TASTD peuvent être construites avec l’éditeur graphique eASTD et traduites en programmes C++ efficaces avec le compilateur cASTD [Tidjon2020].
Les ASTDs peuvent être utilisés dans divers domaines d’application.
- Détection d’intrusion et d’anomalies [TASE2022, AINA2020, ICECCS2018]
- Contrôle d’accès [IJSSOE2011,ISSE2011]
- Système de contrôle : Hémodialyse [ABZ2016], Contrôle automatique de train (CBTC) [Fayolle2017], Contrôle des feux d’une voiture, Contrôleur de vitesse
- Système d’information [ICETE2011]
Un traduction vers B et Event-B a été définie [IFM2010, Fayolle2017] ainsi que qu’une relation de raffinement [Refinement2015, UML&FM2012, FAC2014]. Un interpréteur iASTD a été implémenté [Salabert2011], mais il n’est plus supporté.
Les projets suivants sont en cours concernant les ASTD
- Projet de doctorat Chaymae el Jabri : Définition de patrons de spécifications ASTD en détection d’intrusions et d’anomalies
- Projet de doctorat de Diego de Azevedo Olivera : TASTD, une extension temporelle des ASTD
- Projet de doctorat de Alex Rodrigue Ndouna : Intégration de CCSL dans les ASTD
- Projet de maitrise de Quelen Cartellier : Preuve d’invariants dans les ASTD