Zusammenfassung Formal Methods

Aus VISki
Wechseln zu: Navigation, Suche

Abkürzungen

  • ARI - arithmetic (axiom or rule)
  • CNTR - contradiction (efq rule from logic)
  • DLF - deadlock free
  • EQL - equality
  • FUN - functional (requirement)
  • GRD - guard
  • HYP - hypothesis
  • IMP - implication
  • INI - initialisation
  • INV - invariant
  • MON - monotonicity (of hypotheses)
  • PRP - property
  • WFD - ? (without further deadlock) ?


  • LR - left-to-right (usage of a rule)
  • RL - right-to-left


non-deterministic case:

  • AP - 'after-predicate of the event' (used for INI_INV rule)
  • BAP - 'before-after predicate of the event' (used for event definition)


Definitionen

Definition: Axiom

An axiom is a predicate that constrains the static part of the model, namely the sets and constants


Definition: Invariant

An invariant is a prediacte that constrains the dynamic part of the model, namely the variables

Formalismus und Notation

  • constants
  • properties
  • variables
  • invariants
  • events:
    • simple
Event
  when
    
  then
              non-deterministic: 
  end
  • events:
    • parameterized
...
ToDo:
Nicht-deterministische und parametrisierte Fälle ergänzen.
Alle momentan zu editierenden Einträge werden hier gesammelt.

Regeln

Übersicht

Zu beweisen ist:

  • Initial Model
    • Establishment of the invariants after initialization (INI_INV)
    • Preservation of each invariant after each event (/inv0_k/INV)
    • Deadlock-freeness (there is no state where all events are guarded out) (DLF) (not mandatory!)
  • Refinements
    • Establishment of the concrete invariants after initialization (INI_INV_REF)
    • For old events:
      • Guard strenghtening for each event (/GRD_REF)
      • Preservation of each concrete invariant after each concrete event , refining the abstract event (/inv._k/INV_REF)
        • can take abstract invariants as facts
        • => compatibility of concrete events to abstract ones
    • For new events:
      • Preservation of each concrete invariant after each concrete event , refining the implicit event (/inv._k/INV_REF)
      • Absence of divergence for each concrete event (/WFD_REF1, /WFD_REF2)
        • uses a variant

Proof Obligation Rules

ToDo:
{{{1}}}
Alle momentan zu editierenden Einträge werden hier gesammelt.