Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PIPDefs.thy
changeset 104 43482ab31341
parent 101 c7db2ccba18a
parent 97 c7ba70dc49bd
child 115 74fc1eae4605
equal deleted inserted replaced
103:d5e9653fbf19 104:43482ab31341 
     1 chapter {* Definitions *}
 
       
     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 (*>*)
 
       
     6 
       
     7 chapter {* Definitions *}
 
     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
pip