**Level: ** M1,M2

**Contact: ** Burkhart Wolff, Safouan Taha

** Summary.** The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP; the resulting theory is called HOL-CSP. The "Plain Old Telephone Service" is a standard medium-size example for architectural modeling of a concurrent system. The goal of this internship is a formal analysis of deadlock and life lock properties of this protocol via interactive proof in Isabelle/HOL and Isabelle/HOL-CSP.

### Description

The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP; in particular, the resulting theory HOL-CSP [1] can cope with infinite alphabets, in contrast to model-checking approaches that are limited to finite ones. We extended this theory to a significant degree by taking advantage of more powerful automated proof techniques of modern Isabelle/HOL. A framework for semi-automated refinement proofs has also been provided [2].

The "Plain Old Telephone Service" is a standard medium-size example for architectural modeling of a concurrent system. Quote:

Based on an existing modelling phones, networks, and the architectural composition combining a family of phones with a family of network-adaptors to a global system, one gets:

fixrec T :: "Phones → channels process" and Oside :: "Phones → channels process" and Tside :: "Phones → channels process" and NoReject :: "Phones → channels process" and Reject :: "Phones → channels process" where T_rec : "T⋅ts = (Tside⋅ts ❙; T⋅ts) ⤜ (Oside⋅ts ❙; T⋅ts)" | Oside_rec : "Oside⋅ts = (StartReject❙!ts → tcO❙!(ts,Osetup) → (⨅ p ∈ phones. Oside1 ts p))" | Tside_rec : "Tside⋅ts = (ctT❙?(y,z,os)❙|((y,z)=(ts,Tsetup)) → StartReject❙!ts → ( tcT❙!(ts,Talert,os) → tcT❙!(ts,Tconnect,os) →(Tside_connected ts os) ⊓ (tcT❙!(ts,Tconnect,os) → (Tside_connected ts os))))" | NoReject_rec : "NoReject⋅ts = (StartReject❙!ts → Reject⋅ts)" | Reject_rec : "Reject⋅ts = (ctT❙?(y,z,os)❙|(y=ts ∧ z=Tsetup ∧ os∈phones ∧ os≠ts) → (tcT❙!(ts,Tbusy,os) → Reject⋅ts) □ (EndReject❙!ts → NoReject⋅ts))" definition Tel:: "Phones ⇒ channels process" where ‹Tel p ≡ (T⋅p ⟦{StartReject p, EndReject p}⟧ NoReject⋅p) \ {StartReject p, EndReject p}› ... definition NETWORK :: "channels process" where "NETWORK ≡ (❙|❙|❙| os ∈ (mset_set phones). Call⋅os)" definition TELEPHONES :: "channels process" where "TELEPHONES ≡ (❙|❙|❙| ts ∈ (mset_set phones). Tel ts)" definition SYSTEM :: "channels process" where "SYSTEM ≡ NETWORK ⟦VisibleEvents⟧ TELEPHONES"

The purpose of this internship is to analyse via interactive proofs in Isabelle/HOL and the The Isabelle/HOL-CSP Refinement Toolkit and to prove via refinement proofs a number of deadlock and life lock properties of phones, networks, and (ideally arbitrarily large) SYSTEMs.

### Workplan

- Etat de l'art de POTS and its modelisation
- Interactive refinement proofs in Isabelle/HOL of deadlock-freeness properties such as "∀p ∈ phones. deadlock_free (Tel p)"
- Interactive refinement proofs in Isabelle/HOL of lifelock-freeness properties such as "lifelock_free SYSTEM"

### Required Skills

- Interest in formal protocol analysis
- Basic understanding of concurrent theories such as CCS or CSP
- Basic understanding of interactive theorem proving in Coq or Isabelle (M1 - level ?)
- no knowledge in analogue telephones necessary ;-)

### Bibliography

[1] Safouan Taha, Burkhart Wolff and Lina Ye: Isabelle/HOL-CSP, 2019.

[2] Safouan Taha, Burkhart Wolff and Lina Ye: The Isabelle/HOL-CSP Refinement Toolkit, 2020.

[3] Safouan Taha, Burkhart Wolff and Lina Ye: Philosophers may dine - definitively ! (PDF), iFM, Oct 2019.