Introduction

The goal of this project is to define a framework to reason formally about the B method.

At the core of the project is the definition of a formal semantics for B in the logic of a proof assistant, namely Isabelle/HOL.

Overview

Formalize B entities Machine, Refinement
Formalize soundness
- machine: a LTS where all states satisfy their invariant
- refinement: a LTS that preserve the behavior of the refined LTS
Formalize the proof obligations of the B method
- machine:
  1. initial states satisfy their invariant
  2. the transition relation preserves the invariant
- refinement:
  1. any concrete initial state is related to an abstract initial state
  2. any transition from a concrete state related to an abstract state reaches a concrete state that is also related to an abstract state
Prove that the proof obligations entail soundness

B components as state-transition systems.
- Define the notion of reachability.
- Show some basic properties about reachability.
Observable behaviour of a B component as a set of traces.
B refinement, relates a (concrete) component together with an (abstract) component, using through a gluing relation between their state space.
Composition of refinements.
- Define an identity refinement, show it is neutral for the composition of refinements.
- Property: transitivity.
Enrich the semantics associating input and outputs to the transitions.
Improve the semantic model by distinguishing LTS and machine (LTS plus safety condition).
Improve the semantic model by distinguish path (internal behaviour: states and transitions) and trace (external behavior: events on transitions).
Prove sufficient conditions to establish a safety property w.r.t. initial states and transition relation.
[TODO] Establish a relation between refinement and traces.