2 (*<*)

     1 (*<*)

     3 theory PIPDefs

     2 theory PIPDefs

     4 imports Precedence_ord Moment RTree Max

     3 imports Precedence_ord Moment RTree Max

     5 begin

     4 begin

     6 (*>*)

     5 (*>*)

     7 

     8 

     8 text {*

     9 text {*

     9   In this section, the formal model of  Priority Inheritance Protocol (PIP) is presented. 

    10   In this section, the formal model of  Priority Inheritance Protocol (PIP) is presented. 

    10   The model is based on Paulson's inductive protocol verification method, where 

    11   The model is based on Paulson's inductive protocol verification method, where 

    11   the state of the system is modelled as a list of events happened so far with the latest 

    12   the state of the system is modelled as a list of events happened so far with the latest