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

CHAPTER 4

Introducing LOTOS

In this chapter we introduce an important approach to digital systems and circuits, based on LOTOS and the associated toolbox CADP. LOTOS (Language Of Temporal Ordering Specification) is a high-level specification language originally intended for the specification and verification of communication protocols. However, LOTOS is also applicable to discrete systems, particularly parallel, event-based systems, as well as to digital circuits, and particularly to modular asynchronous circuits. CADP (1) is a powerful toolset, developed at the INRIA Institute in Grenoble, France.

CADP now stands for “Construction and Analysis of Distributed Processes”. Originally, it stood for “CAESAR/ALDEBARAN Development Package”. For further details of CADP, see Section 4.8.

4.1 FROM BLOT TO BASIC LOTOS

In this section we illustrate how Blot specifications may be converted into Basic LOTOS specifications, which can then be analyzed using the CADP toolbox.

Example 4.1 Consider the Blot specification

When we wish to convert this Blot specification into a (Basic) LOTOS specification, we have two options as to the way we handle the ‘$’ symbol. The first is to replace the ‘$’ by ‘stop’. The second is to replace the ‘$’ by ‘exit’. In general, ‘stop’ refers to an undesirable termination, such as deadlock (to be discussed later on), whereas ‘exit’ indicates a proper (“successful”) ...