# Zusammenfassung Formal Methods

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 ${\displaystyle c}$
• properties ${\displaystyle P(c)}$
• variables ${\displaystyle v}$
• invariants ${\displaystyle I(c,v)}$
• events:
• simple
```Event
when
${\displaystyle G(c,v)}$
then
${\displaystyle v:=E(c,v)}$          non-deterministic: ${\displaystyle v:|BAP(c,v,v')}$
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 ${\displaystyle I_{k}}$ after each event ${\displaystyle e_{i}}$ (${\displaystyle e_{i}}$/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 ${\displaystyle e_{i}}$ (${\displaystyle e_{i}}$/GRD_REF)
• Preservation of each concrete invariant ${\displaystyle J_{k}}$ after each concrete event ${\displaystyle f_{i}}$, refining the abstract event ${\displaystyle e_{j}}$ (${\displaystyle f_{i}}$/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 ${\displaystyle J_{k}}$ after each concrete event ${\displaystyle f_{i}}$, refining the implicit event ${\displaystyle skip}$ (${\displaystyle f_{i}}$/inv._k/INV_REF)
• Absence of divergence for each concrete event ${\displaystyle f_{i}}$ (${\displaystyle f_{i}}$/WFD_REF1, ${\displaystyle f_{i}}$/WFD_REF2)
• uses a variant

## Proof Obligation Rules

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