Transformation of MTCCS into an Extension of Timed Automata

This paper presents results from work in progress on finding a method for specification and formal verification of real-time concurrent systems incorporating a non-trivial data component. To model such systems, we use the real-time process algebra MTCCS, a Timed CCS variant, enhanced with a data manipulation model. Our verification method is based on the dual-language approach in which temporal logic is used to state properties over system models defined in some operational specification language. To obtain representations that allow the application of model checking, MTCCS specifications are transformed into XT Graphs, an extension of timed automata that allows the symbolic description of data. This paper discusses the specification language MTCCS and its translation to XTGraphs.