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

CHAPTER 2

Processes

2.1 INTRODUCTION

In this text we are mainly interested in the specification and description of systems such as communication protocols, asynchronous circuits, pipeline controllers, vending machines, and others that are suitably described using the “event-based” approach (see Chapter 1). We will use the notion of process for the purpose of modeling the behavior of such event-based systems. Most processes described in this chapter are related to systems with inputs and outputs. In the next section we relate processes to behavior patterns and discuss some examples of processes as well as some basic concepts.

2.2 EXAMPLES OF PROCESSES AND BASIC CONCEPTS

Example 2.1 (VM1) This example deals with a coffee-vending machine VM1 (1) that will accept a coin, dispense a cup of coffee, and will then do nothing further. Its behavior pattern consists of two events occurring sequentially (one after the other). The first event, named ‘coin’, refers to “inserting a coin into the coffee-vending machine.” The second event is named ‘coffee’, and refers to “getting a cup of coffee.” The behavior pattern we have in mind (denoted VM1) may be specified as follows:

VM1:= coin;(coffee; $)

Here we use the symbol ‘:=’ to mean “is defined by.” The symbol ‘$’ denotes the trivial behavior of doing nothing. Following LOTOS (see Chapter 4), we will refer to the symbol ‘;’ as a prefix operator. An expression such as X;Y is admissible only if X is an event and Y is a behavior pattern. If this ...