Empowering the Event-B Method Using External Theories
Pages 18 - 35
Event-B offers a rigorous state-based framework
for designing critical systems. Models describe state changes
(transitions), and invariant preservation is ensured by inductive proofs
over execution traces. In a correct model, such changes transform safe
states into safe states, effectively defining a partial function, whose
domain prevents ill-defined state changes. Moreover, a state can be
formalised as a complex data type, and as such it is accompanied by
operators whose correct use is ensured by well-definedness (WD)
conditions (partial functions).
This paper
proposes to define transitions explicitly as partial functions in an
Event-B theory. WD conditions associated to these functions prevent
ill-defined transitions in a more effective way than usual Event-B
events. We advocate that these WD conditions are sufficient to define
transitions that preserve (inductive) invariants and safety properties,
thus providing easier and reusable proof methods for model invariant
preservation. We rely on the finite automata example to illustrate our
approach.
Comments
Post a Comment