A HOL-CSP Case-Study : Analysing the Plain-Old-Telephone Protocol

By BurkhartWolff, on December 13, 2021, at 08:48 PM

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:

Plain old telephone service (POTS), or plain ordinary telephone system, is a retronym for voice-grade telephone service employing analog signal transmission over copper loops. POTS was the standard service offering from telephone companies from 1876 until 1988 in the United States when the Integrated Services Digital Network (ISDN) Basic Rate Interface (BRI) was introduced, followed by cellular telephone systems, and voice over IP (VoIP). POTS remains the basic form of residential and small business service connection to the telephone network in many parts of the world. The term reflects the technology that has been available since the introduction of the public telephone system in the late 19th century, in a form mostly unchanged despite the introduction of Touch-Tone dialing, electronic telephone exchanges and fiber-optic communication into the public switched telephone network (PSTN). -- source: Wikipedia

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

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

Required Skills

  1. Interest in formal protocol analysis
  2. Basic understanding of concurrent theories such as CCS or CSP
  3. Basic understanding of interactive theorem proving in Coq or Isabelle (M1 - level ?)
  4. 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.

Tags: Isabelle, Stage M 2

0 comment(s)