Abstract:
The schedulability analysis of real-time systems is challenged by the state space complexity of such systems. It is difficult to develop concrete state space models that can be used to verify the schedulability of real-time systems. This thesis solves the state space complexity problem by means of a new abstraction technique that enables an automated and efficient verification of schedulability properties of real-time task sets. The technique is applied to task queues under the {FIFO and EDF scheduling policies. The approach is based on the spotlight abstraction principle. The novel spotlight abstraction approach partitions the scheduler task queue into a `spotlight' and a `shade'. A small number of tasks that appear to a specified depth at the front of the queue and will be executed in the near future are placed in the spotlight. The shade contains the remaining tasks at the back of the queue which is executed only after the spotlight tasks have been processed. A timed automaton is generated from the spotlight to form an abstract model of the concrete system. The schedulability analysis of the spotlight is performed whereby the behaviour of the shade is summarised and the partial schedulability result for the spotlight tasks is saved for later re-use in the subsequent iterations. In each iteration, if the result is still inconclusive and there still exist tasks in the shade, more tasks are brought from the shade into the spotlight, with which the model checker can proceed. The iterations are continued until a decisive schedulability result (yes or no) is obtained. A new tool, called TVMC, that implements the spotlight abstraction-based model checking approach has been developed. An experimental performance evaluation of the abstraction-based TVMC against model checking without abstraction is presented. Empirical results showed that the execution times of the abstraction-based TVMC were faster than the ones of the approach without abstraction. Moreover, the spotlight abstraction TVMC handled larger task sets whereas the non-abstraction case failed to verify task sets with sizes greater than six due to state explosion. This work also presents an experimental comparison of TVMC against established tools: Timestool and the Uppaal platform based RTLib. TVMC was able to cope with the state explosion problem considerably better than Timestool and RTLib since it was able to handle significantly larger task sets and to finish the analysis in a similar amount of run-times.
