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
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;
Conference_Titel :
Design, Automation and Test in Europe Conference and Exhibition, 2002. Proceedings
Print_ISBN :
0-7695-1471-5
DOI :
10.1109/DATE.2002.998390