際際滷

際際滷Share a Scribd company logo

Modelli per la descrizione di processi concorrenti def

Simone Mazzotta
Simone Mazzotta

presentazione tesi di Laurea Triennale

1 of 12
MODELLI PER LA DESCRIZIONE DI PROCESSI CONCORRENTI RELATORE Prof. Ruggero LANOTTE Candidato Simone MAZZOTTA ANNO ACCADEMICO 2009-2010 UNIVERSIT DEGLI STUDI DELL'INSUBRIA Facolt di Scienze, Matematiche, Fisiche e Naturali Corso di laurea in Scienze e Tecnologie dell Informazione
MACCHINE A STATI GERARCHICI E una tupla (K 1 ,,K n ) di moduli, in cui ogni modulo K i ha i seguenti componenti: Un insieme di nodi N i ; Un insieme di superstati, o box B i ; Un sottoinsieme di nodi di ingresso I i N i ; Un sottoinsieme di nodi di uscita O i N i ; Una funzione di indicizzazione Y i :B i ->{i+1n} che mappa ogni box dell i-esimo modulo ad un indice pi湛 grande di i ; Un insieme di archi E i , che connettono nodi e box .
ESPANSIONE Ad ogni struttura gerarchica se ne pu嘆 associare una ordinaria espansa in modo ricorsivo, sostituendo ogni box con la struttura indicizzata da questultimo. Si noti che ogni stato della struttura espansa 竪 una stringa di lunghezza massima uguale alla profondit di annidamento e la dimensione dellespansione pu嘆 essere esponenziale in tale profondit, ovvero O(|K| nd (K) ).
MODEL CHECKING E uno strumento pratico per la rilevazione degli errori logici nelle prime fasi di progettazione dei sistemi complessi, risolvendo vari problemi quali : Raggiungibilit: verifica se vi 竪 un percorso dal top-level alla regione di destinazione, eseguita con lalgoritmo di ricerca depth-first, che effettua questa analisi con complessit in tempo lineare nella dimensione della struttura gerarchica ad ingresso singolo. Procedure DFS(u) f u 狼 T then print (il nodo 竪 raggiungibile); break // terminare lesecuzione dellintero algoritmo end if; visited := visited {u}; if u 狼 N then foreach (u,v) 狼 E do if v visited then DFS(v); end if; end do; else i:= Y(u); if in I visited then DFS(in I ); end if ; foreach ((u,v),w) 狼 E do if v 狼 visited and w visited then DFS(w); end if; end do; end if; end DFS. DFS(in 1 ); Print (il nodo non 竪 raggiungibile).
MODEL CHECKING rilevamento di un ciclo: verifica se un determinato stato pu嘆 essere raggiunto pi湛 volte, utilizzando una ricerca primaria ed una secondaria. Anchesso ha complessit in tempo lineare. Procedure DFS P (u) Push(u, Stack); visited P := visited P {u}; if u 狼 N then foreach (u,v) 狼 E do if v visited P then DFS P (v); end do; if u 狼 T and u visited s then DFS S (u); else i:= Y(u); if in i visited P then DFS P (in i ); foreach ((u,v),w) 狼 E do if v 狼 visited P and w visited P then DFS P (w); if v 狼 visited S then if w 狼 Stack then print (ciclo trovato); break end if; if w visited S then DFS S (w); end if; end do; end if; Pop(Stack); end DFS P . Procedure DFS S (u) Visited S := visited S {u}; if u 狼 N then foreach (u,v) 狼 E do if v 狼 Stack then print (ciclo trovato); break end if; if v visited S then DFS S (v ); end do; else i:= Y(u); foreach ((u,v),w) 狼 E do if v 狼 visited P then if w 狼 Stack then print (ciclo trovato); break end if; if w visited S then DFS S (w); end if; end do; end DFS S . DFS P (in 1 ); Print (ciclo non trovato).
MODEL CHECKING Vi sono poi altri problemi di decisione quali: il test di vuoto effettuato sull automa gerarchico, con complessit Pspace-complete; il problema delluniversalit, cio竪 quello di decidere se il complemento del linguaggio di automa gerarchico 竪 vuoto, con complessit Expspace-complete; si ha poi il problema di verificare se due linguaggi sono equivalenti, ovvero decidere se, dati due NHA M 1 e M 2 , se L(M 1 ) 竪 uguale al L(M 2 ), anchesso con complessit Expspace-complete; infine la verifica dellinclusione del linguaggio L(M 1 ) L(M 2 ), che ha complessit Pspace-complete.
AUTOMI GERARCHICI COMUNICANTI Una macchina gerarchica concorrenziale 竪 composta da un insieme di macchine che operano in modo concorrente e si sincronizzano periodicamente a diversi livelli di gerarchia utilizzando simboli di un alfabeto comune.
AUTOMI GERARCHICI COMUNICANTI gli operatori gerarchici e quelli concorrenti sono arbitrariamente annidati ed i componenti del prodotto possono sincronizzarsi luno con laltro a differenti livelli. Queste caratteristiche contribuiscono in modo significativo allaumento della complessit del model checking, incrementando la complessit, ad esempio, del problema della raggiungibilit: tale problema, per automi gerarchici e comunicanti, 竪 Expspace-complete e pu嘆 essere risolto in tempo O(k^(d^m)) per un CHA di profondit m, larghezza d > 1 e con ogni modulo gerarchico avente al massimo k nodi o box.
AUTOMI GERARCHICI COMUNICANTI Vi 竪 poi una sottoclasse di CHA, chiamati ben strutturati, in cui pi湛 automi gerarchici possono sincronizzarsi solo al top-level. Questa limitazione porta, per esempio, a risolvere il problema della raggiungibilit in tempo O(k n^d) dove k 竪 il numero degli operatori dellautoma M, ogni modulo in M ha al massimo n stati e d 竪 la loro dimensione. 裡 dellespansione di X 竪 disgiunto dall 裡 dellespansione di N
STATECHARTS I diagrammi Statecharts sono estensione del formalismo convenzionale di macchine a stati; sono diagrammi modulari, gerarchici e ben strutturati e gestiscono lortogonalit, la comunicazione ed il raffinamento degli stati, migliorando anche il loro impatto visivo. Componente OR Componente AND
DISTRIBUTORE DI LATTINE Un esempio di automa gerarchico 竪 raffigurato, tramite il formalismo Statecharts, nellimmagine a fianco,la quale rappresenta una macchina che gestisce la scelta e lerogazione di una bevanda selezionata dallutente. Vi 竪 poi un indicatore automatico che notifica il blocco di una certa bevanda. A questo automa si possono poi applicare alcuni algoritmi del model checking come quello di raggiungibilit e rilevamento di un ciclo.
FINE Grazie per lattenzione. Mazzotta Simone

More Related Content

Modelli per la descrizione di processi concorrenti def

  • 1. MODELLI PER LA DESCRIZIONE DI PROCESSI CONCORRENTI RELATORE Prof. Ruggero LANOTTE Candidato Simone MAZZOTTA ANNO ACCADEMICO 2009-2010 UNIVERSIT DEGLI STUDI DELL'INSUBRIA Facolt di Scienze, Matematiche, Fisiche e Naturali Corso di laurea in Scienze e Tecnologie dell Informazione
  • 2. MACCHINE A STATI GERARCHICI E una tupla (K 1 ,,K n ) di moduli, in cui ogni modulo K i ha i seguenti componenti: Un insieme di nodi N i ; Un insieme di superstati, o box B i ; Un sottoinsieme di nodi di ingresso I i N i ; Un sottoinsieme di nodi di uscita O i N i ; Una funzione di indicizzazione Y i :B i ->{i+1n} che mappa ogni box dell i-esimo modulo ad un indice pi湛 grande di i ; Un insieme di archi E i , che connettono nodi e box .
  • 3. ESPANSIONE Ad ogni struttura gerarchica se ne pu嘆 associare una ordinaria espansa in modo ricorsivo, sostituendo ogni box con la struttura indicizzata da questultimo. Si noti che ogni stato della struttura espansa 竪 una stringa di lunghezza massima uguale alla profondit di annidamento e la dimensione dellespansione pu嘆 essere esponenziale in tale profondit, ovvero O(|K| nd (K) ).
  • 4. MODEL CHECKING E uno strumento pratico per la rilevazione degli errori logici nelle prime fasi di progettazione dei sistemi complessi, risolvendo vari problemi quali : Raggiungibilit: verifica se vi 竪 un percorso dal top-level alla regione di destinazione, eseguita con lalgoritmo di ricerca depth-first, che effettua questa analisi con complessit in tempo lineare nella dimensione della struttura gerarchica ad ingresso singolo. Procedure DFS(u) f u 狼 T then print (il nodo 竪 raggiungibile); break // terminare lesecuzione dellintero algoritmo end if; visited := visited {u}; if u 狼 N then foreach (u,v) 狼 E do if v visited then DFS(v); end if; end do; else i:= Y(u); if in I visited then DFS(in I ); end if ; foreach ((u,v),w) 狼 E do if v 狼 visited and w visited then DFS(w); end if; end do; end if; end DFS. DFS(in 1 ); Print (il nodo non 竪 raggiungibile).
  • 5. MODEL CHECKING rilevamento di un ciclo: verifica se un determinato stato pu嘆 essere raggiunto pi湛 volte, utilizzando una ricerca primaria ed una secondaria. Anchesso ha complessit in tempo lineare. Procedure DFS P (u) Push(u, Stack); visited P := visited P {u}; if u 狼 N then foreach (u,v) 狼 E do if v visited P then DFS P (v); end do; if u 狼 T and u visited s then DFS S (u); else i:= Y(u); if in i visited P then DFS P (in i ); foreach ((u,v),w) 狼 E do if v 狼 visited P and w visited P then DFS P (w); if v 狼 visited S then if w 狼 Stack then print (ciclo trovato); break end if; if w visited S then DFS S (w); end if; end do; end if; Pop(Stack); end DFS P . Procedure DFS S (u) Visited S := visited S {u}; if u 狼 N then foreach (u,v) 狼 E do if v 狼 Stack then print (ciclo trovato); break end if; if v visited S then DFS S (v ); end do; else i:= Y(u); foreach ((u,v),w) 狼 E do if v 狼 visited P then if w 狼 Stack then print (ciclo trovato); break end if; if w visited S then DFS S (w); end if; end do; end DFS S . DFS P (in 1 ); Print (ciclo non trovato).
  • 6. MODEL CHECKING Vi sono poi altri problemi di decisione quali: il test di vuoto effettuato sull automa gerarchico, con complessit Pspace-complete; il problema delluniversalit, cio竪 quello di decidere se il complemento del linguaggio di automa gerarchico 竪 vuoto, con complessit Expspace-complete; si ha poi il problema di verificare se due linguaggi sono equivalenti, ovvero decidere se, dati due NHA M 1 e M 2 , se L(M 1 ) 竪 uguale al L(M 2 ), anchesso con complessit Expspace-complete; infine la verifica dellinclusione del linguaggio L(M 1 ) L(M 2 ), che ha complessit Pspace-complete.
  • 7. AUTOMI GERARCHICI COMUNICANTI Una macchina gerarchica concorrenziale 竪 composta da un insieme di macchine che operano in modo concorrente e si sincronizzano periodicamente a diversi livelli di gerarchia utilizzando simboli di un alfabeto comune.
  • 8. AUTOMI GERARCHICI COMUNICANTI gli operatori gerarchici e quelli concorrenti sono arbitrariamente annidati ed i componenti del prodotto possono sincronizzarsi luno con laltro a differenti livelli. Queste caratteristiche contribuiscono in modo significativo allaumento della complessit del model checking, incrementando la complessit, ad esempio, del problema della raggiungibilit: tale problema, per automi gerarchici e comunicanti, 竪 Expspace-complete e pu嘆 essere risolto in tempo O(k^(d^m)) per un CHA di profondit m, larghezza d > 1 e con ogni modulo gerarchico avente al massimo k nodi o box.
  • 9. AUTOMI GERARCHICI COMUNICANTI Vi 竪 poi una sottoclasse di CHA, chiamati ben strutturati, in cui pi湛 automi gerarchici possono sincronizzarsi solo al top-level. Questa limitazione porta, per esempio, a risolvere il problema della raggiungibilit in tempo O(k n^d) dove k 竪 il numero degli operatori dellautoma M, ogni modulo in M ha al massimo n stati e d 竪 la loro dimensione. 裡 dellespansione di X 竪 disgiunto dall 裡 dellespansione di N
  • 10. STATECHARTS I diagrammi Statecharts sono estensione del formalismo convenzionale di macchine a stati; sono diagrammi modulari, gerarchici e ben strutturati e gestiscono lortogonalit, la comunicazione ed il raffinamento degli stati, migliorando anche il loro impatto visivo. Componente OR Componente AND
  • 11. DISTRIBUTORE DI LATTINE Un esempio di automa gerarchico 竪 raffigurato, tramite il formalismo Statecharts, nellimmagine a fianco,la quale rappresenta una macchina che gestisce la scelta e lerogazione di una bevanda selezionata dallutente. Vi 竪 poi un indicatore automatico che notifica il blocco di una certa bevanda. A questo automa si possono poi applicare alcuni algoritmi del model checking come quello di raggiungibilit e rilevamento di un ciclo.
  • 12. FINE Grazie per lattenzione. Mazzotta Simone