Formal Architecture Specification for Time Analysis

WCET calculus is nowadays a must for safety critical systems. As a matter of fact, basic real-time properties rely on accurate timings. Although over the last years, substantial progress has been made in order to get a more precise WCET, we believe that the design of the underlying frameworks deserve more attention. In this paper, we are concerned mainly with two aspects which deal with the modularity of these frameworks. First, we enhance the existing language Sim-nML for describing processors at the instruction level in order to capture modern architecture aspects. Second, we propose a light DSL in order to describe, in a formal prose, architectural aspects related to both the structural aspects as well as to the behavioral aspects