Formal specification and verification

Formal specification and 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 a sequence of states)
  • 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

Algorithmic verification of invariance properties

Exercise: Give an algorithm to check an invariance property over a finite transition system

  • 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

Temporal Logic (TL)

Temporal properties

  • Temporal refers to logical time
  • Temporal properties express requirements over infinite sequences of states

Example:

  • “Accesses to the critical section are alternatively granted to $\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$”
  • “If $\textcolor{blue}{P_1}$ requests the critical section, then access is eventually granted”
  • A temporal property is true for a model if all its runs satisfy the property
  • Two kinds of temporal properties: safety and liveness

Safety properties

“Nothing bad will never happen”

Example:

  • Invariant properties are a special case of safety properties
  • Partial correcteness for sequential programs
  • ”$\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$ do not access the critical section simultaneously”
  • “Accesses to the critical section are alternatively granted to $\textcolor{blue}{P_1}$ and $\textcolor{red}{P_2}$”

A safety property is characterised by a set $B \subseteq \Sigma^*$ of finite counter-examples

Definition A set $P \subseteq \Sigma^\omega$ is a safety property if there exists $B \subseteq \Sigma^*$ such that $P = \Sigma^\omega - (B \Sigma^\omega)$

Liveness properties

“Something good will eventually happen”

Example:

  • Termination for sequential program
  • “Each process will eventually enter the critical section”
  • “If $\textcolor{blue}{P_1}$ requests the critical section, then access is enventually granted”
  • “Processes enter the critical section infinitely often”

A liveness property is characterised by infinite counter-examples.

Definition: $P \subseteq \Sigma^\omega$ is a liveness property if every finite sequence can be extended into an infinite sequence in $P$

Example: mutual exclusion

Safety: “nothing bad never happens” Liveness: “something good eventually happens”

Example: Processes compete to access their critical sections protected by a lock.

Safety of liveness?

  • Two processes never access their critical section at the same time
  • Each process accesses the critical section infinitely often
  • If a process requires access to the critical section, access is eventually granted
  • The lock is never stolen

Decomposition of specifications

Decomposition lemma: For every property $P \subseteq \Sigma^\omega$, there exists a safety property $S$ and a liveness property $L$ such that $P = S \cap L$.

Proof: let $Closure(P)$ be the set of words $w \in \Sigma^\omega$ s.t. all their prefixes are prefixes of words in $P$. Then, choose $S = Closure(P)$ and $L = P \cup (\Sigma^\omega - Closure(P))$

Exercise: which properties are safety and liveness at the same time?

  • Specifications mix safety, to ensure good behavior, and liveness, to ensure progress
  • For sequential programs: correctness (w.r.t. precondition and postcondition) and termination

Temporal formulas

$\varphi ::= p \, \, \lnot \varphi \, \, \varphi \land \varphi \, \varphi \lor \varphi \, \, \varphi \implies \varphi \, \, \Box \varphi \, \, \Diamond \varphi \qquad\qquad \text{with } p \in AP$
  • $\Box$ means “always”
  • $\Diamond$ means “eventually”

Example:

  • $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$
  • $\Diamond \textcolor{blue}{cs_1} \land \Diamond \textcolor{red}{cs_2}$
  • $\Box (\textcolor{blue}{req_1} \implies \Diamond \textcolor{blue}{cs_1})$

TLA+ operators: ~, /\, \/, =>, [], <>

Semantics of temporal formulas

Expressed over infinite sequences of observations (sets of labels):

Example: labels ${\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}}$ trace: {} {} {$\textcolor{blue}{cs_1}$} {} {$\textcolor{red}{cs_2}$} {} {} … {} {$\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}$} {} {} …

$\sigma$ an infinite trace, $\sigma[i]$ its value in $i$, $\sigma[i…]$ its suffix from $i$

  • $\sigma \models p$ if $p \in \sigma[1]$
  • $\sigma \models \lnot \varphi$ if $\sigma \not\models \varphi$
  • $\sigma \models \varphi_1 \land \varphi_2$ if $\sigma \models \varphi_1$ and $\sigma \models \varphi_2$
  • $\sigma \models \Box \varphi$ if $\sigma[i…] \models \varphi$ for every $i \ge 1$
  • $\sigma \models \Diamond \varphi$ if there exists $i \ge 1$ such that $\sigma[i…] \models \varphi$

Illustration

Example: Labels: ${\textcolor{blue}{req_1}, \textcolor{blue}{cs_1}, \textcolor{red}{cs_2}}$

Traces:

  • $\sigma_1$: {} {} {$\textcolor{blue}{cs_1}$} {} {$\textcolor{red}{cs_2}$} {} {} … {} {$\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}$} {} {} …
  • $\sigma_2$: {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{red}{cs_2}$} {$\textcolor{blue}{req_1}$} {} {} {} {$\textcolor{blue}{cs_1}$} {} … {} {$\textcolor{blue}{req_1}$} {} {$\textcolor{red}{cs_2}$} {} {} {} {} …

Are the formulas below satisfied or not by the traces above?

  • $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$
  • $\Diamond \textcolor{blue}{cs_1} \land \Diamond \textcolor{red}{cs_2}$
  • $\Box (\textcolor{blue}{req_1} \implies \Diamond \textcolor{blue}{cs_1})$

Combining operators

  • $\Box\Diamond$ “infinitely often”
  • $\Diamond\Box$ “almost always”
  • $\rightsquigarrow$ “leads-to” (~> in TLA+): $\varphi_1 \rightsquigarrow \varphi_2$ is a shortcut for $\varphi_1 \implies \Diamond \varphi_2$

Example: Write traces that satisfy the formulas below, and traces that falsify them:

  • $\Box\Diamond \textcolor{blue}{cs_1}$
  • $\Diamond\Box \textcolor{blue}{req_1}$
  • $\textcolor{blue}{req_1} \rightsquigarrow \textcolor{blue}{cs_1}$
  • $\Box (\textcolor{blue}{req_1} \rightsquigarrow \textcolor{blue}{cs_1})$

Relation between $\Box$ and $\Diamond$

Exercise: Give traces that are respectively satisfied by $\Box p$, $\Box \lnot p$, $\lnot \Box p$, $\Diamond p$, $\Diamond \neg p$, $\neg \Diamond p$

  • What is the difference between $\Box \lnot p$ and $\lnot \Box p$?
  • What is the difference between $\Diamond \lnot p$ and $\lnot \Diamond p$?
  • What is the relation between $\Box$ and $\Diamond$?

Semantics over a transition system

Definition A transition system $M$ satisfies a temporal formula $\varphi$ ($M \models \varphi$) if $\sigma \models \varphi$ for every infinite trace $\sigma$ from an initial state of $M$.

Example: Which formulas below are satisfied by the model to the right?

  • $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$
  • $\Diamond \textcolor{blue}{cs_1} \land \Diamond \textcolor{red}{cs_2}$
  • $\Box (\textcolor{blue}{req_1} \implies \Diamond \textcolor{blue}{cs_1})$

bg right:40% fit

Algorithmic verification of temporal formulas

Goal: given $M$ and $\varphi$, decide whether $M \models \varphi$

Specification in TLA+:

NoStarvation == [](req1 ~> cs1)   (* in the .tla file *)

PROPERTY NoStarvation             \* in the .tlc file

Algorithm:

  1. From $\varphi$ compute a Büchi automaton $\mathcal{A}_{\lnot \phi}$
  2. Compute the product $\mathcal{B} = M \otimes \mathcal{A}_{\lnot \phi}$
  3. Decide whether $\mathcal{L}(\mathcal{B}) = \emptyset$

From TL formulas to Büchi automata

Example: $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$

  • {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$} {} {} …
  • {} {} {$\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$, $\textcolor{red}{cs_2}$} {} {$\textcolor{blue}{cs_1}$} {} …

Example: $\Box (\textcolor{blue}{req_1} \rightsquigarrow \textcolor{blue}{cs_1})$

  • {} {$\textcolor{blue}{req_1}$} {} {} {$\textcolor{blue}{cs_1}$} {} {$\textcolor{blue}{cs_1}$} {} {} {$\textcolor{blue}{req_1}$, $\textcolor{blue}{cs_1}$} {} …
  • {} {} {$\textcolor{blue}{req_1}$} {$\textcolor{blue}{cs_1}$} {} {$\textcolor{blue}{req_1}$} {} {} {$\textcolor{blue}{req_1}$} {} {}…

bg vertical right:33% fit bg right:33% fit

Product $M \otimes \mathcal{A}_{\lnot \varphi}$ (1/2)

Example: $\Box \lnot (\textcolor{blue}{cs_1} \land \textcolor{red}{cs_2})$

Product $M \otimes \mathcal{A}_{\lnot \varphi}$ (2/2)

Example: $\Box (\textcolor{blue}{req_1} \rightsquigarrow \textcolor{blue}{cs_1})$

Checking if $\mathcal{L}(M \otimes \mathcal{A}_{\lnot \varphi}) = \emptyset$

  • $\mathcal{L}(M \otimes \mathcal{A}_{\lnot \varphi}) \neq \emptyset$ iff there is an infinite run that visits an accepting state infinitely many times

Exercise: give an algorithm that decides if $\mathcal{L}(M \otimes \mathcal{A}_{\lnot \varphi}) \neq \emptyset$

  • Overall complexity:
    • TL to Büchi automaton: $ \mathcal{A}_{\lnot \varphi} = 2^{\mathcal{O}( \varphi )}$
    • Product: $ M \otimes \mathcal{A}_{\lnot \varphi} = \mathcal{O}( M \times \mathcal{A}_{\lnot \varphi} )$
    • Emptiness checking: $\mathcal{O}( M \otimes \mathcal{A}_{\lnot \varphi} )$
    • Overall complexity: $\mathcal{O}( M \times 2^{ \varphi })$
  • NB: the TL model-checking problem is PSPACE-complete

Temporal Logic of Actions

Actions Formulas

  • TLA+ allows to specify formulas over actions

Example: “If the lock is not free, then it becomes free in the next state” \((lock \neq 0 \implies lock' = 0)\)

  • An action formula $A$ is a formula over primed and unprimed variables, without temporal modalities $\Box$ and $\Diamond$.
  • $(s, s’) \models A$ if $A$ holds with values of unprimed variables from $s$ and values of primed variables from $s’$

Temporal formulas with actions

\[\Box [A]_{\langle V \rangle}\]

where $A$ is an action formula, $V$ is a tuple of variables

Example: “The lock is never stolen” \(\Box[lock \neq 0 \implies lock' =0]_{\langle lock \rangle}\)

  • express properties over consecutive pairs of states on an infinite trace $\sigma$: $\sigma \models \Box [A]_{\langle V \rangle}$ if $(\sigma[i], \sigma[i+1]) \models (A \lor (V’ = V))$ for every $i \ge 1$
  • temporal actions formulas are restricted to safety properties over one action

Illustration

Example: \(\Box[lock \neq 0 \implies lock' =0]_{\langle lock \rangle}\)

Does the formula above hold for the traces below (showing the value of $lock$):

  1. ${0} {0} {0} {0} {0} {0} {0} \dots$
  2. ${0} {1} {0} {2} {0} {1} {0} \dots$
  3. ${0} {1} {1} {1} {0} {2} {0} \dots$
  4. ${0} {1} {1} {1} {1} {1} {1} \dots$
  5. ${0} {1} {1} {1} {2} {0} {0} \dots$

Stuttering-free formulas

  • All TLA+ specificatons should be stuttering free to allow refinement and composition of systems (cf. Stuttering steps)
  • TL formulas are stuttering-free, but TLA+ formulas may not be

Example: the formula below should hold for both the abstact and the refined models \(\Box[lock \neq 0 \implies lock' =0]_{\langle lock \rangle}\)

```TLA+ ... req: lock(self); rel: unlock(self); ... ```
```TLA+ ... req: lock(self); cs1: y := x; cs2: x := x+1; rel: unlock(self); ... ```

Stuttering-free specifications and PlusCal models

  • the TLA+ translation of PlusCal models includes a self-loop on every state
vars == << .... >>  \* Tupe of the variables in the model

Init == ...         \* Initial states over vars
Next == ...         \* Action formula over vars and vars' (transitions)

Spec == Init /\ [][Next]_vars
  • this includes a self-loop on the final states (label Done)
  • hence every run with no deadlock is infinite (termination = reaching Done)

Algorithmic verification of temporal formulas with actions

Goal: given $M$ and $\varphi$, decide whether $M \models \varphi$

Specification in TLA+:

LockNotStolen == [][lock # 0 => lock = 0]_<<lock>>   (* in the .tla file *)

PROPERTY LockNotStolen                               z\* in the .tlc file

Algorithm:

  • same as for state-based safety properties
  • with action properties evaluated on transitions (not on states)