[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification gen-CongIntrans
enrich gen-secdomain-set
 , 
       gen-execute with
   predicates 
      inv : systemstate;
      comment: system invariant;
       
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: equivalence of systemstates w.r.t. secdomain;
       
   
   axioms 
      eqd-refl :  ⊦ eqd(sys, d, sys);
      eqd-symm :  ⊦ eqd(sys, d, sys0) → eqd(sys0, d, sys);
      eqd-trans :  ⊦ eqd(sys, d, sys0) ∧ eqd(sys0, d, sys1) → eqd(sys, d, sys1);
      dom-equiv :  ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) → (cdom(sys, co) ⇒ d ↔ cdom(sys0, co) ⇒ d);
      dom-equal :  ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, cdom(sys, co), sys0) → cdom(sys, co) = cdom(sys0, co);
      locally-respects :  ⊦ inv(sys) ∧ ¬ cdom(sys, co) ⇒ d0 → eqd(sys, d0, exec(sys, co) .1);
      comment: Rushby Def. 4;
       
      output-cons :  ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, cdom(sys, co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2;
      comment: Rushby Def. 3;
       
      weakly-step-consistent
      :  ⊦ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) ∧ eqd(sys, cdom(sys, co), sys0) → eqd(exec(sys, co) .1, d, exec(sys0, co) .1);
      inv-init :  ⊦ inv(initialstate);
      inv-exec :  ⊦ inv(sys) → inv(exec(sys, co) .1);
end enrich