Title
Semi-automatic derivation of timing models for WCET analysis
Abstract
Embedded systems are widely used for supporting our every day life. In the area of safety-critical systems human life often depends on the system's correct behavior. Many of such systems are hard real-time systems, so that the notion of correctness not only means functional correctness. They additionally have to obey stringent timing constraints, i.e. timely task completion under all circumstances is essential. An example for such a safety-critical system is the flight control computer in an airplane, which is responsible for stability, attitude and path control. In order to derive guarantees on the timing behavior of hard real-time systems, the worst-case execution time (WCET) of each task in the system has to be determined. Saarland University and AbsInt GmbH have successfully developed the aiT WCET analyzer for computing safe upper bounds on the WCET of a task. The computation is mainly based on abstract interpretation of timing models of the processor and its periphery. Such timing models are currently hand-crafted by human experts. Therefore their implementation is a time-consuming and error-prone process. Modern processors or system controllers are automatically synthesized out of formal hardware specifications like VHDL or Verilog. Besides the system' functional behavior, such specifications provide all information needed for the creation of a timing model. But due to their size and complexity, manually examining the sources is even more complex than only looking at the processor manuals. Moreover, this would not reduce the effort nor the probability of implementation errors. To face this problem, this paper proposes a method for semi-automatically deriving suitable timing models out of formal hardware specifications in VHDL that fit to the tool chain of the aiT WCET analyzer. By this, we reduce the creation time of timing models from months to weeks.
Year
DOI
Venue
2010
10.1145/1755888.1755899
Proceedings of the 2007 ACM SIGPLAN/SIGBED conference on Languages, compilers, and tools for embedded systems
Keywords
Field
DocType
worst case execution time,vhdl,embedded system,upper bound
Worst-case execution time,Abstract interpretation,Computer science,Correctness,Static analysis,Real-time computing,Formal specification,Verilog,VHDL,Hardware description language
Conference
Volume
Issue
ISSN
45
4
0362-1340
Citations 
PageRank 
References 
4
0.42
17
Authors
2
Name
Order
Citations
PageRank
Marc Schlickling11447.27
Markus Pister217110.84