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