In: IEEE Transactions on Software Engineering, Volume 20, Issue 2, pages 127-141. IEEE Press, February 1994.
Abstract: Addresses the problem of formally analyzing the properties of real-time systems. We propose a method based on modeling the system as a timed Petri net and on specifying its properties in TRIO, an extension of temporal logic suitable for dealing explicitly with time and for measuring it. Timed Petri nets are axiomatized in terms of TRIO, so that their properties can be derived as theorems in the same spirit as the classical Hoare method allows one to prove properties of programs coded in a Pascal-like language. The method is also illustrated through an example.
Keywords: Hoare method; Petri nets; TRIO; axiomatization; dual language; embedded systems; first-order logic; formal analysis; formal specification; logical specifications; property proving; real-time systems; temporal logic; theorem proving; timed Petri net.