A theory of implementation and refinement in timed Petri nets

We define formally the notion of implementation for time critical systems in terms of provability of properties described abstractly at the specification level. We characterize this notion in terms of formulas of the temporal logic TRIO and operational models of timed Petri nets, and provide a method to prove that two given nets are in the implementation relation. Refinement steps are often used as a means to derive in a systematic way the system design starting from its abstract specification. We present a method to formally prove the correctness of refinement rules for timed Petri nets and apply it to a few simple cases. We show how the possibility to retain properties of the specification in its implementation can simplify the verification of the designed systems by performing incremental analysis at various levels of the specification/implementation hierarchy.