DocumentCode :
2090709
Title :
Runtime analysis of synchronous programs for low-level real-time verification
Author :
Logothetis, G. ; Schneider, K. ; Metzler, C.
Author_Institution :
Inst. of Comput. Design & Fault Tolerance, Karlsruhe Univ., Germany
fYear :
2003
fDate :
8-11 Sept. 2003
Firstpage :
211
Lastpage :
216
Abstract :
Synchronous programming languages are well-suited for the implementation and verification of real-time systems. The main benefit for the estimation of real-time constraints is thereby that the macro steps provided by the semantics of synchronous languages can be directly used as building blocks for runtime analysis. We describe a new approach to determine the execution times of the macro steps of a synchronous program with respect to given microprocessors and generate real-time formal models endowed with notions of physical time for formal verification purposes. The execution times are exact, since we consider all possible input sequences.
Keywords :
binary decision diagrams; program verification; programming language semantics; real-time systems; BDD; formal models; formal verification; low-level real-time verification; macro step execution time; microprocessors; real-time constraints; real-time systems; synchronous language semantics; synchronous program runtime analysis; synchronous programming languages; timed Kripke structures; Computer architecture; Computer languages; Computer science; Fault tolerance; Integrated circuit modeling; Microprocessors; Performance analysis; Real time systems; Runtime; Synchronous generators;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Integrated Circuits and Systems Design, 2003. SBCCI 2003. Proceedings. 16th Symposium on
Print_ISBN :
0-7695-2009-X
Type :
conf
DOI :
10.1109/SBCCI.2003.1232831
Filename :
1232831
Link To Document :
بازگشت