An Abstraction-Refinement Theory for the Analysis and Design of concurrent Real-Time Systems
Philip Kurtin is a PhD student in the research group Computer Architecture for Embedded Systems. His supervisor is prof.dr.ir. M.J.G. Bekooij from the faculty Faculty of Electrical Engineering, Mathematics and Computer Science.
Concurrent real-time systems with shared resources belong to the class of safety-critical systems. For such systems it is required to determine both temporally and functionally conservative guarantees, whereas estimates and approximations are usually not sufficient.
However, the growing complexity of real-time systems makes it more and more challenging to apply standard techniques for their analysis. Especially the presence of both cyclic data dependencies (which can occur due to feedback loops, but also due to the usage of FIFO buffers) and cyclic resource dependencies (i.e. resource dependencies that are opposed to the flow of data) makes many related analysis approaches inapplicable. Finally, also the usage of Static Priority Preemptive (SPP) scheduling and its accompanying scheduling anomalies (temporal non-monotonicities) further impede the employment of many “classical” analysis techniques.
To address this growing complexity and to be able to give guarantees nevertheless we consequently need to reduce complexity in a both temporally and functionally conservative manner. We have to be careful, however, because every complexity reduction entails a reduction of accuracy, they are two sides of the same medal.
We identify two different methods to reduce complexity in a conservative way. First, we can reduce complexity by reducing the “entropy” of analysis models by means of abstraction (as opposed to refinement), such that the amount of information contained within the models is lowered. And second, we can also reduce complexity by a reduction of analysis technique “effectiveness”, i.e. we apply simpler, but coarser techniques on the same models. Given these two levers, we aim to seamlessly trade off between complexity and accuracy.
However, there are two significant restrictions that prevent us from making such trade-offs. For one, there is no abstraction-refinement theory that supports the abstraction of non-deterministic, non-monotone, cyclic real-time systems to deterministic, monotone and (if required) acyclic analysis models. And given suitable analysis models, there is only a very coarse analysis technique for the analysis of such models, which prevents trading off accuracy and complexity on the effectiveness scale.
For that matter we present an abstraction-refinement theory for real-time systems in the first part of this thesis. We introduce a timed component model that is defined in such a generic way that both real-time system implementations and any kinds of analysis models for such applications can be expressed therein. The two main constructs of the component model are streams, which are finite or infinite sequences of events (i.e. pairs of timestamps and values), as well as the components themselves that transform input streams to output streams via mathematical relations. We prove various properties for this component model, such as the automatic lifting of input acceptance (i.e. the acceptance of input streams) from component to graph level.
Thereafter, we devise three different abstraction-refinement theories for the timed component model, exclusion, inclusion and bounding. Exclusion can be used to remove unconsidered corner cases such as potential malfunctions that are outside the scope of analysis, resulting in a “model of reality”. Inclusion abstraction allows for the substitution of uncertainty in the model of reality with non-determinism and inclusion refinement enables to derive implementations for which no specific events need to occur, as long as the events take place within certain ranges. In contrast, bounding abstraction permits to replace non-determinism with determinism, enabling the creation of efficiently analyzable models that can be used to give temporal or functional guarantees on non-deterministic and non-monotone implementations, whereas bounding refinement allows to create implementations that adhere to temporal or functional properties of deterministic specification models. We further differ between best-case and worst-case bounding, which is required for applications in which jitter plays a major role.
In the second part of the thesis we use exclusion, inclusion and bounding abstractions to construct several analysis models from concurrent real-time systems with shared resources and SPP scheduling. For SPP scheduling it is required to determine so-called enabling rate characterizations of tasks, as otherwise the interference of higher priority tasks on lower priority ones cannot be bounded. Moreover, the presence of cyclic data and resource dependencies creates a mutual dependency between the schedules of tasks (their enabling and finish times) and the interference due to resource dependencies, which is the reason why all our presented analysis approaches are iterative.
For the determination of schedules we make use of two dataflow models that we define as best-case and worst-case bounding abstractions of the analyzed real-time systems. With the best-case models we compute periodic lower bounds on the schedules of tasks, while upper bounds are determined with the worst-case models. These lower and upper bounds can be used in so-called response time analysis models, which are inclusion abstractions of the underlying real-time systems, to calculate upper bounds on the jitters of higher priority tasks that are suitable to determine so-called period-and-jitter interference characterizations. With these characterizations we can compute maximum response times of tasks, i.e. differences between maximum enabling and finish times considering interference, which results in the aforementioned coarse analysis approach.
To improve effectiveness and therewith accuracy of the period-and-jitter analysis we first propose to combine the aforementioned interference characterization with an explicit consideration of cyclic data dependencies that are the result of both feedback loops and FIFO buffers. We show that the consideration of such dependencies to limit interference results in a significantly higher analysis accuracy. Based on this observation, we attempt to exploit this interference-limiting effect even more by introducing an iterative buffer sizing which does not only analyze, but actually optimizes the underlying real-time systems. On top of that, we discuss the introduction of so-called synchronization edges that can be seen as non-functional FIFO buffers and are placed directly between higher and lower priority tasks, enabling a further exploitation of cyclic dependencies to restrict interference. Lastly, we replace the coarse period-and-jitter interference characterization with execution intervals, resulting in an even higher analysis accuracy.
In our last analysis approach we do not only aim at increasing analysis accuracy, but also at increasing analysis applicability by enabling the support of real-time systems with tasks consisting of multiple phases and operating at different rates. We show that this approach is not only suitable for inherently multi-rate, multi-phase applications, but also for single-rate, single-phase ones because the modeling with phases can be also used to relax the rather strict requirements on the underlying hardware platforms imposed by the aforementioned approaches. With a modification of this approach we further enable the analysis of applications with multiple shared resources.
Finally, we also discuss simulation in the context of our modeling framework. We present the so-called HAPI simulator, which is capable of simulating any kinds of concurrent real-time systems with shared resources. Among other use-cases, we also show that HAPI can be used to falsify erroneously determined analysis results. The latter is enabled by the fact that we can apply HAPI on the same models that we also use for analysis, which is a significant distinction to related approaches.
In the first part of this thesis we show with various case studies the applicability of our abstraction-refinement theory and the underlying component model for many kinds of discrete-event systems and analysis models. In the second part we use a WLAN transceiver application as an ongoing case study to demonstrate that all our improvements, i.e. consideration of cyclic data dependencies, iterative buffer sizing, synchronization edges, execution intervals and multi-phase analysis, result in a significant improvement of analysis accuracy.
