Timing analysis of assembler code control-flow paths

Timinganalysis of assembler code is essential to achieve the strongest possible guarantee of correctness for safety-critical, real-time software. Previous work has shown how timingconstrain ts on controlflow paths through high-level language programs can be formalised using the semantics of the statements comprisingthe path. We extend these results to assembler-level code where it becomes possible to not only determine timingconstrain ts, but also to verify them against the known execution times for each instruction. A minimal formal model is developed with both a weakest liberal precondition and a strongest postcondition semantics. However, despite the formalism’s simplicity, it is shown that complex timingb ehaviour associated with instruction pipeliningand iterative code can be modelled accurately.

Refining exceptions using King and Morgan's exit construct

In this paper we discuss the refinement of exceptions. We extend the Guarded Command Language normally used in the refinement calculus, with a simple exception handling statement, which we model using King and Morgan's exit statement (1995). We derive some variants of King and Morgan's refinement laws for their exit statement, and illustrate the approach with an example of a refinement of a simple program.