<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> / Thesis / Doctor of Philosophy (PhD)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/19727 |
| Date | 08 1900 |
| Creators | Hu, Xiayong |
| Contributors | Lawford, Mark, Wassyng, Alan, Software Engineering |
| Source Sets | McMaster University |
| Language | English |
| Detected Language | English |
Page generated in 0.0022 seconds