Casting Preemptive Time Petri Nets in the Development Life Cycle of Real-Time Software

We describe a methodology for the construction of real-time tasking sets, which smoothly integrates a formal approach in both development and verification processes of the software life cycle. In the design stage, a timeline schema is used to specify concurrent processes with their dependencies and their expected temporal parameters. The schema is automatically translated into an equivalent preemptive time Petri net, which supports verification of the process architecture with respect to timeliness and sequencing requirements through state space analysis. The specification model drives the implementation stage enabling a disciplined coding of the process architecture on top of conventional primitives of a real-time operating system. At the same time, the preemptive Time Petri Net specification and the results of its state space analysis support functional testing enabling the construction of a time-sensitive Oracle and providing a metrics for coverage analysis. Computational experience in the Linux RTAI environment is reported to demonstrate the capability of the method to be effectively integrated in a practical approach.