Modellazione e analisi di sistemi:

Modellazione e 
analisi di sistemi
Appunti di Maurizio Fortunati
Università degli Studi di Milano
Facoltà di Scienze e Tecnologie
Corso di Laurea Magistrale in Sicurezza informatica (Classe LM-66)
Esame di Modellazione e analisi di sistemi
Docente: Elvinia Riccobene 
Anno accademico - 2018/2019Modellazione e analisi dei 
sistemi 
Appunti a cura di Maurizio Fortunati 
Università degli Studi di Milano – Corso Magistrale in Sicurezza Informatica LM-66 
Corso tenuto da Elvinia Riccobene [mail] 
AA 2018/ 19 
Sito Docente 
Link Ariel - Lucidi 
Link Ariel - Video lezioni 
Link SourceForge – Asm examples 
V3.7 – 12 Febbraio 2020 
Sommario 
Sommario ..................................................................................................................................................................................... 2 
Introduzione al corso ........................................................................................................................................................... 5 
ASM I, Prima parte .................................................................................................................................................................. 6 
Riassunto Automi a stati finiti ....................................................................................................................................................... 6 
Da FSM a ASM ......................................................................................................................................................................................... 6 
Esempi porta girevole e macchinetta caffè ...................................................................................................................... 8 
ASM I, Seconda parte ......................................................................................................................................................... 11 
Stato Asm ................................................................................................................................................................................................. 11 
Domini ASM ............................................................................................................................................................................................. 13 
ASM II, Prima parte .............................................................................................................................................................. 15 
Regole di transizione ........................................................................................................................................................................ 15 
Esempi Advanced Clock e Semaforo .................................................................................................................................. 15 
ASM II, Seconda parte ....................................................................................................................................................... 19 
Esempio SluiceGate( Chiusa) .................................................................................................................................................... 19 
Esem pio fattoriale .............................................................................................................................................................................. 21 
Esempio Swap sort vettore ......................................................................................................................................................... 21 
AsmetaL - Linguaggio Strutturale ............................................................................................................................. 23 
Name .......................................................................................................................................................................................................... 24 
Header ....................................................................................................................................................................................................... 24 
Body ............................................................................................................................................................................................................. 24 
main rule ................................................................................................................................................................................................... 26 
Inizializzazione ...................................................................................................................................................................................... 26 
AsmetaL - Linguaggio delle definizioni .................................................................................................................. 26 
Dichiarazione dei domini .............................................................................................................................................................. 26 
Type Domain: .................................................................................................................................................................................................... 27 
Structured Domain ...................................................................................................................................................................................... 28 
Dichiarazione delle funzioni ........................................................................................................................................................ 31 
Funzioni statiche ............................................................................................................................................................................................. 32 
Funzioni dinamiche ...................................................................................................................................................................................... 32 
Funzioni derivate ............................................................................................................................................................................................ 34 
Invarianti.................................................................................................................................................................................................... 35 
Locazioni e aggiornamenti ......................................................................................................................................................... 35 
Convenzioni sugli ID ........................................................................................................................................................................ 36 
AsmetaL - Linguaggio dei termini ............................................................................................................................. 37 
AsmetaL - Linguaggio delle regole .......................................................................................................................... 38 
Skip, Update, Par, Seq .................................................................................................................................................................... 38 
Conditional rule (If, let, forall, choose, switch case) ................................................................................................. 40 
Macro call rule ..................................................................................................................................................................................... 43 
Extend Rule – Riserva di una ASM ........................................................................................................................................ 44 
ASM multi agenti ................................................................................................................................................................. 46 
Definizione .............................................................................................................................................................................................. 46 
ASM Sincrone .................................................................................................................................................................................................... 47 
ASM Asincrone ................................................................................................................................................................................................ 47 
Multi Agent in AsmetaL ................................................................................................................................................................. 48 
Case study – popolazione .................................................................................................................................................................... 48 
AsmetaL - Protocollo Needham-Schroeder ........................................................................................................ 50 
AsmetaL - Esempi ................................................................................................................................................................ 51 
Esem pio ATM ........................................................................................................................................................................................ 51 
Esame 2 luglio 2013 – sbarra cancello automobile .................................................................................................. 56 
Multi Agent ASM - produttore consumatore ................................................................................................................ 57 
Multi Agent ASM - Bambini e caramelle ......................................................................................................................... 60 
Popolazione ........................................................................................................................................................................................... 62 
FrameW ork ASM – Ground Model ............................................................................................................................. 66 
Design ....................................................................................................................................................................................................... 66 
Costruzione del ground model - GM ......................................................................................................................................... 67 
Raffinamento del modello ................................................................................................................................................................... 68 
Esempio chiusa .............................................................................................................................................................................................. 70 
FrameW ork ASM – Analisi .............................................................................................................................................. 74 
Logiche temporali ............................................................................................................................................................................. 74 
Automi di Kripke ............................................................................................................................................................................................. 74 
La CTL -  Computational tree logic .............................................................................................................................................. 75 
Equivalenze Canoniche .......................................................................................................................................................................... 80 
Algoritmo di model Checking ........................................................................................................................................................... 80 
Algoritmo di Labeling - Regole di etichettatura ............................................................................................................... 81 
Esercizi CTL ....................................................................................................................................................................................................... 83 
Algoritmo SAT ..................................................................................................................................................................................... 86 
Algoritm i SAT (EX, EU, AF) ................................................................................................................................................................... 88 
Esercizi SAT ....................................................................................................................................................................................................... 90 
Verifica di proprietà temporali ................................................................................................................................................. 94 
Proprietà ................................................................................................................................................................................................................ 94 
Pattern Noti - Practical patterns of Specifications 2 ..................................................................................................... 97 
Esercizi sulle proprietà temporali .................................................................................................................................................. 97 
OBDD - Ordered Binary Decision Diagrams ............................................................................................................... 10 0 
Teoria .................................................................................................................................................................................................................... 10 0 
Regole di compattezza .......................................................................................................................................................................... 10 1 
Esercizio di compattezza ..................................................................................................................................................................... 10 2 
Alberi BDD ......................................................................................................................................................................................................... 10 4 
Vantaggi di utilizzare ROBDD .......................................................................................................................................................... 10 5 
Calcolo del ROBDD e del SAT ....................................................................................................................................................... 10 5 
NuSMV ................................................................................................................................................................................................................ 10 6 
Preparazione Esame Teorico ...................................................................................................................................... 110 
Preparazione Esame di laboratorio ......................................................................................................................... 117 
Note su Asmeta tools ...................................................................................................................................................... 121 
Codici Sorgenti ................................................................................................................................................................... 122 
Template ................................................................................................................................................................................................ 122 
Advanced Clock ............................................................................................................................................................................... 123 
Cena dei filosofi ................................................................................................................................................................................. 124 
Adolfo ....................................................................................................................................................................................................... 126 
ADOLFO V2 .......................................................................................................................................................................................... 134 
Ex am 15 0 1 20 19 – prod consumatore ............................................................................................................................. 136 
Morra cinese ........................................................................................................................................................................................ 139 
ATM ............................................................................................................................................................................................................ 141 
Tris – Tic Tac Toe ............................................................................................................................................................................. 145 
Lotto .......................................................................................................................................................................................................... 147 
Tombola con la seq .................................................................................................................................................................................. 149 
Token ........................................................................................................................................................................................................ 151 
Container ................................................................................................................................................................................................ 153 
Popolazione ......................................................................................................................................................................................... 154 
Indice delle figure ............................................................................................................................................................. 156 
 
  
Introduzione al corso  
Riferimenti 
Lezione 201 8-02-28-11.0 0 .49 
Introduzione 
Obiettivo del corso, è quello di poter dimostrare che un sistema godi di certe proprietà. 
Come faccio a provare queste proprietà? 
Devo prima fare una rappresentazione astratta del sistema e per farla utilizzo i linguaggi di 
specifica. 
Un linguaggio di specifica permette di poter descrivere il sistema in modo univoco e non 
ambiguo, con il quale si potrà descrivere i requisiti del sistema creando un modello che è la 
rappresentazione astratta del sistema. 
Con questo modello è possibile effettuare delle analisi, definite validazione e verifica, che 
sono basate su simulazione, testing e model checking. 
Validazione: processo di valutazione di un sistema o di una componente per l’intero ciclo di 
sviluppo per determinare se esso soddisfa i requisiti specificati. 
I requisiti, sono documenti scritti in linguaggio naturale che descrivano il sistema come lo 
vuole il cliente. 
Validare significa valutare se il sistema che ho realizzato alla fine o durante lo sviluppo sia 
corretto rispetto ai requisiti. Validazione controlla i requisiti  
Si effettua tramite la simulazione e il testing 
Verifica: Processo di valutazione di un sistema o di una componente per determinare se i 
prodotti di una data fase di sviluppo soddisfano le condizioni (proprietà) imposte allo stato di 
quella fase. 
Dimostrare che il sw che si sta sviluppando in qualsiasi punto soddisfi alcune proprietà. 
Verifica correttezza di proprietà  
Si procede attraverso tecniche di theorem prover e model checker. 
Ovviamente non è possibile testare tutto a carta e penna, quindi utilizzeremo dei sistemi 
automatici. 
Quindi nel corso si studieranno 3 cose, linguaggimetodi tool. 
Metodi formali. 
Sono notazioni rigorose e dal significato preciso, dei simboli che non permettono ambiguità. 
Formalismi operazionali: forniscono una descrizione del comportamento del sistema in 
termini di operazioni di una macchina astratta, li utilizzeremo per effettuare la validazione. 
Per fare simulazione del modello. 
Esempi di formalismi operazionali sono: ASM, B & Z Method, SCR, Petri 
 
Formalismi dichiarativi, descrive il sistema in termini di proprietà che devono soddisfare; li 
utilizzeremo per la fase di verifica. 
Esempi di formalismi dichiarativi sono: Logica temporale, trio, algebre dei processi. 
 
  
ASM I, Prima parte 
Riferimenti 
Video lezione di riferimento 20 18 -02-28-13.0 5.27 lucidi 1 a 26 
Riassunto Automi a stati finiti  
Un automa, chiamato anche: macchina stati finiti, in inglese FSM (finite state macchine) è una 
notazione formale che permette la rappresentazione astratta del comportamento di un 
sistema. 
La FSM è composta da una tupla di 3 elementi:  
• S insieme finito di stati 
• I insieme finito di eventi input 
• δ che è la funzione di transizione  che connette ogni stato S a S’ per via di un input, 
Diagramma di stato è la rappresentazione grafica di una FSM. 
Le FSM sono molto basilari e con esse non si riesce a modellare la memoria o l’output, per 
questo motivo sono state introdotti: 
Automi di Mealy e di Moore per modellare l’output. 
Le FSM estese per modellare la memoria della macchina. 
Le FSM di comunicazione per modellare la comunicazione, ad esempio nelle macchine nei 
sistemi distribuiti. 
FSM temporizzate per modellare il tempo, dove si può definire un tempo di durata della 
transizione. 
Infine si giunge alle macchine di stato di UML o FSM di Harel che permettono di modellare, 
lo stato, input, output attività interne e trans interne e sotto macchine. 
Vedremo altre estensioni: 
ASM – Abstract state machine FSM con stati generalizzati 
Automi di Kripke lo stato porta informazioni di una proprietà che è valida in esso. 
 
Da FSM a ASM 
Agganciandoci al concetto di modello delle FSM vediamo la ASM. 
Per il momento non concentrarti sulla sintassi o sulla forma ma sull’idea di 
funzionamento, perché alcuni dettagli o pezzi di codice non vengono inseriti o 
spiegati per brevità. 
Il linguaggio asm verrà spiegato in modo dettagliato più avanti 
Le differenze che si possono notare riguardano la concezione degli stati, che risultano più 
complessi nelle ASM e le condizioni di input e le azioni di output. 
Nelle FSM si ha un alfabeto finito mentre nelle ASM, si può avere un input qualsiasi. 
Introduciamo le asm con un modello di esempio; un orologio digitale che mostra l’ora che 
viene aggiornata ad ogni delta di tempo, attraverso il DisplayTime.  
Le macchine a stati sono costituite da due concetti, gli stati e le transizioni, andremo a 
sviluppare il concetto di stato e poi quello di transizione delle ASM. 
 
 
4 Funzioni: 
CurrTime: Rappresenta il tempo corrente ed è di tipo reale 
DisplayTime: variabile che rappresenta l’ora 
Delta: un numero reale 
+ : operazione di somma che dati due reali restituisce un reale, Real x Real  
 
In questo caso utilizziamo solamente un insieme di funzioni matematiche, cioè l’insieme dei 
reali. 
CurrTime e DisplayTime le possiamo vedere come delle variabili, il delta come una costante 
e il + come una funzione. 
In ASM tutto viene considerato come una funzione con differenze in base all’arietà (ovvero il 
numero di argomenti presenti). 
In questo esempio le funzioni utilizzate hanno arietà zero tranne il + che ha arietà 2.  
Quindi si possono distinguere funzioni con arietà zero e diverso da zero. 
Successivamente si procede con la costruzione degli stati strutturati che modellano dati 
complessi arbitrari e operazioni per la manipolazione dei dati, sostituendo uno stato non 
strutturato con un’algebra. 
Le transizioni nelle FSM vengono rappresentate con delle frecce, mentre in ASM 
utilizzeremo una formula  simile all’ if then else  if condition then updates . 
È possibile costruire delle regole con diversi costruttori: 
• parallelismo (par) ed azioni sequenziali (seq) 
• iterazioni (while) en invocazioni di sottomachine 
• non determinismo (choose) e parallelismo sincrono non limitato (forall) 
• multi-agenti sincroni e asincroni 
Nella programmazione della ASM andremo a distinguere header, body,main rule, 
initialization:  
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
Figura 1 : Primo esempio di ASM 
Per poter passare da una FSM ad una ASM si può utilizzare il seguente schema: 
 
Figura 2: Da FSM a ASM 
dove: 
• ctl_state è una variabile che rappresenta lo stato corrente e può prendere come valore 
uno stato di controllo (in un insieme finito) 
• i, j1 , j2, … , jn sono stati interni di controllo (i valori di ctl_state) 
• ck (k=1 , 2, … , n) rappresentano le condizioni di input 
• Rk le azioni della macchina 
Facendo un paragone tra fsm e asm si può notare che nelle Fsm esiste un unico stato di 
controllo (ctl_state), che può assumere valori in un insieme finito di un certo tipo. 
Mentre nelle ASM lo stato è più complesso 
Le condizioni di input e le azioni di output, nelle fsm sono un alfabeto finito, mentre nelle 
ASM l’input può avere qualsiasi input. 
Esempi porta girevole e macchinetta caffè 
Porta girevole 
 
 
Figura 3: Esempio Porta girevole 
Gli stati sono i 5 rettangoli (open, stayopen,..) e li inserisco nell’inizializzazione, mentre le 
funzioni da simulare sono le 4 azioni che interconnettono gli stati (click, complete, click + 
ctl_state che serve per verificare lo stato) 
 
Si possono vedere le asm come dello pseudo codice con alcune differenze e caratteristiche. 
Giusto per citarne qualcuna e anticipare alcuni concetti, si vedrà che alcuni stati possono 
scattare contemporaneamente.  
Il click e il time-out sono delle entità che rappresentano il flusso dell’ambiente sul sistema.  
Queste funzioni si andranno a distinguerle tra monitorate e controllate. 
Monitorate sono quelle che arrivano dall’ambiente, il valore viene dato ad ogni stato 
dall’ambiente. 
Il simulatore fornisce dei valori, mentre dal punto di vista semantico è l’ambiente che li 
fornisce e non la macchina che ne effettua l’aggiornamento; la macchina sa che quando 
avrà bisogno di certi dati li potrà ottenere dall’ambiente come una specie di oracolo. 
Mentre quelle cambiate dalla macchina sono quelle controllate. 
Sarà compito delle regole di transizione di aggiornare tali valori, la macchina aggiornerà la 
funzione ctl_state mentre quelle controllate dall’ambiente sarà compito del simulatore 
aggiornarle. 
 
Esempio macchinetta caffè 
 
Figura 4: Esempio macchinetta caffè 
Versione tramite EFSM: 
In questo caso è stata utilizzata una macchina estesa in quanto c’è bisogno della memoria 
per contare le monete e le bevande scelte.  
Si può notare che tutte le transazioni seguono una sequenza simile. In esempio quella rossa 
Azione che attiva la transazione ins (50cent) 
[possibile guardia che può bloccare la transazione][coin<25&…] 
aggiornamento delle variabilicoin≔coin+1, … 
/output /eroga(milk) 
 
In ASM: 
Segnatura/ definizione 
Bisogna definire il tipo di monete e il tipo di prodotto erogato tramite il dominio 
Monete half/ one e prodotto caffè e latte, quindi:  
enum domain cointype = {HALF|ONE} 
enum domain product ={MILK | COFFE} 
Questi due elementi non sono infiniti, perché il latte e il caffè possono essere erogati al 
massimo 1 0 volte e il contenitore delle monete ne contiene al massimo 25. 
Si inseriscono altre due variabili che vengono chiamati domini, che appartengono all’insieme 
degli interi. 
signature: 
domain QuantityDomain subsetof integer 
domain CoinDomain subsetof integer 
 
definitions: 
  domain QuantityDomain={0..10} 
 domain CoinDomain ={0..25} 
 
Si definisce una funzione (available) che dato un prodotto (caffè o latte), ne restituisca la 
quantità presente. 
Questa funzione associa ad ogni prodotto la sua quantità 
controlled available: productQuantityDomain 
 
Si definisce l’insieme delle monete, che fanno parte del dominio delle monete. 
controlled Coins: CoinDomain 
e si definisce il dominio delle monete inserite 
controlled insertedCoin: CoinType 
inizializzazione: 
default init s0: 
 function coins=0 
function available($p in product)=10 
 
regole: 
main rule r_Main = 
if(coins < 25) then 
if(insertedCoin = HALF) then 
if(available(MILK) > 0) then 
r_serveProduct[MILK] 
endif 
else 
if(available(COFFEE)>0) then 
      r_serveProduct[COFFE] 
endif 
endif 
endif 
endif 
 
Volendo si può accorpare in un’unica regola per servire i prodotti, utilizzando una regola con 
parametro. 
Rule r_serveProduct($p in Product)= 
par 
Available($p):= available($p)-1 
 Coins:= coins+1 
endpar 
  
ASM I, Seconda parte 
Riferimenti 
Video lezione di riferimento 20 18 -03-07-10 .38 .44 lucidi da 27 a 42 
Stato Asm 
Nelle ASM gli stati sono associati a un insieme di valori di qualsiasi tipo, memorizzate in 
apposite locazioni. 
Matematicamente una locazione è definita come Il valore di una funzione f  f(x1, … , xn) nello 
stato S, cioè di funzioni con valore.  
Es. availab le (LATTE) = 10 
Potremmo pensare alle locazioni come a delle variabili, ma non sono spazi in memoria che 
contengono un valore, sono invece occupati dal risultato di una certa funzione con un certo 
parametro. 
Per variabili si intende un valore, mentre per locazione la coppia la funzione + parametro. 
Questo ci porta dire che le transizioni di stato delle FSM corrispondono alle transizioni di 
stato delle ASM con aggiornamenti dei valori contenuti nelle locazioni. 
Definizione formale dello stato di una ASM  
Fissato un vocabolario, uno stato: è l’insieme non vuoto (super universo) delle interpretazioni 
delle funzioni del vocabolario. 
Iniziamo a definire cosa sia un vocabolario. 
 
Vocabolario 
Un vocabolario è una collezione finita di nomi e funzioni, un insieme di nomi che non hanno 
significato fino a quando non glielo diamo noi. 
Dare significato = dare un’interpretazione. 
Si può pensar al vocabolario come alla dichiarazione di tutte le funzioni che verranno usate. 
Le funzioni dichiarate possono essere dinamiche o statiche. 
Dinamiche, se il significato può cambiare di stato in stato, mentre statiche se rimane lo 
stesso per tutta l’esecuzione. 
Nei linguaggi di programmazione classici, siamo abituati ad utilizzare le variabili, in asm le 
variabili come le conosciamo noi, non esistono, perché tutto è funzione. 
Per modellare una variabile bisogna creare una sono funzioni dinamica che abbia arietà zero. 
Mentre per definire le costanti, utilizzo delle funzioni statiche con arietà 0. 
Il concetto di funzione matematica racchiude il concetto di variabili, costanti, funzioni e 
insieme. 
Dal punto di vista matematico, se voglio modellare un sistema e rappresentare in astratto lo 
stato attuale mi basta solo definire un insieme di funzioni e definire come queste funzioni 
cambiano di interpretazione passando allo stato successivo. 
Avendo un vocabolario, che contiene dei nomi, associo ai nomi delle funzioni alle quali 
assegno delle interpretazioni e possono essere statiche o dinamiche a seconda del fatto che 
la loro interpretazioni cambia o meno nel tempo. 
Ogni vocabolario ASM contiene sempre 3 funzioni statiche di arietà zero (costanti statiche) 
undef, true e false. 
I numeri sono costanti numeriche che l’utente può definire a piacimento come ad esempio: 
votomin=18 
Il valore undef serve per poter dare la possibilità di far diventare le funzioni totali, perché non 
sempre lo zero ha la stessa interpretazione, ad esempio nella moltiplicazione e nella 
somma, lo zero ha due significati diversi.  
Le funzioni statiche con arietà maggiore di zero sono definite tramite una legge fissa e di 
solito sono le operazioni tra numeri, +, -, *… oppure tra booleani (op logici come and or… ) 
Le funzioni dinamiche con arietà zero sono le classiche variabili. 
Esempio di vocabolario: Σ bool  
Che è il vocabolario di tutte le funzioni booleane. 
In questo vocabolario si inseriscono diversi elementi che sono: 
Due simboli 0 e 1 che sono due costanti. 
Una funzione con arietà 1 che è il NOT con il simbolo “-”. 
Due funzioni binarie chiamate “+ ” “*” per OR e l’AND. 
Per il momento abbiamo solamente definito il vocabolario senza darne un’interpretazione. 
 
Prima di darla cerchiamo di definire il concetto di stato. 
Fissato un vocabolario Σ (che è un insieme di nomi), uno stato A del vocabolario Σ è un insieme 
non vuoto X, detto super universo di A, con le interpretazioni dei nomi delle funzioni di Σ. 
 
Quindi fisso un vocabolario, definisco le interpretazioni dei simboli e definisco un insieme 
non vuoto X che comprende i simboli con le loro interpretazioni, ecco definito il super 
universo A 
Se f è un nome di funzione n-aria di Σ, allora la sua interpretazione f A è una funzione da Xn a 
X. 
Se c è un nome di costante di Σ, allora la sua interpretazione A è un elemento di X 
Adesso vedremo due esempi di stato su Σ  
Ese m p i o 1: 
 
Stiamo facendo discorsi a basso livello, quindi lo zero, l’uno, il meno, il più e l’asterisco devo 
considerarli solo come dei simboli, come dei disegni che fanno parte del vocabolario Σ Bool 
che per il momento non hanno significato. 
 
Per dargli un significato creo lo stato A che è composto dai numeri chiamati anche costanti 0 
e 1. 
Quindi per questo motivo che ai simboli 0, 1 , -, +, * ho ad apice A per indicare che 
attualmente stiamo considerando l’interpretazione nel contesto dello stato A. 
 
I simboli a e b sono da interpretare come qualsiasi valore del dominio cioè che possono 
essere solo 0 e 1 . 
Con questa logica procedo ad analizzare le righe. 
Lo zero, simbolo che ho messo all’interno del mio vocabolario Σ Bool
 
nella mia algebra che 
ha come X come super universo gli associo la costante 0. 
Stessa cosa per il simbolo 1. 
 
Al simbolo – seguito da un valore arbitrario a gli conferisco l’interpretazione 1 -a. 
E così via. 
 
 
 
Domini ASM 
Si possono dividere il super universo in domini o sotto universi in base alla loro funzione 
caratteristica, cioè creo una funzione che risulti vera solamente per gli elementi presenti in 
quel dominio. 
Nella slide si fa l’esempio che il super universo è composto da i seguenti elementi {1,2,3, a, b, 
mario, pippo} che si possono dividere nei domini interi char e string, questi domini sono 
guidati da una funzione che risulterà vera solamente per gli elementi di quel dominio. 
 
Parliamo sempre di funzioni, ma perché serve che tutto sia funzione?  
Perché dobbiamo riportare il concetto delle ASM alle macchine a stato, composte da uno 
stato più la transizione (la freccia). 
Nelle ASM lo stato piuttosto che essere una cosa non strutturata a cui posso definire solo 
nel nome diventa adesso uno stato che è una struttura algebrica, con nomi di funzioni e 
d om ini.  
Per il momento non abbiamo definito formalmente la transizione ma andando per intuizione 
ipotizziamo di fotografare il sistema al momento t0 e t1 ; potremo avere due casi, il primo che 
non sia successo niente e il secondo che sia successo qualcosa. 
Il concetto matematico che può cambiare è l’interpretazione della funzione, perché le 
funzioni non si possono creare o distruggere in quanto il vocabolario è fisso, quindi l’unica 
cosa che si può cambiare è l’interpretazione della funzione. 
Come abbiamo visto tutto è funzione, costanti variabili, domini, predicati. 
Quello che dovrò fare nelle regole di transizione è definire come cambiano le regole di 
interpretazione delle funzioni, questo mi darà il concetto di passo di computazio ne.  
 
Durante le transizioni potranno cambiare solamente le interpretazioni delle funzioni 
dinamiche. 
Le transizioni hanno come mattone di base, l’aggiornamento della funzione. 
 
Esempio di stato ASM – orologio: 
Il vocabolario è composto da 4 elementi 2 funzioni dinamiche e 2 funzioni statiche, il super 
universo è composto da elementi reali.