Hierarchical Timed Abstract State Machines for WCET Estimation

In this paper we present an extension of the Abstract State Machines suited for the modelling of complex processors in the context of system verification. Hard real-time systems use evermore elaborate processors in an environment where certification rules are getting tighter and more explicit regarding the verification of software. The goal of our model is to provide a base for worst-case execution time estimation, providing abstraction capabilities that enable the scaling of analysis. The core difference between our model and the others is that we define time as a mean to enable time accurate runs and components at different abstraction levels that can be dynamically chosen during the execution while staying the closest possible to the original mathematical foundation. The model is able to choose the best suited component definition in order to respond to factors like information on data values. The time extension takes into account the fact that actions are not instantaneous which is essential for real-time systems. Adaptable precision and separation of the analysis from the model of the processor, make our model suited for worst-case execution time.