Abstract
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.
[download the pdf file] [DOI]