<figure><img src="image_1.png" /></figure>

# DEDUCTIVE VERIFICATION OF SYNCHRONOUS REACTIVE PROGRAMS

<figure><img src="image_2.png" /></figure>

Térence Clastres, Frédéric Dabrowski

Université d'Orléans, INSA CVL, LIFO, UR 4022, Orléans, France

<figure><img src="image_3.png" /></figure>

## Deductive Verification

* Formal method to verify the functional correctness of programs
* Starts from an assumption (precondition) `{P}` about the program initial state and tries to conclude the last state reached is within an accepted set of states `{Q}` (postcondition)
* Uses deductively applied inference rules to produce mathematical statements requiring a proof
* Specification is written in a logic language (e.g. predicate logic)
* Various tools developed to ease the verification process, from SMT solvers (Alt-Ergo, Z3...), to dedicated verification platforms communicating with them (Why3, Dafny...)

<figure><img src="image_4.png" /><figcaption>Annotated Program</figcaption></figure>

<figure><img src="image_5.png" /></figure>

## Synchronous Reactive Programs

<figure><img src="image_6.png" /></figure>

For our purposes, programs are written in a simple imperative language with arduino-like setup/loop procedures:

input on off : bool;
output light : bool;
setup : x := false;
loop:
    if on then
        emit true to light;
    else if off then
        emit false to light; end
end

## Temporal Properties

* Instead of viewing a program as a transformational machine, focus on its behaviour over time
* Decomposition Theorem: every program property is a conjunction of a safety and liveness property.

### Safety: a bad thing never happens

* e.g. loop invariant
* proof tool: induction
* doing a bad thing is irremediable
  → finite counter-example

### Liveness: a good thing eventually happens

* e.g. program termination
* proof tools: well-founded relations, coinduction
* a good thing can always be done later
  → infinite counter-example

## Linear Temporal Logic

* Need for a concise way to describe a program behaviour
* A behaviour is seen as an infinite word $\sigma$ (e.g. ababababa...)

<caption>Syntax</caption>

$$LTL(\Sigma) \ni \phi ::= p \in \Sigma \mid \neg \phi \mid \phi \lor \phi \mid X\phi \mid \phi U\phi \mid G\phi \mid \phi R\phi$$

<figure><img src="image_7.png" /><figcaption>Semantics</figcaption></figure>

## Büchi Automaton

* Nondeterministic finite-state automaton on infinite words (recognizer)
* A run is an infinite sequence of state and transitions, starting from a state marked 'initial'
* A word is read left to right. To each letter $x$ must correspond a transition labelled $x$ from the current state to the next
* No final state but an acceptance condition: certain states are marked 'acceptant', and at least one of them must be present infinitely many times in the run for it to be acceptant
* Effective construction from an LTL formula
* More expressive than LTL (equivalent to $\omega$-regular expressions)

<figure><img src="image_8.png" /></figure>

## Verification Procedure for Safety Properties

<figure><img src="image_9.png" /></figure>

## Future Work

### Nondeterministic Specification

* Adds more flexibility
* Büchi automata are $\exists$-automata: a word is accepted if at least one path is acceptant
* Our method requires all paths to be acceptant
* This approach is correct but too naive: useless constraints are generated
  → refinement of the specification automaton

### Liveness

* Safety properties enable us to mark every state acceptant
* Liveness requires showing there are infinitely many accepting states along a path
* How to deal with liveness in rely formula? → fairness assumptions

### Internal Memory

* Specification needs to mention the program internal memory for successful verification
* Internal memory is an implementation detail that shouldn't be visible
* Write a public and private specification and show the private specification implies the public one

### Multiple Programs

* Currently, a single program
* Goal: multiple programs in cooperation
* Parallel / sequential composition
* Controlled memory sharing
* Need for compositionality