Algebraic State-Transition Diagrams 

ASTD (Algebraic State-Transition Diagrams) is a graphical system modeling language that combines hierarchical state machines (à la Statechart) with process algebra operators à la CSP (Communicating Sequential Processes).  A recent extension, called TASTD, allows to model time and to take into account temporal constraints of real-time systems, while keeping an algebraic approach.  TASTD supports all the usual temporal operators found in languages like Stateflow, Stateful Timed CSP and UPPAAL.  ASTD and TASTD specifications can be built with the graphical editor eASTD and translated into efficient C++ programs with the cASTD compiler. 

ASTDs have be used in various application areas. 

A translation to B and Event-B has been defined [IFM2010, Fayolle2017] as well as a refinement relation [Refinement2015, UML&FM2012, FAC2014].  An iASTD interpreter was implemented [Salabert2011], but it is no longer supported. 

The following projects are in progress concerning ASTDs 

  • PhD project of Chaymae el Jabri: Definition of ASTD specification patterns in intrusion and anomaly detection 
  • PhD project  of Diego de Azevedo Olivera: TASTD, a temporal extension of ASTDs 
  • PhD project  of Alex Rodrigue Ndouna: Integration of CCSL in ASTD 
  • Master project of Quelen Cartellier: Proof of invariants in ASTD