Transformation of MTCCS into an Extension of Timed Automata | Zendy

Ronald Lutje Spelberg | Zendy; Hans Toetenel | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Transformation of MTCCS into an Extension of Timed Automata

Author(s) -

Ronald Lutje Spelberg,

Hans Toetenel

Publication year - 1996

Publication title -

electronic workshops in computing

Language(s) - English

Resource type - Conference proceedings

ISSN - 1477-9358

DOI - 10.14236/ewic/fa1996.16

Subject(s) - computer science , automaton , programming language , model checking , specification language , extension (predicate logic) , transformation (genetics) , temporal logic , model transformation , process calculus , component (thermodynamics) , formal specification , formal verification , theoretical computer science , language of temporal ordering specification , artificial intelligence , physics , consistency (knowledge bases) , thermodynamics , biochemistry , chemistry , gene

This paper presents results from work in progress on finding amethod 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 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research