A THEORY OF IMPLEMENTATION AND REFINEMENT IN TIMED PETRI NETS

We define formally the notion of implementation for time critical syst ems 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 implemen tation relation. Refinement steps are often used as a means to derive in a systematic way the system design starting from its abstract speci fication. We present a method to formally prove the correctness of ref inement 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 s ystems by performing incremental analysis at various levels of the spe cification/implementation hierarchy. (C) 1998 - Elsevier Science B.V. All rights reserved.