DocumentCode :
2456740
Title :
Extending synchronous languages for generating abstract real-time models
Author :
Logothetis, G. ; Schneider, K.
Author_Institution :
Inst. for Comput. Design & Fault Tolerance, Karlsruhe Univ., Germany
fYear :
2002
fDate :
2002
Firstpage :
795
Lastpage :
802
Abstract :
We present an extension of synchronous programming languages that can be used to declare program locations irrelevant for verification. An efficient algorithm is proposed to generate from the output of the usual compilation an abstract real-time model by ignoring the irrelevant states, while retaining the quantitative information. Our technique directly generates a single real-time transition system, thus overcoming the known problem of composing several real-time models. A major application of this approach is the verification of real-time properties by symbolic model checking.
Keywords :
program compilers; program verification; programming languages; programming theory; real-time systems; symbol manipulation; abstract real-time model generation; compilation output; extended synchronous programming languages; irrelevant states; program location declaration; program verification; quantitative information retention; real-time model composition; real-time properties; single real-time transition system; symbolic model checking; Costs; Embedded system; Fault tolerance; Formal verification; Hardware; Real time systems; Safety; State-space methods; Synchronous generators; Time to market;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings
ISSN :
1530-1591
Print_ISBN :
0-7695-1471-5
Type :
conf
DOI :
10.1109/DATE.2002.998390
Filename :
998390
Link To Document :
بازگشت