Title :
Modeling and verification of time dependent systems using time Petri nets
Author :
Berthomieu, Bernard ; Diaz, Michel
Author_Institution :
CNRS, Toulouse, France
fDate :
3/1/1991 12:00:00 AM
Abstract :
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
Keywords :
Petri nets; formal specification; parallel programming; program verification; protocols; alternating bit protocol; communication systems; concurrent systems; explicit values; formal verification; specification; time Petri nets; time dependent systems; time-dependent systems; verification; Fires; Petri nets; Protocols; Reachability analysis;
Journal_Title :
Software Engineering, IEEE Transactions on
