Performance Analysis of Real-Time Task Systems using Timed Automata
Georgete Igna
Promotor: prof.dr. F.W. Vaandrager (RU)
Faculty of Science, Mathematics and Computer Science, RU
Radboud Universiteit Nijmegen
Date: 22 January, 2013.
Thesis: PDF
Summary
Computer systems are part of our daily life being included in various systems such as: home appliances, aircrafts, intelligent highway systems, and multimedia communication systems. As the complexity of today’s computer-based systems increases, the design methods that guarantee their correctness also need to be updated. Recently, we observe that industry tends to use formal verification tools more often in the design phase. They benefit, among others, from finding errors early. Formal verification is the process of proving the correctness of a system, represented as an abstract mathematical model, against a given property formally described with mathematical rigor. Examples of formal verification techniques are theorem proving, simulation, testing, and model checking.
The aim of this thesis is to help in the design of computer-based systems by using formal verification techniques, mainly model checking. An example of such a system is an Océ datapath, which we extensively analyze in this thesis. A datapath encompasses the complete trajectory of image data from source (e.g. a scanner) to target (e.g. a printer). Model checking is an automated verification technique that, given a model of finite-state system and a formal property, systematically checks whether the property holds in the model or not. The model checker used in this study is Uppaal. The language of Uppaal is based on timed automata, i.e. finite-state machines extended with real-valued variables called clocks, and extends them with additional features such as bounded integer variables, synchronization channels and user-defined functions.
In Chapter 2, we represent a datapath using three modeling approaches: timed automata, colored Petri nets and synchronous data flow graphs. The three models are configured to encode an Oce-specific problem where a set of concurrent jobs (i.e. applications) have to be scheduled on an architecture with limited resources. Uppaal, CPN Tools and SDF3 are used to derive schedules.
Chapter 3 presents an analysis of two concurrent jobs: one continuously occupying a datapath and the other with uncertain arrival times. This scenario is represented as a two-player timed game, and with Uppaal Tiga we seek acceptable trade-offs between the throughput of the continuous job and the latency of the other job.
In Chapter 4, we refine the timed automata model of the Océ datapath by adding scheduling rules specific to the Océ controller. This model is further analyzed with Uppaal for finding the worst case latency of a job that has uncertain arrival times in a setting where the system is processing in parallel an infinite stream of another competing job.
In Chapter 5, we define real-time task systems (RTTSs) as a general model for real-time systems. In this thesis, we assume that a job contains a finite set of tasks. The set of tasks is represented in an RTTS as a parametrized partial order (PPO), which has been introduced before to compactly represent large task graphs with repetitive behavior. Further, we present a subclass of PPOs that can be efficiently translated to timed automata. Lastly, we report on a series of experiments which demonstrates that models generated from the RTTS representation are more tractable than the handcrafted models of Chapter 2.
In Chapter 6, we scrutinize the validity of the schedules presented in the other chapters and obtained with Uppaal. The duration of some tasks in these schedules is over-approximated, which might make the schedules invalid if one assumes that idle components do not wait (so-called “non-lazy scheduling”) when executing tasks with the exact duration. For the schedules proven invalid, we investigate their robustness by slightly varying some task durations. Both validity and robustness analyses are performed with Z3, a satisfiability modulo theory solver. Since tasks run on physical machines, their duration cannot always be precisely known in advance, but is estimated. Therefore, it is important to study the robustness of these schedules when some preconditions are modified. The work in this chapter can be applied in such a situation.
Even though it required some expertise to model an Océ datapath efficiently, Uppaal has been shown valuable for the comparison of various design options.