Issue No. 06 - November/December (2011 vol. 37)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2011.4
Laura Carnevali , Università di Firenze, Firenze
Lorenzo Ridi , Università di Firenze, Firenze
Enrico Vicario , Università di Firenze, Firenze
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.
Real-time systems, safety-critical SW components, SW life cycle, V-Model, preemptive Time Petri Nets, symbolic state space analysis, model driven development, automated model transformation, automated code generation, Execution Time estimation, real-time testing, test case selection and execution, coverage analysis.
E. Vicario, L. Carnevali and L. Ridi, "Putting Preemptive Time Petri Nets to Work in a V-Model SW Life Cycle," in IEEE Transactions on Software Engineering, vol. 37, no. , pp. 826-844, 2011.