Personnes présentes

• Frédéric Boulanger
• Thibaut Balabonski
• Chantal Keller
• Safouan Taha
• Burkhart Wolff
• Lina Ye

Failure Divergence Semantics of CSP in Isabelle/HOL

Safouan Taha

CSP was first introduced by Tony Hoare in his paper in 1978, which is a formal language for describing patterns of interaction especially for concurrent and compositional systems. In CSP, various process algebraic operators are available to describe the relationships between different processes as well as the way each process communicates with its environment. Nowadays it is also considered as a member of the family called process algebras or process calculi. With this algebraic approach, complex process descriptions can be easily constructed from a few primitive elements. Some principal operators are listed as follows:

• STOP: the process communicating nothing, also called deadlock
• SKIP: successful termination
• Prefix: the process is to communicate an event with its environment and then behaves like a process
• Deterministic choice: the process allows a choice between two component processes, which is determined by its environment that communicate an initial event for one of the processes.
• Nondeterministic choice: the choice between these two component processes is decided by the process itself, i.e., its environment has no control over which of the processes will be selected.
• Parallel with interface: the process is composed by the component processes that are synchronized based on the set of interface events, i.e., any event in the interface can only occur when all component processes are ready to engage in this event.
• Hide: this process allows process abstraction by making some events unobservable.

For CSP with its set of process algebraic operators, its associated trace semantics cannot express non-determinism due to its indistinguishableness from deterministic choice. Furthermore, it cannot distinguish deadlock from infinite internal (hidden and unobservable) activity. To solve these problems, the failure-divergence (F-D) semantic was proposed by introducing the notion of refusal and divergence. With F-D semantic, one can associate the set of refusal events after each trace. In this way, for deterministic choice, the maximal refusal set is the set with all events except a and b. While for non-deterministic choice, it has two maximal refusal sets: all events except a or all events except b. Thus, one can well distinguish deterministic from non-deterministic choice. Furthermore, to be able to tell the difference between deadlock and infinite internal events, the F-D semantic associates a process with a set of traces that result in divergence, i.e., the process engages in executing infinite internal events. Thus, a process with F-D semantic is represented by the set of failures (sets of pairs: trace s with the set of events that can be refused by the process after s) and the set of traces after which a process may diverge.

Originally, six well-definedness conditions are defined the F-D semantics of a process:

• the empty trace is the initial trace of a process
• traces are prefix-closed
• all subsets of a refusal set can be refused by a process
• all events can be included in a refusal set when they are not possible to perform in the next step
• a divergence set is suffix-closed
• after a trace that is in the divergence set, then the process can engage in or refuse any sequence of events.

Then, ticks are formally defined to only appear at the end of a trace, which are added in the set of well-formedness conditions. For such a setting, the process ordering and the refinement ordering can coexist from a proof theory point of view.

(*refinement ordering*) 
P≤Q ≡ Failure P ⊇ Failure Q ∧  Divergence P ⊇ Divergence Q 
(*process ordering*) 
P⊑Q ≡  Divergence P ⊇ Divergence Q 
       ∧ s ∉ Divergence P ⇒ R P s = R Q s
       ∧ min_elems(Divergence P) ⊆ traces Failure Q
(*where R P s ≡ { X | (s, X)∈F P} and min_elems denotes the set of minimal elements of a set*)

It is known that the process ordering implies refinement ordering. One important consequence of this is that if a fix point exists with respect to the process ordering, then it coincides with that with respect to the refinement ordering. For the entire theory, the most complex and important part is to prove the continuity for the set of operators described above. In other words, once the given simple processes are continuous, then the complex process composed by them with CSP-operators are also continuous.

One typique example is described as follows.

datatype 'a channel = left 'a | right 'a | mid 'a | ack

definition SYN  :: "('a channel) set"
where     "SYN  ≡ (range mid) ∪ {ack}"

definition COPY :: "('a channel) process"
where     "COPY ≡ (μ COPY. left`?`x → right`!`x → COPY)"

definition SEND :: "('a channel) process"
where     "SEND ≡ (μ SEND. left`?`x → mid`!`x → ack → SEND)"

definition REC  :: "('a channel) process"
where     "REC  ≡ (μ REC. mid`?`x → right`!`x → ack → REC)"


definition SYSTEM :: "('a channel) process"
where     "SYSTEM ≡ ((SEND ⟦ SYN ⟧ REC) \\ SYN)"

Then we can prove COPY ⊑ SYSTEM.

Safouan demonstrates how he proves the continuity of hide operator with finite hide-set without using the existing theory about könig’s lemma that gives a sufficient condition for an infinite graph to have an infinitely long path.

There exists a model-checker for CSP called FDR that provides automatic refinement proofs for specialized, finite CSP specifications. Isabelle/CSP provides however interactive proof support that can check infinite CSP.