StageHOL-CSP-POTS

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

Contact: B. Wolff, S. Taha

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,[1] 
     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[2] 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).


    C.f. 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 stage is to analyse via interactive proofs in Isabelle/HOL and the HOL-CSP Refinement Toolkit [2] and to prove via refinement proofs a number of deadlock and life lock properties of phones, networks, and (ideally arbitrarily large) SYSTEM's.

Workplan

  1. Etat de l'art de POTS and its modelization
  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.