Subscribe
Issue No.03 - March (1991 vol.17)
pp: 259-273
ABSTRACT
<p>A description and analysis of concurrent systems, such as communication systems, whose behavior is dependent on explicit values of time is presented. An enumerative method is proposed in order to exhaustively validate the behavior of P. Merlin's time Petri net model, (1974). This method allows formal verification of time-dependent systems. It is applied to the specification and verification of the alternating bit protocol as a simple illustrative example.</p>
INDEX TERMS
verification; time dependent systems; time Petri nets; concurrent systems; communication systems; explicit values; formal verification; time-dependent systems; specification; alternating bit protocol; formal specification; parallel programming; Petri nets; program verification; protocols
CITATION
B. Berthomieu, "Modeling and Verification of Time Dependent Systems Using Time Petri Nets", IEEE Transactions on Software Engineering, vol.17, no. 3, pp. 259-273, March 1991, doi:10.1109/32.75415