A Modeling Language for Timed Automata

Sammanfattning: This work details the design and implementation of a modeling language for timed automata. The primary intended use of the language TML is as an interface to controller synthesis system m2mc, which is being developed in a current KTH/Chalmers research project. TML is evaluated by a qualitative comparison with the modeling languages of two well-known model checking tools: Uppaal and Kronos. Two example systems (Fischer’s mutual exclusion protocol and CSMA/CD) are implemented in all three languages, to discover the relative merits of each language. Although not as feature rich as Uppaal, TML brings some new language features which are found to be potentially useful for modeling timed automata systems. These features are largely adopted from the general graph description language Dot, used by programs in the Graphviz software package. As m2mc is still in early development and liable to change, an intermediate JSON representation for timed automata is defined. A compiler targeting this intermediate representation is implemented using Miking, a new compiler tool under development in a separate KTH project. Further compilation from JSON to Uppaal is implemented as a proof of concept.