CHAPTER 11
Guide to Further Studies
In this chapter we provide references to examples on applying the verification methods described in this book to very large as well as more complicated systems. We also refer to colored Petri nets, which are a powerful extension of Petri nets.
11.1 VERIFICATION OF TELECOMMUNICATION SYSTEMS
11.1.1 Plain Old Telephone System (POTS)
A Plain Old Telephone System (POTS) is a well-documented automatic (dialing-based) conventional telephone switching system. It applies the usual set of tones, i.e., dial-tone, ring-tone, busy-tone, and error-tone. The following are some examples of basic requirements:
- It is always possible for every subscriber to lift the receiver (if in the “onhook” state) and replace it (if in the “offhook” state).
- A subscriber, after obtaining a dial-tone, may dial any subscriber.
- For a given subscriber, only one tone may be activated at any one time.
- The system is deadlock-free.
For the application of Full LOTOS to the specification of examples of POTS, see Reference 1. These demos also deal with the verification of some requirements, similar to those listed above.
For additional LOTOS-based descriptions of POTS, see References 2 and 3.
11.1.2 Advanced Telephone Systems
Modern telephone systems provide many facilities, much beyond those offered by POTS. Such facilities include call-forwarding, call-waiting (camp-on-busy), abbreviated dialing, outgoing call screening, and many others.
For LOTOS-oriented descriptions of advanced ...
Get Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.