DocumentCode
1490780
Title
Modeling and verification of time dependent systems using time Petri nets
Author
Berthomieu, Bernard ; Diaz, Michel
Author_Institution
CNRS, Toulouse, France
Volume
17
Issue
3
fYear
1991
fDate
3/1/1991 12:00:00 AM
Firstpage
259
Lastpage
273
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;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.75415
Filename
75415
Link To Document