Putting preemptive Time Petri Nets to work in a V-Model SW life cycle

Preemptive Time Petri Nets (pTPNs) support modeling and analysis of concurrent timed SW components running under fixed priority preemptive scheduling. The model is supported by a well-established theory based on symbolic state space analysis through Difference Bounds Matrix (DBM) zones, with specific contributions on compositional modularization, trace analysis, and efficient overapproximation and cleanup in the management of suspension deriving from preemptive behavior. In this paper, we devise and implement a framework that brings the theory to application. To this end, we cast the theory into an organic tailoring of design, coding, and testing activities within a V-Model SW life cycle in respect of the principles of regulatory standards applied to the construction of safety-critical SW components. To implement the toolchain subtended by the overall approach into a Model Driven Development (MDD) framework, we complement the theory of state space analysis with methods and techniques supporting semiformal specification and automated compilation into pTPN models and real-time code, measurement-based Execution Time estimation, test case selection and execution, coverage evaluation.