Using transformations for proving timing and fault-tolerance properties of programs

Mathai Joseph

(University of Warwick)

Let program P be represented by a predicate defining its initial condition and a set of atomic state transition operations. Assume that faults in the execution environment are modelled by a program F consisting of a set of atomic"fault" operations. Then the effect of faults on the execution of P can be modelled as a transformation of P into FF(P,F). In a similar way, if P is executed on a set Pr of processors under a scheduler S, then this implementation of P can be represented as a transformation I(P) and the deadlines of P will be satisfied if they are satisfied by I(P).

This talk will mainly consider the verification of timing properties using transformations. I will show how real-time program specification and schedulability, which have traditionally been studied in different analytical frameworks, can be considered in the same framework and how a scheduler can be considered generically in terms of a scheduling policy.
Wednesday 8th February 1995, 14:30
Seminar Room 322
Department of Computer Science