Specification and Validation of Real-time Systems Using Petri Nets.

The authors introduce a new transition system - Petri queue networks - and show that this models is as powerful as a Turing machine and that moreover a utilization method exists which makes possible the analysis of such properties as absence of deadlock or coherence of message exchanged. In dealing with a concrete example arising out of the problem of telephone switching, the authors endeavor to show the extent to which formal analysis is useful in designing a real-time system.