Issue No. 02 - February (1994 vol. 20)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.265634
<p>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.</p>
real-time systems; temporal logic; Petri nets; formal specification; theorem proving; real-time systems; property proving; logical specifications; TRIO; formal analysis; timed Petri net; temporal logic; axiomatization; Hoare method; embedded systems; first-order logic; formal specification; dual language
A. Morzenti, M. Felder and D. Mandrioli, "Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models," in IEEE Transactions on Software Engineering, vol. 20, no. , pp. 127-141, 1994.