Deductive Verification of Transition Systems in Why3
State Machine Specifications and Inductive Invariants
State machines and transition relations are used in computer science to model the execution of software systems, and study their semantics and safety properties, in different contexts.
Important properties of a state machine specification have to do with the configurations that can be reached from the initial states.
An invariant of such a state machine is any property that holds in all reachable configurations. Invariants are used in deductive verification to prove safety properties.
In any state machine there are likely some bad/undesired configurations, for instance concerning errors or inconsistencies that should not be allowed to occur.
A safety property of a system is any reachability property that can be framed as“no bad/undesired configuration of the system can be reached from the initial states”. To prove a safety property it suffices to find an invariant that is not true in bad configurations. This immediately implies that such configurations are unreachable.
One way to prove that a property is an invariant is by using induction:
Not all invariants are inductive! Model checking may be able to“prove” any invariant, but in deductive verification inductive invariants are crucial, since it is possible to reason about them without exploring the state space of the system.
State Machine Specifications in Why3, by Example
Imperative(stateful) Encoding
Stateful software modules with multiple state-changing functions can be seen to define state machines.
Consider a verified implementation in Why3 of a “ To Do” software concept, where the state is a pair of sets of tasks, pending and finished:
moduleToDo_implicit
type task
clone export set.SetImpwithtype elt = task
type statettype = { pending : set ; finished : set }
val state : statettype
...
The API of the module consists of three functions: add, complete, and delete. The first of these simply adds a task to the pending set:
let addT (t:task) : ()
requires { not mem t (union state.pending state.finished) }
= add t state.pending
In order to write the function’s specification as a contract we can use logical functions from Why3’s set theory(https://www.why3.org/stdlib/set.html).
The requires clause(aprecondition)states that tasks can only be added if they’re not yet in any of the two lists.
We can add to this postconditions(ensures clauses) giving a logical description of the effects of the function on the module’s state, using the old operator to refer to the state before execution of the function:
State Machine Specifications and Inductive Invariants
State Machine Specifications in Why3, by Example
Imperative (stateful) Encoding
module ToDo_implicit type task clone export set.SetImp with type elt = task
type statettype = { pending : set ; finished : set }
val state : statettype ... let addT (t:task) : () requires { not mem t (union state.pending state.finished) } = add t state.pending