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

CAHPTER 6

Introducing CCS

6.1 ABOUT CCS

CCS (Calculus of Communication Systems) is a theory of communicating systems, developed by Robin Milner (1, 2). Note that LOTOS (see Chapter 4) is based on CCS, as well as on Hoare's CSP 3. This chapter provides an introduction to the theory of CCS, and to its related tool CWB-NC. In the following chapters we describe a variety of applications of CCS. For a recommendable tutorial on CCS and its applications, see Reference 4.

6.2 OPERATORS ‘PREFIX’ AND ‘SUM’

The CCS concept of agent corresponds to that of process introduced in Chapter 2.

The CCS prefix operator, denoted by ‘.’, plays the same role as the LOTOS (or Blot) prefix operator ‘;’. Furthermore, the CCS sum operator ‘+’ corresponds to the LOTOS/Blot choice operator ‘[]’. For example, let VM2 be the vending machine specified in Blot in Chapter 2. Recall that this vending machine operates only once. We repeat its Blot specification:

VM2 : = coin;(coffee;$ [] tea;$)

The corresponding agent is specified in CCS as follows:

VM2_ccs : = coin.(coffee.nil + tea.nil)

Note that the trivial process that does nothing, and is denoted by ‘$’ in Blot, is denoted by ‘nil’ (also ‘0) in CCS. In Chapter 2 we introduced process graphs as a way to represent processes. In CCS such process graphs are known as “transition diagrams” (see Reference 4). The process graph representing VM2, as defined above, was shown in Fig. 2.3.

In view of the above correspondence between CCS and Blot, the process graph ...

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