[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-CongTrans-wf
enrich gen-execute , 
       gen-secdomain-set
 with
   predicates 
      inv : systemstate;
      comment: system invariant;
       
      wf : command;
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: equivalence (relation) of systemstates w.r.t. secdomain (Rushby Def. 3);
       
   
   axioms 
      inv-exec :  ⊦ inv(sys) → inv(exec(sys, co) .1);
      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);
      output-consistent :  ⊦ wf(co) ∧ inv(sys) ∧ inv(sys0) ∧ eqd(sys, cdom(co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2;
      comment: Rushby Def. 3;
       
      locally-respects :  ⊦ wf(co) ∧ inv(sys) ∧ ¬ cdom(co) ⇒ d0 → eqd(sys, d0, exec(sys, co) .1);
      comment: Rushby Def. 4;
       
      step-consistent :  ⊦ wf(co) ∧ inv(sys) ∧ inv(sys0) ∧ eqd(sys, d, sys0) → eqd(exec(sys, co) .1, d, exec(sys0, co) .1);
      comment: Rushby Def. 4.;
       
end enrich