Model checking con NuSMV: logiche CTL e LTL, algoritmo a punto fisso e verifica della mutua esclusione

Un programma concorrente, un protocollo di comunicazione, il controllore di un ascensore o di un semaforo possono funzionare per mesi e poi bloccarsi in una combinazione di eventi che nessun collaudo aveva provato. I metodi formali verificano un sistema in modo esaustivo, dimostrando che una proprietà vale in tutte le esecuzioni possibili. Le strade principali sono due: la dimostrazione automatica dei teoremi (theorem proving), in cui sistema e proprietà sono formule di una logica e si costruisce una dimostrazione, potente ma spesso bisognosa dell’aiuto dell’utente; e il model checking, in cui il sistema è una macchina a stati finiti, le proprietà sono formule di logica temporale, e un algoritmo esplora tutti gli stati raggiungibili. Questa lezione spiega il model checking e le logiche CTL e LTL, ricava l’algoritmo per punti fissi, e lo usa con NuSMV, il model checker simbolico sviluppato da FBK e dalle università di Trento, Genova e Carnegie Mellon, su un classico: la mutua esclusione tra due processi.

L’idea in parole semplici

Immaginate di dover controllare che un incrocio con due semafori non dia mai il verde a entrambe le strade. Provare a mano qualche sequenza di eventi non basta: l’errore potrebbe nascondersi in una combinazione rara. Il model checking costruisce la mappa di tutte le situazioni in cui il sistema può trovarsi (gli stati) e di tutti i passaggi possibili tra di esse, e la percorre interamente cercando una situazione vietata. Se la trova, restituisce il controesempio: la sequenza esatta di passi che porta all’errore, preziosa per correggere il progetto. Se non la trova, la proprietà è dimostrata per tutte le esecuzioni.

Il modello: strutture di Kripke

Il sistema si descrive come una struttura di Kripke: un insieme finito di stati , degli stati iniziali , una relazione di transizione (da ogni stato si può andare in uno o più stati successivi) e, per ogni stato, l’insieme delle proposizioni atomiche vere in esso (per esempio “il processo 1 è nella sezione critica”). Le esecuzioni sono i cammini infiniti che partono da uno stato iniziale; disegnandoli tutti a partire da uno stato si ottiene l’albero delle computazioni.

Le logiche temporali CTL e LTL

Gli operatori temporali parlano di ciò che accade lungo un cammino:

• : vale nel prossimo stato;
• : vale prima o poi (in futuro);
• : vale sempre (globalmente);
• : vale finché non diventa vera , che prima o poi diventa vera.

La LTL (logica temporale lineare) valuta queste formule su ogni cammino: una formula LTL vale se vale su tutti i cammini. La CTL (logica ad albero) mette davanti a ogni operatore un quantificatore sui cammini: (per tutti i cammini) o (esiste un cammino). Così dice “in ogni stato raggiungibile vale ” (una proprietà di sicurezza: niente di male accade mai), “esiste un modo di arrivare a “, “su ogni cammino prima o poi ” (una proprietà di vitalità: qualcosa di buono prima o poi accade), “ogni richiesta è prima o poi servita”.

L’algoritmo: punti fissi

Il model checking CTL calcola, per ogni sottoformula, l’insieme degli stati in cui vale, partendo dalle proposizioni atomiche. Per gli operatori temporali si usano i punti fissi.

Teorema. L’insieme degli stati che soddisfano è il minimo punto fisso dell’equazione , dove sono gli stati in cui vale e gli stati che hanno almeno un successore in ; lo si ottiene iterando , finché non cambia più.

Dimostrazione. Per induzione, è l’insieme degli stati da cui si raggiunge in al massimo passi: vale per , e uno stato raggiunge in al massimo passi se è già in oppure ha un successore che ci arriva in al massimo . La successione è crescente e gli stati sono finiti, quindi si stabilizza dopo al più passi, sull’insieme degli stati da cui è raggiungibile in un numero qualsiasi di passi: proprio . Ogni altro punto fisso contiene ed è chiuso per , quindi contiene tutti i : questo è il minimo. ∎

Gli altri operatori si riducono a questi: ; è il massimo punto fisso di ; . Il costo è lineare nel numero di stati e transizioni.

L’esplosione degli stati. Il problema è che gli stati crescono esponenzialmente con le variabili: 20 variabili booleane danno un milione di stati, 300 ne danno più degli atomi dell’universo. NuSMV usa due rimedi: il model checking simbolico, che rappresenta gli insiemi di stati come formule booleane compresse con i BDD (diagrammi di decisione binaria), e il bounded model checking, che cerca controesempi di lunghezza limitata trasformando il problema in una formula da dare a un risolutore SAT.

Un esempio: la mutua esclusione

Due processi condividono una risorsa (una stampante, una variabile) e non devono mai trovarsi insieme nella sezione critica. Ogni processo ha una bandierina che alza quando vuole entrare. Uno scheduler sceglie a ogni istante quale processo esegue un passo: la variabile del modello rappresenta questa scelta, lasciata libera (non deterministica) così che NuSMV esamini tutti gli intrecci possibili.

Il protocollo ingenuo. Ogni processo controlla che la bandierina dell’altro sia abbassata, poi alza la propria ed entra. Sembra corretto, ma NuSMV risponde che la proprietà è falsa e mostra un controesempio di 6 passi: il processo 1 controlla (bandierina dell’altro bassa), poi lo scheduler fa controllare anche il processo 2 (bandierina del primo ancora bassa), ed entrambi entrano. Il difetto è che “controllare” e “alzare la bandierina” sono due passi separati.

L’algoritmo di Peterson (1981) aggiunge una variabile turno: ogni processo alza la bandierina, poi cede il turno all’altro, e aspetta finché l’altro non vuole entrare o il turno è suo. NuSMV verifica che:

• è vera: la mutua esclusione è garantita;
• è vera, e anche la formula LTL equivalente : chi aspetta entra prima o poi;
• gli stati raggiungibili sono 68 su 400 possibili.

L’importanza dell’equità. La seconda proprietà vale solo con le clausole FAIRNESS s = 1 e FAIRNESS s = 2, che considerano solo le esecuzioni in cui lo scheduler fa muovere ciascun processo infinite volte. Togliendole, NuSMV trova un controesempio: il processo 1 aspetta, e lo scheduler fa muovere per sempre solo il processo 2, che resta fermo. Non è un difetto del protocollo ma del modello dello scheduler: il model checking costringe a rendere esplicite anche queste ipotesi.

Un’applicazione: verificare un sito web

Le stesse idee si applicano a oggetti molto diversi da un protocollo. Nella tesi di laurea da cui è nato questo argomento (Politecnico di Bari, 2002) un sito web viene trasformato automaticamente in un modello NuSMV, e le proprietà che un buon sito deve avere vengono scritte in CTL. Il programma realizzato, DaWeb, legge le pagine, costruisce il modello e lancia il model checker.

L’idea è considerare il sito come una macchina a stati: la variabile Paging dice su quale pagina si trova il visitatore, la variabile State dice se si sta guardando una pagina (page) o si sta seguendo un collegamento (link). Ogni link della pagina è una transizione possibile; la scelta è non deterministica, perché il visitatore può cliccare qualunque link. Le proprietà tipiche della tesi sono:

• raggiungibilità della home: da ogni pagina si può tornare all’indice, AG (State = page -> EF Paging = index);
• consistenza dei link: ogni collegamento porta a una pagina esistente, AG (State = link -> EX State = page);
• vincoli sul percorso: per esempio, in un negozio online, al pagamento si arriva solo passando dal login;
• proprietà sul contenuto delle pagine (pagine interne o esterne, statiche o dinamiche, dimensione massima, data di aggiornamento), verificate allo stesso modo con variabili aggiuntive.

Ecco un piccolo negozio online nello stile della tesi, con due errori volutamente inseriti: la pagina del prodotto ha un link a offerte, che non esiste, e la pagina di conferma dell’ordine non ha collegamenti.

MODULE main
VAR
  State  : {page, link};
  Paging : {index, catalogo, prodotto, carrello, login, pagamento, conferma, contatti, offerte};
ASSIGN
  init(State)  := page;
  init(Paging) := index;
  next(State) := case
    State = page : link;                                 -- si clicca un collegamento
    State = link & Paging = offerte : link;              -- pagina inesistente: si resta bloccati sul link
    TRUE : page;                                         -- il collegamento porta a una pagina esistente
  esac;
  next(Paging) := case
    State = link : Paging;                               -- arrivati a destinazione la pagina non cambia
    Paging = index     : {catalogo, contatti, login};
    Paging = catalogo  : {prodotto, index};
    Paging = prodotto  : {carrello, catalogo, offerte};  -- offerte non esiste: link rotto
    Paging = carrello  : {login, catalogo};
    Paging = login     : {pagamento, index};
    Paging = pagamento : {conferma, carrello};
    Paging = conferma  : conferma;                       -- pagina senza collegamenti
    Paging = contatti  : index;
    TRUE : Paging;
  esac;
SPEC AG (State = page -> EF (State = page & Paging = index))
SPEC AG (State = link -> EX (State = page))
SPEC AG (Paging = carrello -> !E [ !(Paging = login) U (Paging = pagamento) ])

NuSMV trova entrambi gli errori e li spiega con un controesempio:

• la prima proprietà è falsa: il controesempio è il cammino index, login, pagamento, conferma; dalla pagina di conferma non si torna più alla home;
• la seconda è falsa: il cammino index, catalogo, prodotto, offerte arriva a un link che non porta a nessuna pagina;
• la terza è vera: dal carrello non esiste alcun cammino che arrivi al pagamento senza passare dal login.

Il vantaggio rispetto a un semplice programma che controlla i link uno per uno è che le proprietà riguardano i percorsi e non le singole pagine: “dopo il carrello si passa sempre dal login” non si verifica guardando una pagina alla volta. Per i siti dinamici la tesi aggiunge parametri (per esempio l’utente collegato) e verifica le proprietà per ciascun valore.

Il model checking nella pratica

Il model checking è usato nella progettazione dei circuiti digitali (dopo il famoso errore della divisione del Pentium, nel 1994, Intel ha adottato in modo sistematico la verifica formale per le unità aritmetiche e i protocolli delle cache), nei protocolli di comunicazione, nel software di bordo di aerei e treni e nei sistemi di controllo industriali. Edmund Clarke, Allen Emerson e Joseph Sifakis hanno ricevuto il premio Turing nel 2007 per averlo inventato. I limiti sono l’esplosione degli stati e la necessità di un modello finito fedele: si verifica il modello, non il codice reale, a meno di usare strumenti che estraggono il modello dal codice.

In sintesi

• Il model checking esplora tutti gli stati raggiungibili di un sistema finito e verifica proprietà in logica temporale, restituendo un controesempio se sono false.
• CTL quantifica sui cammini (A, E) e sul tempo (X, F, G, U); LTL valuta le formule su ogni cammino.
• L’algoritmo calcola insiemi di stati con punti fissi: minimo per EF ed EU, massimo per EG.
• NuSMV rappresenta gli insiemi di stati con i BDD e cerca controesempi con il bounded model checking.
• Nell’esempio il protocollo ingenuo viola la mutua esclusione in 6 passi; quello di Peterson è sicuro e vivo, sotto l’ipotesi di uno scheduler equo.
• Lo stesso metodo verifica un sito web: pagine e link diventano stati e transizioni, e NuSMV trova link rotti, pagine senza uscita e percorsi non ammessi.

La tesi completa, con il programma DaWeb, i modelli dei siti e tutte le specifiche, si può leggere qui: tesi completa (PDF).

Il codice

Il modello di Peterson per NuSMV (file peterson.smv). Si verifica con NuSMV peterson.smv; il modello ingenuo è uguale, con gli stati idle, check, setf, crit e senza la variabile del turno.

-- algoritmo di Peterson: bandierina "voglio entrare" e variabile turno t
MODULE main
VAR
  pc1 : {idle, flag, turn, wait, crit};
  pc2 : {idle, flag, turn, wait, crit};
  f1 : boolean;
  f2 : boolean;
  t : {1, 2};
  s : {1, 2};                       -- il processo che fa un passo in questo istante
ASSIGN
  init(pc1) := idle;  init(pc2) := idle;
  init(f1) := FALSE;  init(f2) := FALSE;  init(t) := 1;
  next(pc1) := case
    s = 1 & pc1 = idle : {idle, flag};
    s = 1 & pc1 = flag : turn;
    s = 1 & pc1 = turn : wait;
    s = 1 & pc1 = wait & (!f2 | t = 1) : crit;
    s = 1 & pc1 = crit : idle;
    TRUE : pc1;
  esac;
  next(f1) := case
    s = 1 & pc1 = flag : TRUE;
    s = 1 & pc1 = crit : FALSE;
    TRUE : f1;
  esac;
  next(pc2) := case
    s = 2 & pc2 = idle : {idle, flag};
    s = 2 & pc2 = flag : turn;
    s = 2 & pc2 = turn : wait;
    s = 2 & pc2 = wait & (!f1 | t = 2) : crit;
    s = 2 & pc2 = crit : idle;
    TRUE : pc2;
  esac;
  next(f2) := case
    s = 2 & pc2 = flag : TRUE;
    s = 2 & pc2 = crit : FALSE;
    TRUE : f2;
  esac;
  next(t) := case
    s = 1 & pc1 = turn : 2;         -- cedo il turno all'altro
    s = 2 & pc2 = turn : 1;
    TRUE : t;
  esac;
FAIRNESS s = 1
FAIRNESS s = 2
SPEC AG !(pc1 = crit & pc2 = crit)
SPEC AG (pc1 = wait -> AF pc1 = crit)
LTLSPEC G (pc1 = wait -> F pc1 = crit)

L’uscita di NuSMV:

-- specification AG !(pc1 = crit & pc2 = crit)  is true
-- specification AG (pc1 = wait -> AF pc1 = crit)  is true
-- specification  G (pc1 = wait ->  F pc1 = crit)  is true

Lo stesso algoritmo in Python, con gli stati esplorati uno per uno (model checking esplicito): visita in ampiezza degli stati raggiungibili, ricerca del controesempio più corto e calcolo di come minimo punto fisso.

from collections import deque

# Model checking esplicito: gli stessi due modelli di NuSMV, stati come tuple (pc1, pc2, f1, f2, t, s)

def step_peterson(st, i):
    """Mosse del processo i (1 o 2) nello stato st; restituisce i possibili (pc_i, f_i, t) successivi."""
    pc, f, t = st[i - 1], st[1 + i], st[4]
    other_f, me, other = st[4 - i], i, 3 - i
    if pc == "idle":
        return [("idle", f, t), ("flag", f, t)]
    if pc == "flag":
        return [("turn", True, t)]
    if pc == "turn":
        return [("wait", f, other)]
    if pc == "wait":
        return [("crit", f, t)] if (not other_f or t == me) else [("wait", f, t)]
    return [("idle", False, t)]                      # crit: esce e abbassa la bandierina


def step_naive(st, i):
    pc, f, t = st[i - 1], st[1 + i], st[4]
    other_f = st[4 - i]
    if pc == "idle":
        return [("idle", f, t), ("check", f, t)]
    if pc == "check":
        return [("setf", f, t)] if not other_f else [("check", f, t)]
    if pc == "setf":
        return [("crit", True, t)]
    return [("idle", False, t)]


def successors(st, step):
    s = st[5]                                        # il processo che si muove ora
    out = []
    for pc, f, t in step(st, s):
        new = list(st)
        new[s - 1], new[1 + s], new[4] = pc, f, t
        for s_next in (1, 2):                        # il prossimo processo è scelto in modo non deterministico
            new[5] = s_next
            out.append(tuple(new))
    return out


def explore(step):
    init = [("idle", "idle", False, False, 1, s) for s in (1, 2)]
    parent = {x: None for x in init}
    queue = deque(init)
    while queue:                                     # visita in ampiezza: il primo stato cattivo trovato ha il cammino più corto
        x = queue.popleft()
        for y in successors(x, step):
            if y not in parent:
                parent[y] = x
                queue.append(y)
    return parent


def EF(states, step, goal):
    """Insieme degli stati da cui si può raggiungere goal: minimo punto fisso Z = goal ∪ pre(Z)."""
    Z = {x for x in states if goal(x)}
    while True:
        new = Z | {x for x in states if any(y in Z for y in successors(x, step))}
        if new == Z:
            return Z
        Z = new


bad = lambda x: x[0] == "crit" and x[1] == "crit"
for name, step in (("ingenuo", step_naive), ("Peterson", step_peterson)):
    parent = explore(step)
    states = set(parent)
    viol = [x for x in states if bad(x)]
    print(f"{name}: {len(states)} stati raggiungibili; AG !(crit1 & crit2) {'falsa' if viol else 'vera'}")
    if viol:
        x, path = viol[0], []
        while x is not None:
            path.append(x); x = parent[x]
        print("  controesempio di", len(path) - 1, "passi:", " -> ".join(f"{p[0]}/{p[1]}" for p in reversed(path)))
    good_init = all(x not in EF(states, step, bad) for x in states if x[:5] == ("idle", "idle", False, False, 1))
    print("  stati iniziali fuori da EF(crit1 & crit2):", good_init)

L’esecuzione stampa per il protocollo ingenuo 32 stati raggiungibili, la proprietà falsa e il controesempio di 6 passi idle/idle, check/idle, setf/idle, setf/check, setf/setf, crit/setf, crit/crit; per Peterson 68 stati raggiungibili, come NuSMV, e la proprietà vera, con lo stato iniziale fuori dall’insieme .