Integrating astd in the Rodin platform
Paul Amar, Marc Frappier, Cécile Lartaud, Jérémy Milhau · 2010
The astd notation is a graphical modeling language associated with formal semantics. It can be used to describe process and information system (IS) behaviors. By executing such specification with an interpreter, an IS controller can verify that executed actions comply with the model of the formal system. astd main disadvantage is currently its lack of tools. Ongoing works try to address this issue. The Algebraic State Transition Diagrams notation, or astd [3] offers a graphical and formal representation for processes. Based on automata, Statecharts and eb process algebra, the astd notation combines advantages of each approaches. But in practice, a designer has to write a text representation of an astd structure in order to use it with iastd [5], an interpretor for astd. Rodin Platform iASTD eASTD astd ProB Rodin Provers .bcm .bcc Translation via EMF Graphical animation Control emf iASTD Graphical edition Proofs MC & Animation