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

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