DocumentCode
2588755
Title
Verifying safety-critical timing and memory-usage properties of embedded software by abstract interpretation
Author
Heckmann, Reinhold ; Ferdinand, Christian
Author_Institution
AbsInt Angewandte Informatik GmbH, Saarbrucken, Germany
fYear
2005
fDate
7-11 March 2005
Firstpage
618
Abstract
Static program analysis by abstract interpretation is an efficient method to determine the properties of embedded software. One example is value analysis, which determines the values stored in the processor registers. Its results are used as input to more advanced analyses, which ultimately yield information about the stack usage and the timing behavior of embedded software.
Keywords
embedded systems; formal verification; program diagnostics; program processors; systems analysis; timing; abstract interpretation; embedded processor; embedded software; formal verification; memory-usage properties verification; processor registers; safety-critical timing verification; stack usage; static program analysis; value analysis; Application software; Automatic control; Concrete; Embedded software; Information analysis; Machinery; Real time systems; Registers; Runtime; Timing;
fLanguage
English
Publisher
ieee
Conference_Titel
Design, Automation and Test in Europe, 2005. Proceedings
ISSN
1530-1591
Print_ISBN
0-7695-2288-2
Type
conf
DOI
10.1109/DATE.2005.326
Filename
1395637
Link To Document