A formal technique to analyze real-time systems

Author

Wang, Ji ; Chen, Huowang

Author_Institution

Dept. of Comput. Sci., Changsha Inst. of Technol., Hunan, China

fYear

1993

fDate

1-5 Nov 1993

Firstpage

180

Lastpage

185

Abstract

A technique to analyze the temporal properties of real-time systems is presented in this paper. In our framework, the behavior of the system under development, which is modeled in an extension of Statecharts called Statecharts+, is captured by the underlying computational model, Timed Automata. On the basis of the operational semantics defined for arbitrary time domains, we present a formal translation technique to compile the real-time system specification into Timed Automata. Therefore, model checking of real-time properties can be applied to the automatic analysis of real-time systems

Keywords

automata theory; computational linguistics; formal specification; program compilers; program interpreters; real-time systems; systems analysis; temporal logic; Statecharts+; Timed Automata; arbitrary time domains; automatic analysis; compile; computational model; formal translation technique; model checking; operational semantics; real-time systems; specification; temporal properties; Automata; Computational modeling; Computer applications; Computer science; Concurrent computing; Embedded system; Process control; Real time systems; Software engineering; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 1993. COMPSAC 93. Proceedings., Seventeenth Annual International

Conference_Location

Phoenix, AZ

Print_ISBN

0-8186-4440-0

Type

conf

DOI

10.1109/CMPSAC.1993.404194

Filename

404194