A timed automata semantics for real-time UML specifications

Author

Toetenel, Hans ; Roubtsova, Ella ; van Katwijk, Jan

Author_Institution

Fac. of Inf. Technol. & Syst., Delft Univ. of Technol., Netherlands

fYear

2001

fDate

2001

Firstpage

88

Lastpage

95

Abstract

We introduce extensions of the UML class, object and statechart diagrams and define the semantics of the UML extensions by means of extended timed graphs (XTG), a timed automata variant. This approach opens the possibility to specify properties of the UML specifications using the timed computation tree logic. The transformation of the UML-specification into XTG allows the verification the system by model checking using the LPMC model checker tool, which uses XTG as its input language.

Keywords

automata theory; formal specification; graph theory; object-oriented languages; program verification; real-time systems; specification languages; UML; Unified Modeling Language; XTG; extended timed graphs; formal specification; formal verification; object oriented language; real-time systems; timed automata semantics; Application software; Automata; Clocks; Computer science; Formal verification; Mathematics; Object oriented modeling; Real time systems; Tree graphs; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Human-Centric Computing Languages and Environments, 2001. Proceedings IEEE Symposia on

Print_ISBN

0-7803-7198-4

Type

conf

DOI

10.1109/HCC.2001.995243

Filename

995243