Home

Federica EU

1/13

Adriano Peron » 1.Introduzione ai metodi formali di specifica

Formalismi di specifica

Il problema affrontato nel corso è quello della specifica formale di sistemi software e/o hardware.

Con specifica formale si intende la rappresentazione del sistema considerato utilizzando un linguaggio (linguaggio o formalismo di specifica) per il quale siano formalmente definite:

la sintassi
la semantica

La semantica formale del linguaggio di specifica permette di associare ad ogni descrizione (specifica) una struttura matematica (semantica della specifica).

Esempio: UML ha una sintassi ben definita ma non una semantica formale accettata.

Specifica formale di sistemi

La descrizione riguarda usualmente i seguenti aspetti:

Struttura del sistema: la descrizione delle componenti strutturali e delle loro interazioni;
Stato del sistema: la descrizione di una istantanea del sistema (ad esempio, per i sistemi SW avanzamento del controllo e contenuto delle variabili);
Comportamenti del sistema: la descrizione delle sue esecuzioni intese usualmente come sequenze di cambiamento di stato.

Finalità della specifica formale

Finalità della specifica formale:

Fornire una descrizione precisa del sistema (riconducibile a una struttura matematica) che descriva la struttura del sistema e tutti e soli i suoi comportamenti.
Permettere, mediante la struttura matematica derivante dalla specifica (modello semantico della specifica), di valutare esaustivamente le proprietà del sistema specificato (verifica).

Contesto applicativo:

Progettazione e/o modellizzazione HW/SW;
Verifica dei requisiti della progettazione e/o del modello.

Passi del processo di specifica e verifica

Finalità del corso

La finalità del corso è quella di introdurre i concetti, i problemi e le tecniche di base della specifica formale.

L’attenzione si concentra sui seguenti aspetti:

Scelta del formalismo di specifica
Numerosi sono i formalismi presenti in letteratura e ciascuno usualmente meglio si adatta ad una specifica categoria di problemi.
Alcuni formalismi sono supportati da TOOL di specifica e verifica.

Scelta degli aspetti rilevanti da introdurre nella specifica
In funzione della successiva attività di verifica, vanno rappresentati tutti gli aspetti rilevanti del problema tralasciando eventualmente (astrazione) i dettagli non utili allo scopo.

Espressione delle proprietà che la specifica deve soddisfare
Pur essendo strettamente connessa con l’attività di verifica (e trattata superficialmente nel corso), questa attività può richiedere attenzione ed accorgimenti in fase di specifica.

Formalismi di specifica: esempi

Formalismi stato-transizione

Idea: Rappresentazione grafica degli stati globali e delle transizioni di stato innescate da un evento.

Ricadono in questa categoria di formalismi:

Automi regolari, Macchine di Mealy, di Moore, Statecharts di UML, Automi a pila, Macchine ricorsive, Automi temporizzati etc.

Esempio di grafo Stato-Transizione per una macchina distributrice di caffè.

Formalismi di specifica: esempi (segue)

Reti di Petri

Idea: Rappresentazione grafica di stati spazialmente distribuiti (Place) contenitori di elementi informativi (token) e di transizioni che connettono Place.

Lo scatto della transizione dipende dal contenuto dei Place e lo altera.

Esempio di Rete di Petri.

Formalismi di specifica: esempi (segue)

Algebre di processi

Idea: I processi sono composti a partire da processi elementari mediante operazioni e assumono la forma di espressioni algebriche (termini).

Un termine rappresenta il sistema e il suo stato.

Le regole di trasformazione dei termini (semantica delle operazioni) determinano il comportamento del sistema.

Esempi di formalismi: CCS, CSP, Pi-calculus etc.

Esempio di definizione di termini in CCS per la macchina distributrice di caffè.

Formalismi Stato-Transizione

I formalismi esaminati in questo corso appartengono alla categoria dei formalismi Stato-Transizione

Vantaggi:

Formalismi tra i più tradizionali e diffusi;
Natura grafica che ne facilita l’intuizione;
Semplice uso e supporto di ambienti di progettazione.

Rappresentazione in forma di grafo

Elementi costitutivi:

Stati (nodi del grafo);
- Rappresentano naturalmente lo stato del controllo del sistema. Lo stato in assenza di strutture dati può implicitamente anche essere associato a informazioni sui dati.
Transizioni (archi del grafo);
- Rappresentano generalmente il passo di avanzamento del controllo.
Etichette transizioni (etichette degli archi);
- Rappresentano le condizioni per il passo di avanzamento del controllo e gli eventuali side effect aggiuntivi.
(Eventuali) strutture dati aggiuntive (non rappresentate graficamente).

Struttura transizioni

Struttura generale di una transizione:

Trigger
Condizione per lo scatto della transizione dipendente da stimoli esterni al sistema (ambiente);

Condizione
Condizione per lo scatto della transizione dipendente da stimoli interni al sistema (ad esempio contenuto delle strutture dati);

Azione

Side effect dello scatto della transizione (ad esempio, output verso l’ambiente o aggiornamento delle strutture dati).

Struttura della transizione.

Stati Finiti/Infiniti

Nel corso si considerano formalismi sia in grado di descrivere sistemi a stati finiti, sia a stati infiniti.

L’infinitezza delle stato può essere determinata da:

variabili o strutture dati che assumono valori in domini illimitati;
strutture di controlo che permettono forme di ricorsione o attivazione dinamica di processi.

Formalismi per sistemi a stati finiti considerati nel corso

Macchine a stati finiti (FSM) deterministiche e non deterministiche;
Automi di Büchi;
FSM gerarchiche;
Statecharts.

Formalismi per sistemi a stati infiniti considerati nel corso

Macchine ricorsive (RSM);
Automi a pila (PDA);
Automi temporizzati (TA).

Criteri di contronto per i formalismi

I formalismi verranno confrontati in relazione ai seguenti Criteri

Espressività

Intrinseca capacità del formalismo di descrivere propriamente il sistema da specificare.
E’ un criterio che permette di stabilire raffronti quantitativi tra formalismi (fissato il dominio di confronto).

Naturalezza descrittiva

Capacità del formalismo di descrivere il sistema mantenendo in forma esplicita le caratteristiche rilevanti del sistema.
Un formalismo sufficientemente espressivo per un problema può essere inadeguato a rappresentarlo in modo naturale.
Se soddisfatto consente specifiche leggibili, estranee ad aspetti implementativi e alla codifiche di aspetti non esprimibili esplicitamente.
E’ criterio qualitativo.

Criteri di confronto per i formalismi (segue)

I formalismi verranno confrontati in relazione ai seguenti Criteri

Succintezza

Criterio che si riferisce alle dimensioni della specifica e riguarda la capacità del formalismo di esprimere alcuni problemi in maniera concisa.
E’ un criterio quantitativo che permette di stabilire raffronti tra formalismi (usualmente della stessa capacità espressiva).

Proprietà di chiusura

Criterio che si riferisce alla possibilità di comporre le specifiche mediante opportune operazioni ottenendo specifiche composte a partire da specifiche semplici.
Esempi classici sono le operazioni di unione, intersezione e complemento (se significative rispetto al dominio semantico).

Criteri di confronto per i formalismi (segue)

I formalismi verranno confrontati in relazione ai seguenti Criteri

Proprietà di decidibilità e complessità

Determinante è la proprietà della raggiungibilità di uno stato del sistema.
Decidibilità e complessità hanno notevole peso rispetto alla possibilità effettiva di verifica.

Tecniche e tool di verifica

Il fine principale della specifica formale è di fornire unmodello formale del sistema che permetta la verifica (semi-)automatica delle proprietà attese. Rilevante la presenza di ambienti che permettano: