Modeling and verification of time dependent systems using time Petri nets
- 1 March 1991
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 17 (3), 259-273
- https://doi.org/10.1109/32.75415
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
This publication has 10 references indexed in Scilit:
- A Generalized Timed Petri Net Model for Performance AnalysisIEEE Transactions on Software Engineering, 1987
- Modeling and analysis of communication and cooperation protocols using petri net based modelsComputer Networks (1976), 1982
- REBUS, A Fault-Tolerant Distributed System for Industrial Real-Time ControlIEEE Transactions on Computers, 1982
- Protocol Representation with Finite-State ModelsIEEE Transactions on Communications, 1980
- Timed Petri nets and preliminary performance evaluationPublished by Association for Computing Machinery (ACM) ,1980
- A polynomial time algorithm for solving systems of linear inequalities with two variables per inequalityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1979
- Complexity of some problems in Petri netsTheoretical Computer Science, 1977
- Recoverability of Communication Protocols--Implications of a Theoretical StudyIEEE Transactions on Communications, 1976
- Parallel program schemataJournal of Computer and System Sciences, 1969
- A note on reliable full-duplex transmission over half-duplex linksCommunications of the ACM, 1969