An-Najah Staff

A complementary verification method for real-time application with dynamic task structure has been developed. Here the real-time application is developed by means of Model-Driven Engineering. The basic verification technique is given by model checking. However, the model checking is executed at run-time whenever some reconfiguration of the task set takes place. Instead of exploring the entire state space of the model to be checked, only a partial state space at model level covering the execution trace of the checked task is explored. This on-line model checking can be seen as an extension to the traditional schedulability acceptance test which is needed anyway in systems with dynamic task set. Therefore this runtime verification is implemented as a service of the underlying operating system. In this paper we describe this method in general, explain some design and implementation decisions and provide experimental results.