O'Reilly logo

Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS by Rakefet Kol, Michael Yoeli

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

image

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”) ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required