Scheduling analysis based on model checking for multiprocessor real-time systems

Real-time systems (RTS) are omnipresent in several domains. The trend is to use multiprocessor architecture to satisfy the timing constraints of such systems. The model-checking methods have proven to be useful for making the development process reliable at a high abstraction level. Based on this approach, the present paper proposes a new technique for scheduling analysis of a partitioned multiprocessor RTS. Starting from a model with dynamic priority time Petri Nets modeling the system, we have proposed a generation of a reduced states graph. Thus, through the properties of the graph the schedulability is checked. Our approach provides an implementation of a Partition Checker tool, which produces an affirmation of the schedulability or a counterexample in the case of non-schedulable system to reduce the SW/HW space exploration.