PROVING PROPERTIES OF REAL-TIME SYSTEMS THROUGH LOGICAL SPECIFICATIONS AND PETRI-NET MODELS

We address the problem of formally analyzing the properties of real-ti me systems. We propose a method based on modeling the system as a time d Petri net and on specifying its properties in TRIO, an extension of temporal logic suitable for dealing explicitly with time and for measu ring it. Timed Petri nets are axiomatized in terms of TRIO, so that th eir properties can be derived as theorems in the same spirit as the cl assical Hoare method allows one to prove properties of programs coded in a Pascal-like language. The method is also illustrated through an e xample.