@INPROCEEDINGS{Schlickling10,
  author = {Marc Schlickling and Markus Pister},
  title = {Semi-Automatic Derivation of Timing Models for {WCET} Analysis},
  booktitle = {LCTES '10: Proceedings of the 2010 ACM SIGPLAN-SIGBED conference on Languages, compilers, and tools for embedded systems},
  year = {2010},
  month = {April},
  publisher = {ACM},
  note = {To appear},
  location = {Stockholm, Sweden},
  subproject={R2},
  access={restricted},
  bibtex={schlickling.lctes10.bib},
  pdf={schlickling.lctes10.pdf},
  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
            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.},
}