4/26/20151 Metodi formali nello sviluppo software a.a.2013/2014 Prof.Anna Labella.
-
Upload
croccifixio-bossi -
Category
Documents
-
view
216 -
download
2
Transcript of 4/26/20151 Metodi formali nello sviluppo software a.a.2013/2014 Prof.Anna Labella.
04/11/23 1
Metodi formali nello sviluppo software
a.a.2013/2014
Prof.Anna Labella
04/11/23 2
Ripartiamo dagli automi
Stati e transizioni etichettate Gli automi sono caratterizzati dal
linguaggio che “accettano”
04/11/23 3
L’algebra dei linguaggi
• Algebra di Boole
• Monoide rispetto alla concatenazione
• Iterazione
04/11/23 4
L’algebra dei linguaggi
04/11/23 5
L’algebra dei linguaggi
04/11/23 6
04/11/23 7
Equivalenza di automi
Accettare lo “stesso” linguaggio– Il linguaggio di uno può ridursi al linguaggio
dell’altro usando le proprietà algebriche di P(A*)
04/11/23 8
Sistemi reattivi
Protocolli di comunicazione Sistemi operativi Dispositivi di comando e controllo
04/11/23 9
Sincronia ed asincronia
Comunicazione
Osservabilità
Non determinismo
04/11/23 10
Sistemi di transizione
Sistemi stato-transizione: una macchina astratta per la computazione
Definizione Etichettatura Relazione con gli automi
04/11/23 11
Sistema di transizione (etichettato) TS=(,S, , S0), dove è un alfabeto finito non vuoto– S è un insieme (finito) non vuoto di stati S S è la relazione di trsansizione,
– S0 S è l‘insieme degli stati inziali
simile ad un automa finito nondeterministico,
con molti stati iniziali ma senza stati finali
simile ad un modello di Kripke etichettato: un sistema di mondi possibili con una nozione di accessibilità
04/11/23 12
Un sistema di transizione genera parole (finite o infinite) w0w1w2... sse ci sono stati s0s1s2s3...
t.c. s0 S0 e (si,wi,si+1)
Uno stato è identificato con le possibilità che mette a disposizione
Problemi con la terminazione ed il deadlock
04/11/23 13
Esempio: un registratore
1. ={up, dn}
2. S={off, tape, memory, play}
3. ={(off,dn,tape), (tape,up,off), (tape,dn,memory), (memory,up,off), (memory,dn,play), (play,dn,tape), (play,up,off)}
4. S0={off}
off
memorytape play
dn
dn dn
dn
up up up
04/11/23 14
Sistemi di Transizione paralleli Parallel transition system T=(T1,…,Tn)
– each Ti is a transition system
– SiSj=
interleaving semantics– on its private alphabet, each Ti can make an
independent move– synchronization is via common events
example: power switch and camcorder mode
04/11/23 15
Example
T=(switch, camera) {pwr_fail, pwr_res} are private to camera synchronization alphabet {up,dn} how big is the state space?
but_hi
but_lo
dn up
off
on
dn,pwr_res
up,pwr_fail
memorytape
play
dn
dn dn
onswitch camera
dn
04/11/23 16
The global transition system T associated
with a parallel transition system (T1,…,Tn) is defined as T=(, S, , S0), where
= i
– S= S1 … Sn
– S0 = S1,0 … Sn,0, and
– ((s1,…,sn),a,(s1‘,…,sn‘)) iff for all Ti
• if ai, then ((s i),a,(s i‘))i, and
• if ai, then s i=s i‘.
04/11/23 17
Finite State Automata
Coffee machine A1:
Coffee machine A2:
Are the two machines ”the same”?
1kr
1kr
tea
coffee
1kr
1kr
tea
coffee
1kr