An Approach Based on Simulation and Verification for the Schedulability Analysis of Real-Time Systems

This paper proposes an approach to fixed-priority schedulability analysis of real-time (RT) systems which combines simulation and verification techniques. A RT tasking set is first abstracted by a Pre-emptive Time Petri Net (PTPN) model which makes it possible to specify the control structure and timing behavior of each task. A simulation tool can then be exploited to test schedulability and to estimate bounds on response times of tasks. Schedulability analysis is further investigated by exhaustive verification (model checking) using a translation of PTPNs to Timed Automata which relies on discrete-time. The verification work mainly consists in a refinement of the simulation results. In complex system models, though, when exhaustive verification can become hard in practical terms, simulation can anyway be applied to provide useful insights about schedulability. The paper demonstrates usefulness of the proposed approach through a concrete example.