Specification and verification of timed automaton using meta-modeling and graph grammars

Timed automaton is considered as one of the most powerful formalisms for the specification and verification of critical systems having temporal aspects. However, they lack a graphical environment to create and analyze timed automaton models. In this paper, we propose an approach based on the combined use of Meta-Modeling and Graph Grammars to automatically generate a visual Modeling tool for timed automaton specification. In our approach, the UML Class diagram formalism is used to define a meta-model of timed automaton specification. From this meta-model, ATOM³ automatically generates a visual tool to build timed automaton models. We also proposed a graph grammar to generate the textual code following the UPAAL model checker´s syntax. This allows in one hand the user to avoid the errors when this description is done manually and in the other hand to use UPPAL model checker for verifying some properties. An example illustrates the feasibility and validity of the proposed approach.