Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

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:

1. It is always possible for every subscriber to lift the receiver (if in the “onhook” state) and replace it (if in the “offhook” state).
2. A subscriber, after obtaining a dial-tone, may dial any subscriber.
3. For a given subscriber, only one tone may be activated at any one time.
4. 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 ...