Proving Implementability of Timing Properties with Tolerances

Abstract

<p> Many safety-critical software applications are hard real-time systems. They have stringent timing requirements that have to be met. We present descriptions of timing behaviors that include precise definitions as well as analysis of how functional timing requirements (FTRs) interact with performance timing requirements (PTRs), and how these concepts can be used by software designers. The definitions explicitly show how to specify timing requirements with tolerances on time durations. </p> <p> This thesis shows the importance of specifying both FTRs and PTRs, by revealing the fact that their interaction directly determines the final implementability of real-time systems. By studying this interaction under three environmental assumptions, we find that the implementability results of the timing properties are different in each environment, but they are closely related. The results allow us to predict the system's implementability without developing or verifying the actual implementation. This also shows that we can sometimes significantly reduce the sampling frequency on the target platform, and still implement the timing requirement correctly. </p> <p> We present a component-based approach to formalizing common timing requirements and provide a pre-verified implementation of one of these requirements. The verification is performed using the theorem proving tool PVS. This allows domain experts to specify the tolerance in each individual timing requirement precisely. The pre-verified implementation of a timing requirement is demonstrated by applying the method in two examples. These examples show that both the design and verification effort are reduced significantly using a pre-verified template. </p> <p> A primary focus of this thesis is on how to include tolerances on timing durations in the specification, implementation and verification of timing behaviors in hard real-time applications. </p>