Text size
  • Small
  • Medium
  • Large
Contrast
  • 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

    AUTHORS

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

    ABSTRACT

    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.

    PAPER FORMATS

    PDF filePDF Version of this Paper (267kb)