19
A
A
Per contattare l’autore:[email protected]/in/lucianomanelli
Luciano Manelli
DASM e CoreASMper l’analisi di sistemi complessi
Copyright © MMXVIAracne editrice int.le S.r.l.
via Quarto Negroni, Ariccia (RM)
()
----
I diritti di traduzione, di memorizzazione elettronica,di riproduzione e di adattamento anche parziale,
con qualsiasi mezzo, sono riservati per tutti i Paesi.
Non sono assolutamente consentite le fotocopiesenza il permesso scritto dell’Editore.
I edizione: maggio
5
A mia figlia Sara, che è la mia fonte di energia A mia moglie Stefania, che ha supportato questa mia passione Ai miei genitori Anna e Piero, che credono sempre in un mondo migliore
6
7
“Essentially, all models are wrong,
but some are useful.”
George E.P. Box, Norman R. Draper, “Empirical Model-Building and Response Sur-
faces”, Wiley, 1987.
6
8
9
9
Prefazione
Questo libro nasce dall’esigenza di presentare e studiare nuovi e per-formanti metodi formali per l’analisi e la descrizione delle specifiche operazionali, la modellazione, il controllo e la verifica, la specifica e la progettazione dei moderni sistemi informativi, altamente dinamici e complessi, che contengono attività parallele e concorrenti, affinché pos-sano affiancarsi, quale valido strumento di supporto, ai progettisti e, quale alternativa standard, valida, innovativa e vincente, alle attuali me-todologie usate nel campo dell’ingegneria del software. Il testo prende spunto dalla tesi di dottorato dell’autore e affronta lo sviluppo delle Di-stributed Abstract State Machine con l’ausilio di CoreASM per lo stu-dio e la verifica di sistemi complessi. Abbinamento necessario in un momento in cui la teoria necessita di applicazione pratica, affinché possa essere valorizzata in ambito lavorativo-professionale e di ricerca scientifica. Infatti la metodologia ASM permette di studiare stati e tran-sizioni in ambienti complessi in maniera flessibile ed approfondita, of-frendo, grazie alla possibilità di descrivere un modello in forma grafica, una rappresentazione espressiva, flessibile, completa e raffinabile al li-vello di approfondimento richiesto. Viene affrontato, a completamento del testo e come tangibile rappresentazione delle analisi sviluppate, un caso studio legato ad una particolare tipologia di servizi middleware per il Grid Computing: dalla descrizione informale, alla specifica dei requi-siti, alla loro modellazione, alla progettazione degli agenti software coinvolti, alla generazione del codice ASM con regole e stati, alla veri-fica degli scenari.
Ho sempre pensato e sostenuto che i sogni debbano essere conqui-stati e spero che la lettura e lo studio del presente libro vada oltre al suo scopo strettamente didattico aprendo prospettive su una realtà in conti-nua evoluzione.
8
10
11
11
Indice
Prefazione.............................................................................................. 9
Indice ................................................................................................... 11
Introduzione ........................................................................................ 15
Ringraziamenti .................................................................................... 17
Capitolo I - I metodi formali – Abstract State Machine ...................... 19 1.1 Introduzione ............................................................................. 19
1.2 Specifiche e metodi formali nello sviluppo del software ......... 20
1.3 Metodi Formali ........................................................................ 21
1.3.1 Le reti di Petri ...................................................................... 21
1.3.2 Le Abstract State Machine ................................................... 22
1.3.3 Abstract State Machine vs Petri Nets ................................... 24
1.4 Metodi formali nell’Industria ................................................... 24
1.5 Il metodo ASM......................................................................... 28 1.6 Dalle FSM alle ASM................................................................ 29
1.7 Definizione di ASM ................................................................. 32
1.8 Esecuzione delle ASM ............................................................. 35
1.9 Composizione di ASM ............................................................. 36 1.10 Ground Model .......................................................................... 37
1.11 Synchronous e Asynchronous Multi-Agent ASMs .................. 38
1.12 Definizione di DASM - Asynchronous Multi-Agent ASM ..... 39
1.13 Analisi delle proprietà di Sistema con DASM ......................... 40 1.13.1 Raggiungibilità - Reachability ............................................. 42
1.13.2 Reversibilità - Reversibility .................................................. 43
10
12
1.13.3 Vitalità - Liveness ................................................................ 44
1.13.4 Completezza - Completeness ............................................... 45 1.13.5 Deadlock .............................................................................. 46
Capitolo II - CoreASM ....................................................................... 49
2.1 Introduzione ............................................................................. 49
2.2 Progettazione Concettuale di coreASM .................................. 49
2.3 Installazione di Eclipse ............................................................ 51
2.4 Installazione Plugin di CoreASM per Eclipse ......................... 53
2.5 Creare un nuovo progetto ........................................................ 56
2.6 Creare una nuova specifica CoreASM .................................... 58 2.7 Lavorare con CoreASM........................................................... 60
2.8 Specifiche CoreASM ............................................................... 62
2.9 Strutture CoreASM .................................................................. 63
2.10 L’Universo degli Agenti .......................................................... 65 2.11 Sviluppo del codice ................................................................. 66
Capitolo III - Servizi, Middleware e Grid Computing ........................ 67
3.1 Introduzione ............................................................................. 67
3.2 I servizi .................................................................................... 68
3.3 I Sistemi Distribuiti ................................................................. 70 3.4 Cluster ...................................................................................... 71
3.5 Grid Computing ....................................................................... 73
3.5.1 Tecnologia Grid ................................................................... 76
3.5.2 Servizi Grid .......................................................................... 78 3.5.3 Modellizzazione dei Servizi Grid ......................................... 82
3.6 Cloud Computing .................................................................... 83
3.7 Conclusioni .............................................................................. 87
12 Indice
13
Capitolo IV - DASM e CoreASM per i Servizi Grid .......................... 89
4.1 Introduzione ............................................................................. 89
4.2 I Servizi di Execution Management ......................................... 90
4.3 Execution Management vs DASM .......................................... 91
4.4 Esperienze di modellazione formale per Grid .......................... 92
4.5 Descrizione Informale e Specifica dei Requisiti ...................... 95
4.6 Specifiche Funzionali ............................................................. 103
4.7 Agenti Software per modellare i Servizi di Grid Computing 109
4.8 Modello Dispatcher ................................................................ 111
4.8.1 Stati ASM del Dispatcher ................................................... 111
4.8.2 Specifica del Dispatcher e codice CoreASM ...................... 113
4.8.3 Rules ASM del Dispatcher .................................................. 116
4.9 Modello Resources Pool ........................................................ 117
4.9.1 Modello ResourceLocalQueue ........................................... 118 4.9.2 Stati ASM del ResourceLocalQueue................................... 118
4.9.3 Specifica del ResourceLocalQueue e codice CoreASM ..... 119
4.9.4 Rules ASM del ResourceLocalQueue ................................. 121
4.9.5 Modello ResourceExecutor ................................................ 122
4.9.6 Stati ASM del ResourceExecutor ........................................ 123 4.9.7 Specifica del ResourceExecutor e codice CoreASM .......... 124
4.9.8 Rules ASM del ResourceExecutor ...................................... 127
4.10 Modello JobManager ............................................................. 128
4.10.1 Stati ASM del JobManager................................................. 129 4.10.2 Specifica del JobManager e codice CoreASM ................... 131
4.10.3 Rules ASM del JobManager ............................................... 136
4.11 Il Ground Model..................................................................... 142
12
1.13.3 Vitalità - Liveness ................................................................ 44
1.13.4 Completezza - Completeness ............................................... 45 1.13.5 Deadlock .............................................................................. 46
Capitolo II - CoreASM ....................................................................... 49
2.1 Introduzione ............................................................................. 49
2.2 Progettazione Concettuale di coreASM .................................. 49
2.3 Installazione di Eclipse ............................................................ 51
2.4 Installazione Plugin di CoreASM per Eclipse ......................... 53
2.5 Creare un nuovo progetto ........................................................ 56
2.6 Creare una nuova specifica CoreASM .................................... 58 2.7 Lavorare con CoreASM........................................................... 60
2.8 Specifiche CoreASM ............................................................... 62
2.9 Strutture CoreASM .................................................................. 63
2.10 L’Universo degli Agenti .......................................................... 65 2.11 Sviluppo del codice ................................................................. 66
Capitolo III - Servizi, Middleware e Grid Computing ........................ 67
3.1 Introduzione ............................................................................. 67
3.2 I servizi .................................................................................... 68
3.3 I Sistemi Distribuiti ................................................................. 70 3.4 Cluster ...................................................................................... 71
3.5 Grid Computing ....................................................................... 73
3.5.1 Tecnologia Grid ................................................................... 76
3.5.2 Servizi Grid .......................................................................... 78 3.5.3 Modellizzazione dei Servizi Grid ......................................... 82
3.6 Cloud Computing .................................................................... 83
3.7 Conclusioni .............................................................................. 87
13Indice
14
4.12 Implementazione del Ground Model ..................................... 144
4.13 Analisi degli scenari sviluppati in CoreASM ........................ 145 4.13.1 Scenario 1 .......................................................................... 146
4.13.2 Scenario 2 .......................................................................... 146
4.13.3 Scenario 3 .......................................................................... 147
4.13.4 Scenario 4 .......................................................................... 148
4.13.5 Scenario 5 .......................................................................... 148
4.14 Locations del Modello ASM ................................................. 150
4.15 Analisi delle proprietà di Sistema con DASM ...................... 154
4.15.1 Raggiungibilità - Reachability ........................................... 154
4.15.2 Reversibilità - Reversability ............................................... 155
4.15.3 Vitalità - Liveness .............................................................. 156
4.15.4 Completezza - Completeness ............................................. 156
4.15.5 Deadlock ............................................................................ 156 4.15.6 Proprietà e progettazione del JobManager: osservazioni 156
4.16 Interoperabilità tra middleware: formalismi e confronti ....... 157
4.16.1 GRAM – Globus ................................................................. 158
4.16.2 WMS – GLite ...................................................................... 162
4.16.3 BES – OGF ........................................................................ 165
4.16.4 Interoperabilità: osservazioni ............................................ 168
Indice delle Figure ............................................................................ 169
Indice delle Tabelle .......................................................................... 171
Bibliografia ....................................................................................... 173
14 Indice
15
15
Introduzione
Il seguente testo propone lo studio delle Abstract State Machine, nella loro accezione distribuita con l’ausilio di agenti software, per l’analisi di sistemi software complessi ed altamente dinamici. Lo studio teorico è affiancato dallo strumento CoreASM, plugin di Eclipse, utile per la progettazione e la verifica delle specifiche formali. Il testo si ri-volge sia al pubblico degli studenti, che a quello dei professionisti, quale evoluzione ed alternativa alla metodologia classica, al fine di ap-prendere e applicare i metodi formali, in ottica di lifelong learning, aprendo gli orizzonti ad un mondo in continua e pressante evoluzione. L’analisi teorica è integrata e completata da un dettagliato caso studio di attuale ricerca scientifica, ovvero l’analisi dei servizi di middleware di una Grid. La modellizzazione, la visualizzazione, la specifica, il con-trollo e la verifica del caso studio sono supportate dal CoreASM, con-figurabile come plugin di Eclipse e strumento versatile ed indispensa-bile per l’applicazione dei concetti teorici.
Il primo capitolo del presente testo introduce ed analizza i metodi formali, standard in vari ambiti dell’ingegneria del software per la ge-stione delle specifiche, approfondendo le Distributed Abstract State Machine.
Il secondo capitolo illustra caratteristiche e componenti del Co-reASM, introducendone la programmazione in ambiente Eclipse.
Il terzo capitolo è dedicato al caso studio, in quanto analizza le ca-ratteristiche funzionali dei servizi di middleware delle Grid, partendo dai servizi web e dai sistemi distribuiti e giungendo ad un approfondi-mento sui servizi di Execution Management delle Grid atti alla esecu-zione dei job sottomessi.
L’ultimo capitolo è dedicato alla modellazione del servizio preso in esame nel caso studio e all’analisi del modello DASM ipotizzato: dalla individuazione degli stati, alla creazione delle regole, alla definizione degli agenti software, fino alla generazione del Ground Model. La dis-sertazione è corredata da uno studio degli scenari proposti in ambiente CoreASM e dall’analisi delle proprietà di sistema.
14
4.12 Implementazione del Ground Model ..................................... 144
4.13 Analisi degli scenari sviluppati in CoreASM ........................ 145 4.13.1 Scenario 1 .......................................................................... 146
4.13.2 Scenario 2 .......................................................................... 146
4.13.3 Scenario 3 .......................................................................... 147
4.13.4 Scenario 4 .......................................................................... 148
4.13.5 Scenario 5 .......................................................................... 148
4.14 Locations del Modello ASM ................................................. 150
4.15 Analisi delle proprietà di Sistema con DASM ...................... 154
4.15.1 Raggiungibilità - Reachability ........................................... 154
4.15.2 Reversibilità - Reversability ............................................... 155
4.15.3 Vitalità - Liveness .............................................................. 156
4.15.4 Completezza - Completeness ............................................. 156
4.15.5 Deadlock ............................................................................ 156 4.15.6 Proprietà e progettazione del JobManager: osservazioni 156
4.16 Interoperabilità tra middleware: formalismi e confronti ....... 157
4.16.1 GRAM – Globus ................................................................. 158
4.16.2 WMS – GLite ...................................................................... 162
4.16.3 BES – OGF ........................................................................ 165
4.16.4 Interoperabilità: osservazioni ............................................ 168
Indice delle Figure ............................................................................ 169
Indice delle Tabelle .......................................................................... 171
Bibliografia ....................................................................................... 173
16
17
17
Ringraziamenti
Ringrazio i mentori che mi hanno seguito nella mia esperienza di Dottorato. Il Professor Sebastiano Pizzutilo, mio tutor e guida che mi ha accolto e formato nell’ambito dei sistemi distribuiti e il Professor Alessandro Bianchi che mi ha assistito e seguito assiduamente nella ste-sura dei miei lavori fornendomi le basi metodologiche sulle ASM.
16
18
19
19
Capitolo I
I metodi formali – Abstract State Machine
1.1 Introduzione
In questo capitolo verranno introdotti i concetti del formalismo delle Abstract State Machine e verranno forniti gli strumenti per applicare il metodo di sviluppo ASM-based. Questo al fine sia di stimolare l’analisi critica dei sistemi, sia di ampliare le capacità di astrazione e formaliz-zazione di un problema, sia, in ultimo, di applicare le conoscenze ac-quisite nell’analisi di fenomeni legati alla realtà. Infatti, i sistemi infor-mativi ed industriali complessi non solo presentano requisiti multipli e difficili da analizzare, ma presentano l’emergente caratteristica di coo-perazione tra diversi componenti al fine di fornire servizi sempre più raffinati. I sistemi complessi si compongono quindi di moduli indipen-denti, spesso distribuiti, ciascuno capace di offrire servizi computazio-nali in cooperazione con gli altri. Questa crescente complessità com-porta la necessità comprendere e modellare in maniera opportuna il comportamento dei sistemi non solo in ottica computazionale, ma anche in ottica di comunicazione tra le componenti. I metodi formali vengono incontro a tale esigenza consentendo di creare una specifica completa, uniforme e non ambigua rispetto a quella prodotta tramite metodi infor-mali. Inoltre, tale specifica matematica può essere dimostrata corretta ed eseguita ad alto livello tramite linguaggi di specifica eseguibili e porta alla notevole riduzione degli errori nello sviluppo software di si-stemi critici.
Verranno di seguito introdotti i linguaggi formali con un relativo approfondimento sulle ASM e sulle Distributed ASM, chiudendo con un approfondimento sull’uso dei metodi formali nell’industria.
18
