A generalized approach to the analysis of real-time computer systems
Andre N. Fredette · 1993
This dissertation aims to close the gap between real-time schedulability analysis approaches and formal specification and verification techniques for real-time. We develop a generalized approach to schedulability analysis that is mathematically founded in a process algebra called RTSL. RTSL is used to describe the functional behavior, timing behavior, timing constraints (or deadlines), and scheduling discipline for real-time systems. Within the framework of our approach, we formally model the most commonly used real-time scheduling disciplines and provide a capability for modeling others. The formal semantics of RTSL uses the scheduling discipline as a parameter and allows the reachable state space of any system to be automatically generated and searched for timing exceptions. We provide a generalized schedulability analysis algorithm to perform this state-based analysis. The RTSL approach is less restrictive than existing real-time schedulability analysis approaches with respect to the kinds of processes and time constraints that can be specified and analyzed. Within RTSL, time constraints can be specified for a whole process, as well as for any component of a process. Exception handlers can also be specified and analyzed. RTSL has a basic synchronization primitive with which most general forms of inter-process cooperation can be modeled. The ability to specify more general types of processes provides greater flexibility to real-time system developers while maintaining the desired property of verifiability of schedulability. The modularity of the scheduling discipline in RTSL provides a common process model that can be used to compare the effectiveness of different scheduling disciplines on a given system. Finally, RTSL can serve as a theoretical foundation for developing and analyzing new and existing real-time scheduling approaches. A common limitation with state-based analysis approaches for real-time systems is that they can only be used for systems that operate in a discrete time domain. We show how this obstacle may be overcome by identifying a class of finitely analyzable continuous-time systems for which state-based analysis is practical and then showing that many common continuous-time systems are finitely analyzable.