Introduction to formal verification

Introduction to formal verification

Frédéric Herbreteau, Bordeaux INP/LaBRI (frederic.herbreteau@bordeaux-inp.fr)

Objective

  • Use model-checking to assert the correctness of a system
    • from a model $M$: a set of runs given as a transition system
    • and a specification $\varphi$ \(M \models \varphi\)
  • The specification $\varphi$ shall specify which runs are correct and which are not
  • A dedicated algorithm is then use to decide wether $M \models \varphi$ or not

What is a specification?

  • Property of the runs of a system: which runs are correct and which are not?
  • Must have a clear and well-defined semantics

Example: mutual exclusion

”$\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$ do not access the critical section simultaneously”

Good run Bad run

Formalising specifications

  • $AP$ = set of atomic propositions on states (labels)
  • $\Sigma = 2^{AP}$ is the set of all sets of atomic propositions (observations)
  • $\Sigma^*$ and $\Sigma^\omega$ are the sets finite and infinite sequences over $\Sigma$
  • A property $P$ is any subset of infinite traces from $\Sigma^\omega$

Example: mutual exclusion (cf. previous slide)

  • $AP$?
  • What is $\Sigma$?
  • Give some traces from $\Sigma^*$ From $\Sigma^\omega$?
  • Express “$\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$ do not access the critical section simultaneously”

Invariance properties

  • Properties that involve only one state (not several states on a run)
  • Must hold in every state of the model

Example:

  • mutual exclusion: no state with both $\textcolor{blue}{cs_1}$ and $\textcolor{red}{cs_2}$
  • absence of deadlock: every state has (at least) one outgoing edge
  • domain: the value of $x$ is always non-negative

Specification of invariance properties in TLA+

  • Invariant property in TLA+:
Mutex == ~(cs1 /\ cs2)    (* in .tla file *)

INVARIANT Mutex           \* in .cfg file
  • Deadlock verification in TLA+:
CHECK_DEADLOCK TRUE       \* in .cfg file