Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Transformation of MTCCS into an Extension of Timed Automata

    1st BCS-FACS Northern Formal Methods Workshop

    Ilkley, UK. 23rd - 24th September 1996


    R.F. Lutje Spelberg & W.J. Toetenel


    This paper presents results from work in progress on finding a method for specification and formal verification of realtime 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 XTGraphs, an extension of timed automata that allows the symbolic description of data.

    This paper discusses the specification language MTCCS and its translation to XTGraphs.


    PDF filePDF Version of this Paper (267kb)