Home

Federica EU

1/14

Adriano Peron » 2.Semantica dei formalismi di specifica

Semantica dei formalismi di specifica

Un formalismo di specifica deve essere dotato di semantica formale.

La semantica formale del linguaggio di specifica permette di associare ad ogni specifica una struttura matematica.

La struttura matematica adottata tradizionalmente è il:

Labelled Transition System (LTS)

Descrizione dei comportamenti;
Input per le attività di verifica.

Specifica e Model Checking

Semantica mediante LTS: vantaggi

Vantaggi:

Gli LTS sono le strutture di input dei sistemi di verifica (model checker);

Consento di valutare quantitativamente la similarità tra diverse specifiche.

Se la struttura delle etichette è adeguata, si possono confrontare specifiche scritte in linguaggi diversi confrontando gli LTS.

Confronto di specifiche

Labelled Transition System: definizione

Un LTS su un alfabeto $\Sigma$ , è un grafo con archi etichettati da simboli dell’alfabeto.

Formalmente un LTS è una terna $\langle S,S_0,\Delta \rangle$ ,

S, è l’insieme degli stati;

$S_0 \subseteq S$ è il sottoinsieme degli stati iniziali;

$\Delta \subseteq S \times \Sigma \times S$ è la relazione di transizione tra stati; se $\langle s,a,s' \rangle \in \Delta$ il sistema può transire dallo stato s allo stato s’ e l’azione osservabile all’esterno è a.

L’LTS condivide la natura grafica dei formalismi Stato-Transizione.

L’LTS è in generale una struttura di più basso livello rispetto al linguaggio di specifica.

Labeled Transition System

Stato: corrisponde ad una istantanea del sistema descritto (stato del controllo e delle strutture dati).
Transizione: Rappresenta una transizione di stato del sistema rispetto ad un evento simboleggiato dalla etichetta dell’arco.
Comportamento: sequenza di transizioni (finita o infinita) che rappresenta un cammino nell’LTS a partire da uno stato iniziale.

$s_0 \stackrel{a_0}{\longrightarrow} s_1<br /> \stackrel{a_1}{\longrightarrow} \ldots<br /> \stackrel{a_{i-1}}{\longrightarrow} a_i \mbox{ con } \langle<br /> s_{j-1},a_{j-1},s_j \rangle \in \delta, \ \forall\ 0 \leq j-1 < i$

I comportamenti del sistema sono tutti e soli i cammini dell’LTS che iniziano dallo stato inziale.

Traccia: l’informazione osservabile di un comportamento è solo la sequenza di simboli che etichetta il cammino $a_0, a_1, \ldots a_i$ .

Equivalenze per LTS

Un sistema può essere descritto ‘equivalentemente’ mediante specifiche sintatticamente diverse.

Problema: Come riconoscere se due specifiche descrivono il medesimo sistema?

Intuitivamente due descrizioni che determinano gli stessi comportamenti descrivono lo stesso sistema.

Il confronto non deve essere condotto sulla descrizione (sintassi) ma sulla semantica (LTS) che descrive i comportamenti.

Criteri di equivalenza per le specifiche sono suggeriti da criteri di raffronto degli LTS.

E’ possibile esprimere una ricca gamma di criteri di equivalenza adatti alle diverse necessità.

Equivalenza LTS: esempi

Esempio d’uso di criteri di equivalenza: metodologia di sviluppo modulare delle specifiche.

Sostituendo nella specifica di un sistema un modulo con un modulo ad esso equivalente il comportamento del sistema non dovrebbe cambiare.

Richiede un forte criterio di equivalenza rispetto ai comportamenti.

Sviluppo modulare delle specifiche

Equivalenza LTS: esempi (segue)

Esempio d’uso di criteri di equivalenza: sviluppo top-down di una specifica.

Quando si raffina una specifica (implementazione della specifica) l’implementazione non deve introdurre comportamenti non previsti nella specifica.

Richiede un criterio di equivalenza in grado di astrarre dai dettagli introdotti nell’implementazione e non presenti nella specifica.

Sviluppo top-down delle specifiche

Equivalenze LTS

Un criterio troppo forte: isomorfismo di LTS.

Un criterio troppo debole: equivalenza per tracce.

Due LTS sono equivalenti per tracce se hanno lo stesso insieme di tracce.

Es. Tracce(LTS1)=Tracce(LTS2)=

{10,10.caffè,10.thè}

Sistemi equivalenti ma ……:

LTS1: si inserisce la moneta e la macchina sceglie la bevanda.
LTS2: si inserisce la moneta poi si sceglie la bevanda.

Due LTS equivalenti per tracce.

Bisimulazione forte

Dati due LTS $\langle S_1,S_{0,1}\Delta_1\rangle\ \mbox{ e } \langle S_2,S_{0,2}\Delta_2 \rangle \mbox{su } \Sigma$ ,

una bisimulazione forte è una relazione $R \subseteq S_1 \times S_2$

che soddisfa il seguente requisito: se $s_1\ R\ s_2$ allora deve valere

(1) $\forall \lambda \in \Sigma \mbox{ tale che } s_1 \stackrel{\lambda}{\longrightarrow} s'_1\in\Delta_1,\exists s'_2\in S_2 \mbox{ tale che }s_2\stackrel{\lambda}{\longrightarrow} s'_2 \in\Delta_2 \mbox{ e } s'_1\ R\ s'_2$ .

(2) $\forall \lambda \in \Sigma \mbox{ tale che } s_2 \stackrel{\lambda}{\longrightarrow} s'_2 \in\Delta_2, \exists s'_1\in S_1 \mbox{ tale che } s_1 \stackrel{\lambda}{\longrightarrow} s'_1 \in\Delta_1 \mbox{ e } s'_1\ R\ s'_2$ .

Esempio di bisimulazione (insensibile alle duplicazioni)

Le seguenti relazioni sono bisimulazioni

$\begin{array}{l}R_1= \{\langle s_4,r_3\rangle \} \\R_2=\{\langle s_5,r_3\rangle \} \\R_3=\{ \langle s_2,r_2\rangle,\langle s_4,r_3\rangle\} \\R_4=\{ \langle s_3,r_2\rangle,\langle s_5,r_3\rangle \} \\R_5=\{ \langle s_1,r_1\rangle ,\langle s_2,r_2\rangle,\langle s_4,r_3\rangle,\langle s_3,r_2\rangle,\langle s_5,r_3\rangle\}\}\end{array}$

LTS bisimili (duplicazione).

Proprietà della bisimulazione forte

Se R e S sono due relazioni di bisimulazione forte anche le seguenti sono relazioni di bisimulazione forte:

$\begin{array}{l}R \cup S \mbox{ (unione)}\\R^{-} \mbox{ (relazione inversa)}\\R \circ S \mbox{ (relazione composta)}\end{array}$

L’unione arbitraria di relazioni di bisimulazione è una relazione di bisimulazione.

Questo permette di affermare l’esistenza della massima bisimulazione forte, definibile come l’unione di tutte le bisimulazioni:

$\approx \bigcup \{R : R \mbox{ \`e una bisimulazione forte}\}.$

LTS bisimili

Due LTS sono fortemente bisimili se la coppia dei loro stati iniziali appartiene alla massima bisimulazione forte.

Bisimulazioni:

$\begin{array}{l}R_1= \{\langle s_4,r_3\rangle \} \\R_2=\{\langle s_5,r_3\rangle \} \\R_3= \{\langle s_4,r_4\rangle \} \\R_4=\{\langle s_5,r_4\rangle \} \\R_5=\{\langle s_4,r_3\rangle,\langle s_5,r_3\rangle,\langle s_4,r_4\rangle,\langle s_5,r_4\rangle\}\end{array}$

R5 è la massima bisimulazione e non contiene la coppia di stati iniziali $\langle s_1,r_1 \rangle$ .

LTS non bisimili.

LTS bisimili

Esempio di LTS bisimili: unfolding di ciclo.

Bisimulazione:

$R = \{\langle s_1,r_i\rangle: i\geq 1 \}$

R contiene la coppia di stati iniziali $\langle s_1,r_1 \rangle$ .

Si osservi che LTS1 ha un solo stato e LTS2 un numero infinito di stati.

LTS bisimili.

Bisimulazione forte

La bisimulazione forte è una nozione adeguata per lo sviluppo modulare.

Due LTS fortemente bisimili soddisfano lo stesso insieme di proprietà espresse mediante alcune logiche standard (ad esempio, logica temporale lineare).

La nozione di bisimulazione forte è un criterio troppo forte per lo sviluppo top-down di specifiche (specifica-implementazione).