The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - February (1994 vol.20)
pp: 127-141
ABSTRACT
<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>
INDEX TERMS
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
CITATION
D. Mandrioli, A. Morzenti, "Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models", IEEE Transactions on Software Engineering, vol.20, no. 2, pp. 127-141, February 1994, doi:10.1109/32.265634
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool