MINISTERO DELL'ISTRUZIONE, DELL'UNIVERSITÀ E DELLA …horvath/firb2010/final/all.pdfMINISTERO...

MINISTERO DELL'ISTRUZIONE, DELL'UNIVERSITÀ E DELLA RICERCADirezione Generale per il Coordinamento e lo Sviluppo della ricerca

PROGETTO DI RICERCA - MODELLO ABANDO FIRB - PROGRAMMA "FUTURO IN RICERCA"

Anno 2010 - Protocollo: RBFR10ZMBO

LINEA D'INTERVENTO 3

1 - Titolo del Progetto di Ricerca

ItalianoValutazione quantitativa di sistemi concorrenti e temporizzati: metodi per applicazioni

IngleseQuantitative Evaluation of Timed Concurrent Systems: Methods for Applications

2 - Durata del Progetto di Ricerca36 mesi

3 - Coordinatore scientifico della ricerca (Principal Investigator)HORVATH Andras HRVNRS74D30Z134W

(cognome) (nome) (codice fiscale)

Ricercatore confermato 30/04/1974

(qualifica) (data di nascita)

Università degli Studi diTORINO

Dipartimento di INFORMATICA

(Istituzione diappartenenza)

(Dipartimento/Istituto/Divisione/Settore)

011 6706803 011 751603 [email protected]

(telefono) (fax) (e-mail)

4 - Abstract del Progetto di RicercaItaliano

Il progetto e la manutenzione di sistemi distribuiti operanti in ambienti e condizioni impredicibili richiedono accurata valutazione di modelli probabilistici nel tempo.Questa esigenza ha ispirato una vasta letteratura sui linguaggi di modellazione formale in combinazione con tecniche di soluzione analitica e simulativa. Inparticolare, negli ultimi anni, una parte significativa di questa letteratura si è concentrata sulla verifica automatica mediante tecniche di model checkingprobabilistiche.

Molte delle attività di cui sopra non sono ancora state adottate nella pratica industriale e cio' è principalmente dovuto ad alcune specifiche lacune. La maggior partedi tali ricerche si è basata su modelli riconducibili a catene di Markov. Cio' rappresenta una limitazione espressiva del modello e diventa un ostacolo alla suaapplicazione nei diversi settori quali i sistemi in tempo reale, i protocolli di comunicazione e, più in generale, i sistemi con memoria nel tempo. L'esplosione dellospazio degli stati inoltre limita l'applicazione di tali modelli nella pratica quando cresce la complessità dei modelli in caso di scenari piu' realistici. In misurasignificativa, l'applicazione è limitata anche dalla mancanza di tecniche di modellazione e prassi consolidate in grado di catturare scenari reali senza violare leipotesi che rendono possibile la valutazione.

Il progetto propone di sviluppare ricerca di base per ovviare alle carenze di cui sopra. Le linee di ricerca sono state individuate sulla base dei campi applicativi chesaranno utilizzati per testare e valutare gli algoritmi e le tecniche sviluppate nel corso del progetto. I campi di applicazione considerati sono: il cloud computing, lereti di sensori, il monitoraggio e la predizione on-line di infrastrutture, ed il processo di sviluppo di real-time software. Le problematiche ingegneristiche affrontate intali ambiti sono cruciali in numerose questioni di importanza strategica, come ad esempio, garantire la sicurezza del territorio, la progettazione e la gestione delsistema sanitario di assistenza nazionale, il risparmio energetico, i sistemi critici ed i processi industriali regolati da norme di certificazione di processo e di prodotto(come quelli relativi l'industria automobilistica, aerea, ferroviaria e dei trasporti in genere, l'ingegneria del software di sistemi critici, ecc.)

Inoltre, quale ulteriore innovativo campo di applicazione delle tecniche di valutazione quantitative proposte identifichiamo l'organizzazione aziendale, con l'obiettivodi fornire una rappresentazione in grado di catturare le possibili correlazioni tra il modello organizzativo, il focus strategico e le performance dell'azienda.

Le linee di ricerca proposte del progetto sono descritte brevemente di seguito.

1

(1) Analisi di modelli non-Markoviani attraverso Markovianizzazione.Spesso approssimazioni Markoviane di fenomeni non-Markoviani possono essere specificate ed utilizzate per effettuare analisi sufficientemente accurate. Inparticolare affronteremo due aspetti cruciali di questo approccio.(i) La specifica di modelli Markoviani approssimati.(ii) Tecniche innovative per la rappresentazione compatta e la soluzione di tali modelli di approssimazione, dal momento che questi potrebbero essere soggetti adesplosione dello spazio degli stati.

(2) Analisi approssimata di modelli non-MarkovianiLa soluzione esatta di modelli non-Markoviani relativi a sistemi reali è, nel caso piu' generale, spesso impossibile da ottenere, ma ci sono casi in cui approssimazioniaccurate possono essere ottenute. Tre temi saranno affrontati in tal senso.(i) Se un modello è composto da un gran numero di sottomodelli che interagiscono, le cosiddette tecniche asintotiche (quali il piu' diffuso e ben noto approccio meanfield) possono essere utilizzate per l'analisi. Le tecniche asintotiche sono note e definite per modelli Markoviani, il nostro obiettivo è di estenderle a modelli nonMarkoviani.(ii) Se un modello è composto da sottomodelli che interagiscono sporadicamente, tecniche a punto fisso di iterazione potrebbero essere applicate nella soluzione. Talitecniche sono implementate e vengono solitamente applicate all'analisi a regime di modelli Markoviani. Il nostro obiettivo è fornire estensioni di tali tecnicheall'analisi transitoria ed a modelli non-Markoviani.(iii) La modellazione dei meccanismi di prelazione è di particolare interesse nello sviluppo di software real time. La presenza di tali meccanismi rende in generaleimpossibile l'analisi esatta di modelli non-Markoviani anche in caso di spazio degli stati contenuto. Noi puntiamo a sviluppare tecniche approssimate basate su classidi stato stocastiche per l'analisi dei sistemi con scheduling a prelazione.

(3) Model checking.La gran parte dei metodi e dei tools di model checking sin qui sviluppati sono applicabili esclusivamente a modelli Markoviani e permettono di verificare solo unristretto insieme di proprietà. Al fine di estendere l'applicabilità del model checking probabilistico prenderemo in considerazione i seguenti punti.(i) Model checking di modelli non Markoviani. Tre approcci saranno sviluppati per la verifica automatica di modelli non Markoviani: model checking basati suclassi di stato stocastiche, model checking attraverso astrazioni, procedure di model checking statistiche.(ii) Unificazione di logiche temporali e algoritmi associati. Logiche diverse sono in grado di esprimere diverso tipo di proprietà e richiedono algoritmi specifici. Ilnostro obiettivo è definire una logica unitaria e di svilupparne l'algoritmo di model checking associato.(iii) Model checking composizionale da specifiche incomplete. Spesso un sistema opera in un ambiente le cui condizioni non sono completamente specificate. Ilnostro obiettivo è di sviluppare specifiche di composizione e tecniche di analisi che consentano di verificare i modelli a partire solo dalle ipotesi relative l'ambienteesterno.

Quattro unità di ricerca parteciperanno al progetto, tutte con competenze specifiche su diversi degli argomenti considerati e con grande esperienza nello sviluppo ditool. I membri dei diversi gruppi hanno già collaborato e pubblicato numerosi articoli sulle tematiche di interesse.

Inglese

Design and maintenance of distributed systems operating in unpredictable environments require quantitative evaluation of probabilistic timed models. This need gavebirth to a wide literature devoted to formal modeling languages combined with analytical and simulative solution techniques. In particular, in recent years, asignificant portion of this literature has been focused on automatic verification through probabilistic model checking.

Several of the above efforts have not yet been transformed into industrial practice and this is mainly due to the following shortcomings. Most of such researchesconsider models whose underlying stochastic processes are Markov chains. This marks a limit in the expressive power of the model, preventing application in severaldomains such as real time systems, communication protocols, and, more generally, systems that accumulate memory over time. The state space explosion also limitspractical applicability when models complexity grows in correspondence of more real scenarios. To a significant extent, application is also limited by the lack ofestablished modeling patterns and practices able to capture real scenarios without breaking the assumptions that make the evaluation viable.

The project proposes fundamental research to alleviate the above shortcomings.

The research directions we propose have been identified by examining application areas that will be used to evaluate algorithms and tools developed throughout theproject. The application areas are: cloud computing, wireless sensor networks, online monitoring and prediction infrastructures, and the development process of realtime software. The engineering problems of these areas are crucial in several issues of strategic importance, such as, guaranteeing home-land security, design andmanagement of nation wide health care systems, energy conservation, safety critical systems and industrial processes ruled by process and product certificationstandards (like automotive, railways signaling, airborne and space engineering software).

Moreover, as a novel application area to formal quantitative evaluation we identify business organizations, where we aim at providing a representation able tocapture possible correlations among the organizational model, the strategic focus and the performance of a company.

The proposed research directions are briefly described in the following.

(1) Analysis of non-Markovian models by Markovianization.It is often the case that Markovian approximations of non-Markovian phenomena can be built and used to carry out sufficiently accurate approximate analyses. Wewill address two crucial aspects of this approach.(i) The construction of approximating Markovian models.(ii) Innovative techniques for the compact representation and the solution of such approximating models, since they can be subject to state space explosion.

(2) Approximate analysis of non-Markovian models.Exact solution of general non-Markovian models of real systems is most often unfeasible but there are cases in which accurate approximations can be obtained. Threesubjects will be addressed.(i) If a model is composed of a large number of interacting submodels, the so-called asymptotic techniques (among the others the well-known mean field approach)can be used for the analysis. Asymptotic techniques are available for Markovian models and we aim to extend them to non-Markovian models.(ii) If a model is composed of loosely interacting submodels, then fixed point iteration schemes can be applied for the solution. Such techniques are available and havebeen applied for the steady state analysis of Markovian models. We aim to provide extensions to transient analysis and to non-Markovian models.(iii) Modeling of preemption mechanisms is of particular interest in the development of real time software. The presence of such mechanisms makes the exact analysisof general non-Markovian models unfeasible even for small state spaces. We aim at developing approximating techniques based on stochastic state classes for theanalysis of systems with preemptive scheduling.

(3) Model checking.Most of probabilistic model checking methods and tools are applicable only to Markovian models and allow for verifying only a limited set of properties. In order toincrease the applicability of probabilistic model checking we consider the following issues.(i) Model checking of non-Markovian models. Three approaches will be developed for the automatic verification of non-Markovian models: model checking based onstochastic state classes, model checking by abstractions, statistical model checking procedures.(ii) Unification of temporal logics and associated algorithms. Different logics are capable of expressing different kind of properties and require different algorithms.Our aim is to define a unified logic and develop an associated model checking algorithm.(iii) Model checking compositional incomplete specifications. It is often the case that a system operates in a not completely specified environment. We aim to developcompositional specification and analysis techniques which verify models having in hand only assumptions for what concerns the behavior of the environment.

2

Four research units participate in the project, all of them with specific expertise on many of the considered issues and with long term experience in tool development.Members of different groups have already cooperated and published numerous papers on the involved subjects.

5 - Parole chiaveItaliano1. Valutazione delle prestazioni2. Sistemi distribuiti su larga scala con vincoli di QoS3. Modellazione di sistemi temporizzati concorrenti4. Processi non-Markoviani5. Model checking probabilistico

Inglese1. Performance evaluation2. QoS constrained large-scale distributed systems3. Modeling timed concurrent systems4. Non-Markovian processes5. Probabilistic model checking

6 - Settori di ricerca ERC (European Research Council) interessati dal Progetto di Ricerca

PE Physical Sciences and EngineeringPE6 Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems PE6_10 Simulation and modelling tools

PE7 Systems and communication engineering: electronic, communication, optical and systems engineering PE7_3 Simulation engineering and modelling

PE6 Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems PE6_1 Computer architecture, parallel, distributed and pervasive computing

7 - Curriculum scientifico del Coordinatore della RicercaItaliano

1 Studi e posizioni di lavoro

A. Horvath ha ottenuto, presso la Technical University of Budapest, Ungheria, la laurea in Ingegneria Informatica in 1997 e il titolo di Dottore di Ricerca inInformatica in 2004. Dal 1 ottobre 1999 al 30 settembre 2001 è stato assegnista di ricerca presso il Dip. di Informatica dell'Università degli Studi di Torino. Dalaprile 2003 è ricercatore presso il Dip. di Informatica dell'Università degli Studi di Torino.

2 Attività di ricerca

La sua ricerca si concentra sulla valutazione delle prestazioni e verifica della correttezza di sistemi ad eventi discreti. Ha pubblicato 14 articoli in rivisteinternazionali e 36 articoli in atti di convegni internazionali con revisione. Ai suoi lavori sono state fatte circa 300 citazioni.

2.1 Risultati scientifici

Segue l'elenco di risultati scientifici rilevanti per il progetto.

Approssimazione di comportamenti non-Markoviani con modelli Markoviani: Per via della loro trattabilità analitica e numerica, i modelli Markoviani, in particolarele catene di Markov, sono ampiamente utilizzati per la valutazione delle prestazioni di sistemi. Essi però pongono anche una limitazione ai comportamenti chepossono essere modellati con precisione. Tuttavia, è possibile approssimare comportamenti non-Markoviani con modelli Markoviani. In questo contesto ha sviluppatoalgoritmi per la costruzione di modelli Markoviani che approssimano fenomeni reali [1,2,3,4,5,6,7,9,15,17,19,26,31,35,36,37].

Soluzione per catene di Markov strutturate: Le approssimazioni Markoviane di comportamenti non-Markoviani danno luogo a catene di Markov strutturate. Hasviluppato tecniche che, sfruttando tale struttura, permettono di analizzare modelli di grandi dimensioni [21,27,29,30,33,34,40].

Modelli non-Markoviani: Un modello non-Markoviano è un modello in cui lo stato è descritto da uno o più componenti discreti e da uno o più componenti continui. Imodelli non-Markoviani permettono di considerare durate non-esponenziali e di modellare quantità continue (per esempio, la temperatura di un componente).Horvath ha contribuito sia nella definizione di formalismi per la descrizione di modelli non-Markoviani sia per quanto riguarda le tecniche di soluzione[8,10,11,12,14,15,18,20,22,23,24,25,28,32,41].

2.2 Partecipazione a comitati e ad organizzazione di eventi

Program co-chair:3rd European Performance Engineering Workshop (EPEW'06),Budapest, Hungary, June 2006;7th Int. Workshop on Performability Modeling of Computer andCommunication Systems) (PMCCS), Torino, Italy, Sep. 2005;TiSto'09, Int. Workshop on Timing and Stochasticity in Petri netsand other models of concurrency, Paris, France, June 2009;SMC'09, 4th Int. Workshop on Tools for solving Structured MarkovChains, Pisa, Italy, 2009.

3

Membro del comitato di programma:EPEW'06,'07,'08,'09 (European Performance Engineering Workshop);QEST'07,'09 (Int. Conf. on the Quantitative Evaluation of Systems);AMSTA'09,'10 (Int. Conf. on Analytical and Stochastic ModellingTechniques and Applications);MASCOT'09,'10 (IEEE/ACM Int. Symp. on Modelling, Analysis andSimulation of Computer and Telecommunication Systems);

2.3 Partecipazione in progetti di ricerca

2006-08: Progetto europeo STREP FP6-2004-IST-4-027513 CRUTIAL (CRitical UTility InfrastructurAL resilience)2006-07: Progetto nazionale MIUR PRIN FAMOUS (Fluid Analytical Models Of aUtonomic Systems)2002-05: Progetto nazionale MIUR FIRB PERF (Performance Evaluation of Complex Systems: Techniques, Methodologies and Tools)2001-03: Progetto europeo EEC-IST 25434 DepAuDE (Dependability for embedded Automation systems in Dynamic Environments with intra-site and inter-sitedistribution aspects)2001-02: Progetto nazionale COFIN (ora PRIN) Planet-IP (PLanning IP NETworks)1999-2000: Progetto europeo EEC-IST 28620 TIRAN (TaIlorable fault toleRANce frameworks for embedded applications)

Inglese

1 Studies and positions

Andras Horvath received the M.Sc. degree in computer science at the Budapest University of Technology and Economics, Hungary, in 1997 and the PhD degree incomputer science in 2004. From the 1st of October 1999, to the 30th of September 2001, he was a temporary researcher at the Dept. of Computer Science of theUniversity of Turin. From April 2003 he is an assistant professor at the Dept. of Computer Science of the University of Turin.

2 Research activity

His research activity is focused on performance evaluation and correctness verification of discrete event systems. He published 14 papers in international journalsand 36 papers in refereed conference proceedings. More than 300 citations have been made to his papers.

2.1 Scientific achievements

We list his scientific achievements that are relevant for the project.

Approximation of non-Markovian behavior by Markovian models: Because of their analytical and numerical tractability, Markovian models, in particular, Markovchains, are widespread utilized in performance evaluation of discrete event systems. Markov chains, however, are limited for what concerns the types of behaviorsthey are able to model with precision. Nevertheless it is possible approximate non-Markovian behavior by Markovian models. In this context, he has developedalgorithms for the construction of Markovian models to approximate real phenomena [1,2,3,4,5,6,7,9,15,17,19,26,31,35,36,37].

Solution techniques for structured Markov chains: Application of Markovian approximations of non-Markovian behaviors results in structured Markov chains. He hasdeveloped techniques that, exploiting this structure, are capable of analyzing models with large state spaces [21,27,29,30,33,34,40].

Non-Markovian models: A non-Markovian model is a model whose state is described by one or more discrete components and one or more continuous components.On the contrary of Markov chains, non-Markovian models can describe non-exponential durations and the evolution of continuous quantities. He has contributed bothin the definition of formalisms for the description of non-Markovian models and for what concerns their solution techniques[8,10,11,12,14,15,18,20,22,23,24,25,28,32,41].

2.2 Participation in committees and organization of events

Program co-chair:

3rd European Performance Engineering Workshop (EPEW'06),Budapest, Hungary, June 2006;7th Int. Workshop on Performability Modeling of Computer andCommunication Systems) (PMCCS), Torino, Italy, Sep. 2005;TiSto'09, Int. Workshop on Timing and Stochasticity in Petri netsand other models of concurrency, Paris, France, June 2009;SMC'09, 4th International Workshop on Tools for solvingStructured Markov Chains, Pisa, Italy, 2009.

Program committee member:EPEW'06,'07,'08,'09 (European Performance Engineering Workshop);QEST'07,'09 (Int. Conf. on the Quantitative Evaluation of Systems);AMSTA'09,'10 (Int. Conf. on Analytical and Stochastic ModellingTechniques and Applications);MASCOT'09,'10 (IEEE/ACM Int. Symposium on Modelling, Analysis andSimulation of Computer and Telecommunication Systems);

2.3 Participation in research projects

2006-08: European project STREP FP6-2004-IST-4-027513 CRUTIAL (CRitical UTility InfrastructurAL resilience)2006-07: Italian national project MIUR PRIN FAMOUS (Fluid Analytical Models Of aUtonomic Systems2002-05: Italian national project MIUR FIRB PERF (Performance Evaluation of Complex Systems: Techniques, Methodologies and Tools)2001-03: European project EEC-IST 25434 DepAuDE (Dependability for embedded Automation systems in Dynamic Environments with intra-site and inter-sitedistribution aspects)2001-02: Italian national project COFIN (ora PRIN) Planet-IP (PLanning IP NETworks)1999-2000: European project EEC-IST 28620 TIRAN (TaIlorable fault toleRANce frameworks for embedded applications)

4

8 - Pubblicazioni scientifiche più significative del Coordinatore della Ricercanº Pubblicazione Titolo rivista

1. HORVATH A., G. HORVATH, M. TELEK. (2010). A joint moments based analysis of networks of MAP/MAP/1queues. PERFORMANCE EVALUATION, vol. 67; p. 759-778, ISSN: 0166-5316

PERFORMANCE EVALUATION

2. HORVATH A., G. HORVÁTH, M. TELEK (2009). A traffic based decomposition of two-class queueing networkswith priority service. COMPUTER NETWORKS, vol. 53; p. 1235-1248, ISSN: 1389-1286, doi:10.1016/j.comnet.2009.02.016

COMPUTER NETWORKS

3. L. NAPIONE, D. MANINI, F. CORDERO, HORVATH A., A. PICCO, M. DE PIERRO, S. PAVAN, M. SERENO,A. VEGLIO, F. BUSSOLINO, G. BALBO (2009). On the use of stochastic Petri nets in the analysis of SignalTransduction Pathways for Angiogenesis process. LECTURE NOTES IN COMPUTER SCIENCE, vol. LNBI5688; p. 281-295, ISSN: 0302-9743

LECTURE NOTES IN COMPUTERSCIENCE

4. HORVATH A., SÁNDOR RÁCZ, MIKLóS TELEK (2009). Moments Characterization of Order 3 MatrixExponential Distributions. LECTURE NOTES IN COMPUTER SCIENCE, vol. 5513; p. 174-188, ISSN:0302-9743


5. L. BODROG, HORVATH A., M. TELEK (2008). Moment characterization of matrix exponential and Markovianarrival processes. ANNALS OF OPERATIONS RESEARCH, vol. 160(1); p. 51-68, ISSN: 0254-5330

ANNALS OF OPERATIONSRESEARCH

6. HORVATH A., M. TELEK (2007). Matching more than three moments with acyclic phase type distributions.STOCHASTIC MODELS, vol. 23(2); p. 167-194, ISSN: 1532-6349

STOCHASTIC MODELS

7. M. GRIBAUDO, HORVATH A. (2005). Model checking functional and performability properties of stochasticfluid models. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. Vol. 128, n.6; p. 295-310,ISSN: 1571-0661

ELECTRONIC NOTES INTHEORETICAL COMPUTERSCIENCE

8. A. BOBBIO, HORVATH A., M. TELEK (2005). Matching three moments with minimal acyclic phase typedistributions. STOCHASTIC MODELS, vol. 21; p. 303-326, ISSN: 1532-6349

STOCHASTIC MODELS

9. A. BOBBIO, HORVATH A., M. TELEK (2004). The scale factor: A new degree of freedom in phase typeapproximation. PERFORMANCE EVALUATION, vol. 56(1-4); p. 121-144, ISSN: 0166-5316


10. HORVATH A., M. TELEK, G. HORVÁTH (2004). Analysis of inhomogeneous Markov reward models. LINEARALGEBRA AND ITS APPLICATIONS, vol. 386; p. 383-405, ISSN: 0024-3795

LINEAR ALGEBRA AND ITSAPPLICATIONS

11. M. GRIBAUDO, HORVATH A., A. BOBBIO, E. TRONCI, E. CIANCAMERLA, M. MINICHINO (2003). Fluidpetri nets and hybrid model-checking: A comparative case study. RELIABILITY ENGINEERING & SYSTEMSAFETY, vol. 81(3); p. 239-257, ISSN: 0951-8320

RELIABILITY ENGINEERING &SYSTEM SAFETY

12. M. GRIBAUDO, HORVATH A. (2003). Modeling hybrid positive systems with hybrid petri nets. LECTURENOTES IN COMPUTER SCIENCE, vol. 294; p. 71-78, ISSN: 0302-9743


13. A. BOBBIO, HORVATH A., M. SCARPA, M. TELEK (2003). Acyclic discrete phase type distributions:Properties and a parameter estimation algorithm. PERFORMANCE EVALUATION, vol. 54(1); p. 1-32, ISSN:0166-5316


14. HORVATH A., M. TELEK (2002). Time domain analysis of non-markovian stochastic petri nets with pritransitions. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, vol. 28(20); p. 933-943, ISSN: 0098-5589

IEEE TRANSACTIONS ONSOFTWARE ENGINEERING

15. M. GRIBAUDO, HORVATH A., A. BOBBIO, E. TRONCI, E. CIANCAMERLA, M. MINICHINO (2002).Model-checking based on fluid petri nets for the temperature control system of the icaro co-generative plant.LECTURE NOTES IN COMPUTER SCIENCE, vol. 2434; p. 273-283, ISSN: 0302-9743


16. HORVATH A., M. TELEK (2002). Phfit: A general phase-type fitting tool. LECTURE NOTES IN COMPUTERSCIENCE, vol. 2324; p. 82-91, ISSN: 0302-9743


17. HORVATH A., M. TELEK (2002). Markovian modeling of real data traffic: Heuristic phase type and map fittingof heavy tailed and fractal like samples. LECTURE NOTES IN COMPUTER SCIENCE, vol. 2459; p. 405-434,ISSN: 0302-9743


18. M. GRIBAUDO, HORVATH A. (2002). Fluid stochastic petri nets augmented with flush-out arcs: A transientanalysis technique. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, vol. 28(10); p. 944-955, ISSN:0098-5589

IEEE TRANSACTIONS ONSOFTWARE ENGINEERING

19. A. BOBBIO, HORVATH A. (2001). Petri nets with discrete phase type timing: A bridge between stochastic andfunctional analysis. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, vol. 52(3); p. 209-226,ISSN: 1571-0661

ELECTRONIC NOTES INTHEORETICAL COMPUTERSCIENCE

20. M. GRIBAUDO, M. SERENO, HORVATH A., A. BOBBIO (2001). Fluid stochastic Petri nets augmented withflush-out arcs: Modelling and analysis. DISCRETE EVENT DYNAMIC SYSTEMS, vol. 11; p. 97-111, ISSN:0924-6703

DISCRETE EVENT DYNAMICSYSTEMS

21. S. BERNARDI, S. DONATELLI, HORVATH A. (2001). Special session on the practical use of high-level Petri Nets:Implementing compositionality for stochastic petri nets. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FORTECHNOLOGY TRANSFER, vol. 3(4); p. 417-430, ISSN: 1433-2779

INTERNATIONALJOURNAL ONSOFTWARE TOOLSFOR TECHNOLOGYTRANSFER

22. M. TELEK, HORVATH A. (2001). Transient analysis of age-MRSPNs by the method supplementary variables.PERFORMANCE EVALUATION, vol. 45(4); p. 205-221, ISSN: 0166-5316

PERFORMANCEEVALUATION

23. M. GRIBAUDO, M. SERENO, HORVATH A., A. BOBBIO (2001). Fluid Stochastic Petri Nets Augmented with Flush-outArcs: Modelling and Analysis. DISCRETE EVENT DYNAMIC SYSTEMS, vol. Volume 11, Numbers 1-2, Januar; p. 97-117,ISSN: 0924-6703, doi: 10.1023/A:1008339216603

DISCRETE EVENTDYNAMIC SYSTEMS

24. HORVATH A., A. PULIAFITO, M. SCARPA, M. TELEK (2000). Analysis and evaluation of non-Markovian stochastic Petrinets. LECTURE NOTES IN COMPUTER SCIENCE, vol. 1786; p. 171-187, ISSN: 0302-9743

LECTURE NOTES INCOMPUTER SCIENCE

25. HORVATH A., L. RIDI, E. VICARIO. (2010). Transient analysis of generalised semi-Markov processes using transientstochastic state classes. In: Proc. of 7th International Conference on the Quantitative Evaluation of Systems (QEST).Williamsburg, VA, USA, Sept 15-Sept 18, Los Alamitos: IEEE Computer Society, p. 231-240, ISBN/ISSN: 9780769541884

26. HORVATH A., L. RIDI, E. VICARIO (2010). Approximating distributions and transient probabilities of Markov chains byBernstein expolynomial functions. In: Proc. of International Conference on the Numerical Solution of Markov Chains.Williamsburg, VA, USA, September 15-18, Williamsburg, VA, USA: College of William & Mary, p. 52-55

27. P. BALLARINI, HORVATH A. (2009). Memory efficient analysis for a class of large structured Markov chains [work inprogress]. In: Proc. of International Workshop on Tools for solving Structured Markov Chains (SMCtools'09). Pisa, Italy,Oct 2009, Gent, Belgium: Institute for Computer Sciences, Social-Informatic, p. 1-4

5

28. HORVATH A., E. VICARIO (2009). Aggregated stochastic state classes in quantitative evaluation of non-Markovianstochastic Petri nets. In: Proc. of 6th International Conference on the Quantitative Evaluation of Systems (QEST). Budapest,Hungary, Sept. 2009, Los Alamitos: IEEE Computer Society, p. 155-164

29. P. BALLARINI, HORVATH A. (2008). Memory efficient calculation of path probabilities in large structured markov chains.In: Proc. of 5nd International Conference on the Quantitative Evaluation of Systems (QEST). St Malo, France, Sept 2008,STATI UNITI D'AMERICA: IEEE CS Press, p. 157-166

30. P. BALLARINI, HORVATH A. (2007). Compositional model checking of product-form CTMCs. In: Proc. of 7th InternationalWorkshop on Automated Verification of Critical Systems (AVOCS'07). Oxford, 10-12 September, 2007, Oxford: MichaelGoldsmith, Bill Roscoe, p. 1-16

31. HORVATH A., M. TELEK (2007). On the properties of acyclic bilateral phase type distributions. In: Proc. of InternationalWorkshop on Tools for solving Structured Markov Chains (SMCtools 2007). Nantes, France, 26/10/2007, Dortmund: PeterBuchholz, Tugrul Dayar, p. 1-8

32. D. CEROTTI, S. DONATELLI, HORVATH A., J. SPROSTON (2006). CSL model checking for generalized stochastic Petrinets. In: Proc. of 3rd International Conference on the Quantitative Evaluation of Systems (QEST). Riversida, California,USA, Sept 2006, Riversida, California, USA: Gianfranco Ciardo, p. 199-210

33. HORVATH A. (2005). Steady state solution for models with geometric and finite support activity duration. In: Proc. of 2ndInternational Conference on the Quantitative Evaluation of Systems (QEST'05). Torino, Italy, 19-22/9/2005, Torino, Italy:Gianfranco Balbo, p. 114-123

34. HORVATH A., M. GRIBAUDO (2002). Matrix geometric solution of fluid stochastic petri nets. In: Proc. 4th InternationalConference on Matrix-Analytic Methods in Stochastic models

35. HORVATH A., M. TELEK (2002). A markovian point process exhibiting multifractal behaviour and its application to trafficmodeling. In: Proc. 4th International Conference on Matrix-Analytic Methods in Stochastic models

36. HORVATH A., M. TELEK (2000). Approximating heavy tailed behavior with phase type distributions. In: Proc. of 3rdInternational Conference on Matrix-Analytic Methods in Stochastic models

37. HORVATH A., G. I. RZSA, M. TELEK (2000). A MAP fitting method to approximate real traffic behavior. In: Proc. of 8thIFIP Workshop on Performance Modeling and Evaluation of ATM and IP

38. A. BOBBIO, S. GARG, M. GRIBAUDO, HORVATH A., M. SERENO, M. TELEK (1999). Modeling software systems withrejuvenation, restoration and checkpointing through fluid stochastic Petri nets. In: Proc. of 8th Intern. Workshop on PetriNets and Performance Models

39. A. BOBBIO, S. GARG, M. GRIBAUDO, HORVATH A., M. SERENO, M. TELEK (1999). Modeling Software Systems withRejuvenation, Restoration and Checkpointing through Fluid Stochastic Petri Nets. In: International Workshop on Petri Netsand Performance Models (PNPM '99). Zaragoza, Spain, 8-10 Settembre 1999, Washington, DC, USA: IEEE ComputerSociety, p. 82-91, ISBN/ISSN: 0-7695-0331-4 , doi: 10.1109/PNPM.1999.796555

40. HORVATH A., A. PULIAFITO, M. SCARPA, M. TELEK, O. TOMARCHIO (1998). Design and implementation of aWEB-based non-Markovian stochastic Petri net tool. In: Advances in Computer and Information Sciences, Proc. of ISCIS'98

41. M. TELEK, HORVATH A. (1998). Supplementary variable approach applied to the transient analysis of age-MRSPNs. In: Proc. of 3rd InternationalComputer Performance & Dependability Symposium (IPDS '98)

42. HORVATH A., B. MEINI (a cura di) (2009). Proc. of 4th International Workshop on Tools for solving Structured Markov Chains. Gent, Belgium:nstitute for Computer Sciences, Social-Informatics, ISBN: 978-963-9799-70-7

43. HORVATH A., O. H. ROUX (a cura di) (2009). Proc. of 1st International Workshop International Workshop on Timing and Stochasticity in Petri netsand other models of concurrency. Paris: University Pierre & Marie Curie

44. HORVATH A., M. TELEK (a cura di) (2006). Lecture Notes in Computer Science, 4054, Formal Methods and Stochastic Models for PerformanceEvaluation, Third European Performance Engineering Workshop, EPEW 2006. Budapest: A. HORVATH, M. TELEK, ISBN: 3-540-35362-3

45. HORVATH A., A. RISKA (a cura di) (2005). Proc. of 7th International Workshop on Performability Modeling of Computer and CommunicationSystems (PMCCS7). Torino: A. HORVATH, A. RISKA

9 - Elenco delle Unità di Ricerca (UR)nº Responsabile scientifico Qualifica Istituzione Dip/Ist/Div/Sez Mesi/Persona1. HORVATH Andras Ricercatore confermato Università degli Studi di TORINO Dipartimento di INFORMATICA 75

2. GRIBAUDO Marco Ricercatore confermato Politecnico di MILANO Dipartimento di ELETTRONICA E INFORMAZIONE 40

3. BRUNEO Dario Ricercatore confermato Università degli Studi di MESSINA Dipartimento di MATEMATICA 73

4. LORETI Michele Ricercatore confermato Università degli Studi di FIRENZE Dipartimento di SISTEMI E INFORMATICA 52

10 - Breve descrizione della RicercaItaliano

Il progetto si propone di affrontare problematiche di ricerca di base, ispirate da precisi ambiti applicativi, nell'area della valutazione quantitativa di modelliprobabilistici, temporizzati e concorrenti. Le applicazioni prese in esame (quattro casi di studio nell'area dell'ingegneria ed uno relativo all'economia) spaziano su unvasto campo di problemi di modellistica e progettazione. Dopo averle descritte, si forniranno le direzioni di ricerca identificate allo scopo di dare un contributo neltrattamento di tali applicazioni.

1 Aree applicative

Le applicazioni saranno utilizzate per identificare i problemi di natura pratica sui quali le tecniche sviluppate saranno testate. Per ognuna di esse, si fornirà unadescrizione del fenomeno da modellare e si definiranno gli obbiettivi dell'analisi.

1.1 Cloud computing

Il cloud computing è un recente paradigma di calcolo distribuito secondo il quale i dati ed i servizi risiedono in data center scalabili e accessibili in manierapervasiva tramite la rete Internet. In tale contesto, verranno affrontati problemi di ottimizzazione: valutare, date le richieste da parte degli utenti, il dimensionamentodelle risorse e la configurazione ottimale per soddisfare i requisiti di service level agreement (SLA) e minimizzare il costo totale ed il consumo energetico. Ledimensioni dei siti cloud e l'eterogeneità dei domini amministrativi portano ad interessanti sfide nell'ambito della valutazione delle prestazioni. In tale contesto,infatti, risultano spesso coinvolti un elevato numero di parametri dipendenti dal tempo la cui regolazione è resa complessa dall'autonomia di ogni sito. Al contempo,

6

la complessità delle infrastrutture può portare a fenomeni di esplosione dello spazio degli stati.

1.2 Reti wireless di sensori (WSN)

Le reti wireless di sensori sono reti composte da sensori equipaggiati con interfacce radio e distribuiti su di un'area geograficamente estesa. L'attività di ricerca intale ambito si è finora focalizzata su aspetti di comunicazione di rete e di gestione dei dati. Nonostante ciò, molte applicazioni presentano requisiti stringenti diaffidabilità. Ciò è dovuto al fatto che i sensori generalmente utilizzati presentano un tempo di vita limitato. Al fine di ridurre il consumo energetico, i nodi possonoessere messi in modalità sleep, disattivando l'equipaggiamento radio quando non è necessario trasmettere dati. La modellazione di tali reti presenta aspetti complessiquali la presenza di timer e di altri eventi non esponenzialmente distribuiti o la necessità di sincronizzazione tra i differenti sensori e/o tra le varie attività di unostesso sensore.

1.3 Predizione per infrastrutture di monitoraggio distribuito

Si consideri uno scenario in cui un sistema critico viene supervisionato da una infrastruttura dinamica di monitoraggio allo scopo di tenere traccia della suaevoluzione e fornire misure quantitative sul raggiungimento delle condizioni critiche. Tale scenario potrebbe essere costituito da un luogo pubblico (e.g. un aeroportoo un museo) tenuto sotto sorveglianza mediante una rete di telecamere e/o da una WSN. In particolare, la WSN potrebbe effettuare un monitoraggio pervasivo dibasso livello identificando comportamenti che potrebbero condurre a condizioni critiche e guidando l'infrastruttura di monitoraggio a orientare le telecamere versole regioni di interesse o ad azionare meccanismi di escalation. Lo studio di tali sistemi richiede strumenti per la valutazione della probabilità di raggiungere lecondizioni critiche entro un certo orizzonte temporale. E' necessario porre le basi per un motore di predizione dinamica che, osservando l'evoluzione del sistema, siain grado di quantificare la probabilità di possibili futuri comportamenti in maniera energeticamente efficiente.

1.4 Processo di sviluppo industriale di SW real-time

Nel contesto dello sviluppo di SW real-time soggetto a standard di certificazioni, si affronterà il caso di un controllore real-time caratterizzato da task concorrentieseguiti su processori con schedulazione preemptive. Il modello include molteplici timer concorrenti con distribuzioni non esponenziali su un supporto eventualmentefinito (e.g., timeout, picchi di traffico, ritardi variabili). L'analisi di tale scenario richiede tecniche che siano in grado di analizzare modelli non Markoviani in gradodi associare misure di probabilità ai possibili comportamenti del sistema (e.g., probabilità di condizioni di carico elevato, distribuzione del tempo di completamento).L'obbiettivo è quello di assistere i passi della progettazione e della validazione del SW real-time ottenendo un alto livello di rigore durante l'intero processo disviluppo.

1.5 Diffusione di modelli organizzativi di business

Un'area applicativa innovativa per la valutazione formale e quantitativa è quella della diffusione di modelli organizzativi di business aperti e di obbiettivi strategici invari settori industriali. Una volta identificati tali settori, le relative aziende verranno caratterizzate su certo periodo di tempo in termini del loro modelloorganizzativo e del loro obbiettivo strategico. Sulla base di tale caratterizzazione, sarà costruito un modello del settore industriale utile a catturare, se esiste, lacorrelazione tra il modello organizzativo, l'obbiettivo strategico e le prestazioni delle aziende. Il modello sarà validato verificando se esso è in grado di fornireinformazioni utili sulla evoluzione del settore industriale.

2 Percorsi di ricerca

L'applicabilità di approcci di modellazione formale per sistemi probabilistici, temporizzati e concorrenti è limitata dai seguenti fattori: (1) la maggior parte delletecniche considera Markoviani il cui potere espressivo è spesso troppo basso; (2) anche se tramite Markovianizzazione un modello Markoviano può essere utilizzatoper descrivere il sistema, il problema dell'esplosione dello spazio degli stati può impedirne l'analisi; (3) i modi in cui sono poste le domande a cui l'analisi deve darerisposta sono spesso limitati e/o poco naturali per i non esperti. Le seguenti linee di ricerca sono state identificate allo scopo di superare queste limitazioni.

2.1 Analisi di modelli non Markoviani tramite Markovianizzazione

Uno degli approcci tramite i quali è possibile studiare modelli non Markoviani è quello di attuare una approssimazione Markoviana dei tempi del sistema. A questoscopo possono essere utilizzate le distribuzioni phase type (PH). Recentemente è stato dimostrato che anche le distribuzioni matrix exponential (ME) consentonol'applicazione di tecniche numeriche sviluppate per le catene di Markov. La maggior parte delle tecniche attualmente disponibili sono sviluppate per il dominio tempocontinuo. Studi recenti hanno dimostrato che alcune importanti proprietà (e.g. la presenza di un supporto finito) possono essere meglio caratterizzate nell'ambito deltempo discreto. Conseguentemente, si definirà la controparte discreta delle distribuzioni ME e verranno estesi gli approcci di approssimazioni più promettenti. Traquesti vi è quello basato su famiglie di polinomi ortogonali (Jacobi o Bernstein) per il quale risulta ancora necessario sviluppare gli algoritmi associati. Verràinvestigato anche l'utilizzo di altre promettenti famiglie (e.g. quella della somma di polinomi quadrati).

Un problema simile è quello della modellazione dei pattern di traffico. Se il traffico è descritto da un processo di arrivo Markoviano (MAP) o da un processo matrixexponential (MEP) allora il modello del sistema completo può essere risolto tramite tecniche sviluppate per i modelli Markoviani. Un problema cruciale è quello diriprodurre fedelmente la correlazione e la struttura dei picchi di carico. Si valuteranno le tecniche esistenti e saranno sviluppate nuove tecniche con particolareattenzione a schemi di interazione innovativi (e.g. le reti sociali o quelle p2p) che presentano picchi di carico sia in download che in upload con un impatto notevolesull'infrastruttura sottostante.

I modelli in cui i tempi sono rappresentati da distribuzioni PH e i processi di arrivo sono di tipo MAP possono essere descritti, tramite l'approccio di espansione dellospazio degli stati, tramite catene di Markov. Lo svantaggi di questa tecnica è l'esplosione dello spazio degli stati. E' possibile affrontare tale problema ricorrendo atecniche di rappresentazione simbolica e all'algebra di Kronecker che consentono una rappresentazione compatta. Verranno utilizzati multi-terminal multi-valueddecision diagram e altre strutture dati per immagazzinare lo spazio degli stati espanso e saranno sviluppati nuovi algoritmi di generazione dello spazio degli statibasati sulla saturazione.

Come menzionato precedentemente, i modelli che includono distribuzioni ME e processi di arrivo di tipo MEP possono essere analizzati grazie a tecniche numerichesviluppate per le catene di Markov. Nel caso di questi modelli, però, l'errore numerico non è facilmente stimabile. Conseguentemente, verranno sviluppate tecniche disoluzione efficienti basate su risolutori di equazioni differenziali e sistemi lineari. Verrà, inoltre, sfruttata la caratteristiche delle distribuzioni ME e MEPs per cuiesse hanno un infinito numero di rappresentazioni e la scelta di quella da utilizzare ha un impatto sull'errore numerico.

2.2 Analisi approssimata di modelli non Markoviani

L'approccio mean field può essere utilizzato per approssimare il comportamento di sistemi composti da un elevato numero di oggetti interagenti. I risultati fornitisono esatti in senso asintotico ovvero quando il numero degli oggetti tende all'infinito. Nell'approccio mean field classico ogni oggetto è rappresentato da una catenadi Markov. L'obbiettivo è quello di estendere l'approccio mean field al caso di oggetti che hanno uno spazio degli stati ibrido in cui ogni stato presenta una partecontinua e una discreta.

Un altra famiglia di tecniche asintotiche che verranno prese in considerazione è quella che permette di identificare i colli di bottiglia di un sistema allo scopo diprogettare politiche di allocazione adeguate. Anche se tali tecniche sono ben consolidate, rimangono da indagare parecchi punti. In particolare, si studierà l'impattodella potenza del sistema. Questo indice è definito come il rapporto tra il throughput e il tempo di risposta: massimizzare la potenza del sistema significa ottenere ilthroughput massimo riducendo al contempo il tempo di risposta.

7

Nel caso di sistemi complessi composti da sotto-sistemi quasi indipendenti, una approssimazione a regime può essere ottenuta tramite l'utilizzo di iterazioni di puntofisso, risolvendo i sotto-modelli in isolamento e esprimendo le dipendenze attraverso il passaggio di parametri. Ci si propone di estendere tale approccio al caso dianalisi in transitorio di sistemi non Markoviani. Ciò richiede che le informazioni scambiate tra i sotto-modelli non siano parametri a valore singolo ma distribuzioni.Come conseguenza, risulta necessario investigare le condizioni di convergenza.

Una tecnica di esatta per modelli non Markoviani è quella fornita della classi di stato stocastiche. vettori dei tempi residui sono supportati su zone DBM (differencebound matrix) le quali consentono una codifica compatta e una manipolazione efficiente. Tuttavia, questa proprietà dipende dall'assunzione di una semanticapreemptive repeat different (PRD) e non è conservata in caso di semantica preemptive resume (PRs) che rappresenta l'approccio di gran lunga più comune 'ambitodeisistemi real-time. si propone di estenderetecniche fine di includere modelli che combinino differenti politiche di preemption: PRD, PRs e PRI (Repeat Identical). Aquesto scopo, sarà proposto un approccio approssimato che mantenga il supporto dei timer nei limiti della rappresentazione DBM, rendendo possibilel'implementazione per sistemi di dimensioni .

2.3 Model checking

Nell'ambito di processi di Markov rigenerativi il comportamento del modello può essere descritto e analizzato tramite i kernel locale e globale. Il metodo delle classidi stato stocastiche può essere utilizzato per ottenere una descrizione simbolica dei due kernel. Verrà sfruttata questa proprietà per sviluppare procedure di modelchecking basate sull'approccio delle classi di stato stocastiche. In particolare, la generazione delle classi sarà guidata dalla formula che deve essere verificata. Sitesteranno anche tecniche di approssimazione tramite distribuzioni per la rappresentazione dei kernel.

I risolutori esistenti per problemi di model checking su modelli Markoviani forniscono un insieme limitato di operatori e metodi ad-hoc per la loro soluzione. Leprocedure utilizzate risultano poco flessibili dato che è difficile estenderle a operatori che non sono nell'insieme predefinito. La logica CSL-TA è stata proposta perfornire un modo più generale per esprimere le formule, basata sugli automi temporizzati. L'algoritmo già esistente per il model checkin CSL-TA è flessibile ma nonefficiente. Verrà studiato come è possibile ottenere un algoritmo più efficiente e le sue prestazioni saranno valutate sia teoricamente che sperimentalmente.

Nell'ambito del model-checking, la tecnica di astrazione viene utilizzata per calcolare, tramite un modello più piccolo, i valori limite della probabilità con cui unsistema soddisfa una certa proprietà. Questa idea verrà applicata ai sistemi non Markoviani per ottenere una sorta discretizzazione delle distribuzioni di probabilitàcontinue. L'uso di region graph per la costruzione del modello astratto generalmente conduce a sistemi con grossi spazi degli stati. Per gli automi temporizzati,metodi alternativi si sono dimostrati vantaggiosi. Sulla base di questi precedenti, saranno sviluppati dei metodi di astrazione per sistemi non Markoviani che evitanola costruzione esplicita del region graph.

Un altro approccio per la verifica formale è il model checking statistico per il quale ci sono ancora problemi aperti nel caso di applicazione ai modelli nonMarkoviani. Verrà studiato l'utilizzo di campioni stratificati per guidare la generazione di run di simulazione in modo da valutare una formula con il livello dicertezza più elevato possibile fissato il numero di run. Considerando che i modelli non Markoviani sono più espressivi di quelli Markoviani, anche la logica che vieneutilizzata per esprimere le formule deve essere più espressiva. Verrà sviluppata una logica grazie alla quale sarà possibile riferirsi alla parte intrinsecamente nonMarkoviana del modello, come le componenti a stati continui (e.g., la temperatura) o i tempi residui.

Infine, verranno studiate delle tecniche per gestire la specifica composizione e l'analisi quantitativa di sistemi concorrenti temporizzati. In particolare, verrà seguitol'approccio sviluppato per l'analisi quantitativa: solo alcune parti del sistema sono completamente specificati mentre il resto è descritto da una serie di assunzioni.Algoritmi formali adatti allo scopo verranno definiti per verificare se alcune proprietà sono soddisfatte o meno nel caso in cui la specifica è eseguita in un ambienteche rispetta le assunzioni considerate.

Inglese

The project proposes fundamental research in the area of quantitative evaluation of probabilistic timed concurrent models inspired by applications. First, we describethe applications (four engineering themes and one from economics) which cover a wide range of modeling and design problems. Then we provide research directionsthat we have identified to advance the state of the art of the treatment of these problems.

1 Application areas

The applications will be used to set up problems to test the developed techniques. They provide a description of the phenomena to model and define the goal of theanalysis.

1.1 Cloud computing

Cloud computing is an emerging paradigm where data and services reside in scalable data centers and can be ubiquitously accessed from any connected device overthe Internet. Cloud providers need to acquire sufficient number of virtual resources using underlying physical resources (servers, storage, and networks) to handleand satisfy user demands. We will tackle optimization problems in this context. Given a set of user demands to the cloud, what are the optimal capacity andconfiguration to uphold the service level agreement (SLA) requirements while minimizing the total cost and energy consumption? The large-scale of the cloud sitesand the heterogeneity of administration domains bring to challenges in the quality of service (QoS) and performance assessment of cloud infrastructures. Several timedependent parameters and events are involved, the autonomy of each site could complicate their specific setting and the complexity of the infrastructure can bring tothe explosion of the state space.

1.2 Wireless sensor networks

Wireless sensor networks (WSN) are networks composed of sensors equipped with radio interfaces and distributed over a geographical region. Recent research onWSN was mainly focused on networking aspects and data management. However, many applications also have strict dependability requirements. In fact, sensors donot guarantee continuous functioning over time and have limited lifetime. To reduce energy consumption, nodes can be turned off in sleep mode, deactivating theradio equipments when no data have to be transmitted. The presence of timers and other non-exponentially distributed events and the necessity of synchronizationamong different sensors and/or among different activities with the same equipment are crucial aspects in modeling sensor networks.

1.3 Online prediction for distributed monitoring infrastructures

We consider a safety-critical scenario supervised by an on-line monitoring infrastructure in order to keep track of its evolution and provide quantitative measures onthe reachability of critical conditions. Such scenario can be a public place (e.g., an airport or a museum) kept under surveillance by a network of cameras and/or aWSN. In particular, the WSN may be used to enforce low-level pervasive sensing to identify behaviors that may lead to critical conditions, driving the monitoringinfrastructure to point cameras towards regions of interest or to trigger escalation mechanism. The validation of such systems requires means to evaluate theprobability of reaching critical conditions within a finite time horizon. These means then constitute the basis for an on-line prediction engine that, observing theevolution of the system, provides the possible future behaviors quantifying their probabilities. Such prediction engine can provide energy-efficient strategies thatadapt the operating conditions to the actual and expected states of the supervised system.

1.4 Development process of real-time SW

In the context of development of real-time SW subject to certification standards, we address the case of a real-time controller includingmultiple concurrent tasks running on a set of processors under preemptive scheduling. When temporal parameters of the system are associated with a stochasticcharacterization, the model includes multiple concurrent timings with non-exponential distribution over a possibly finite support (e.g., timeouts, bursty traffic, jittering

8

delays). The analysis requires techniques for non-Markovian preemptive models including the possibility of associating probability measures to the feasible behaviorsof the system, enabling the derivation of performance measures (e.g., probability of heavy workload conditions, distribution of completion time). The goal is tosupport the steps of design and verification of real-time SW and to permit a higher degree of rigor in the overall development process.

1.5 Diffusion of business organization models

As a novel application area to formal quantitative evaluation, we will consider the diffusion of open business organization models and strategic focus in variousindustries. Having chosen the industries, the companies will be characterized over a period of time in terms of their organization model and strategic focus. Based onthis characterization, a model of the industry able to capture, if exists, the correlation between the organizational model, the strategic focus and the performance ofthe companies will be constructed. The model will be validated by verifying if it will be capable to provide useful insight in to the evolution of the industry and itsrelevant companies.

2 Research directions

The applicability of formal modeling approaches for probabilistic timed concurrent systems are limited by the following factors: (1) most techniques addressMarkovian models whose expressive power is often too low for real problems;(2) even if by Markovianization a Markovian model can describe the system, state spaceexplosion can inhibit the analysis;(3) the ways of expressing the questions that the analysis has to answer are often limited and/or not natural for non-experts. Wehave identified the following research lines to overcome these limitations.

2.1 Analysis of non-Markovian models by Markovianization

An approach to treat non-Markovian models is to substitute the non-Markovian durations by Markovian approximations. To this purpose phase type (PH)distributions are usually used, but recently it has been shown that also matrix exponential (ME) distributions, which do not have a Markovian interpretation, lead tosystems that can be tackled by numerical techniques developed for Markovian chains. The most recent survey on approximations with PH distributions dates back to1997 and no such survey exists for ME distributions. Based on the applications, we will collect a benchmark of distributions and evaluate the available techniques.Most techniques are developed for the continuous time domain even if recent studies have shown that important features (like finite support or low variability) can bebetter faced in discrete time. We will define the discrete time counterpart of ME distributions and will transfer the most promising fitting approaches to discrete time.A novel approach of approximation is based on families of polynomials (Jacobi or Bernstein) but it still requires a proper development of the associated algorithms.We will investigate also the use of another promising family, namely, the sum of squares polynomials.

A problem similar to distribution approximation is traffic characterization, aiming at constructing models to reproduce traffic patterns. If the traffic is described by aMarkovian arrival process (MAP) or a matrix exponential process (MEP) then the overall system model can be solved by techniques developed for Markovianmodels. A crucial point is to properly reproduce the correlation and the burstiness structure of the traffic, being these two aspects crucial from a performance point ofview. We will evaluate the existing techniques and develop new ones with special attention to the fact that novel interaction schemes (like social or p2p networks) havenot only heavy download but heavy upload traffic as well and it has a strong impact on the underlying infrastructure.

Models composed of PH distributed durations and MAPs can be described, through a state space expansion approach, by Markov chains. The drawback of thisapproach is the explosion of the state space. One way to face this problem is to recur to symbolic state space representation techniques that, together with Kroneckeralgebra, can lead to a compact representation. In particular, we will study multi-terminal multi-valued decision diagrams and other symbolic data structures as a wayto store the so-called augmented reachability graph and we will develop new ways to collect all the necessary information by applying saturation based state spacegeneration algorithms.

As mentioned before, models including ME distributions and MEPs give rise to systems that can be tackled by numerical techniques developed for Markov chains. Adifference is however that when these techniques are applied to Markov chains, the numerical error of the calculations is easy to control while this is not the case formodels with ME distributions and MEPs. We will develop efficient solution techniques for such models based on both general differential equation and linear systemsolvers and by exploiting characteristics of ME distributions and MEPs (as the fact that they have an infinite number of representations and the choice of therepresentation has as impact on the numerical error of the analysis).

2.2 Approximate analysis of non-Markovian models

The mean field approach is used to approximate the transient and the stationary behavior of systems composed of a large number of interacting objects. The providedresults are exact in an asymptotic sense, i.e., when the number of objects tends to infinity. In the classical mean field approach each object is a Markov chain with adiscrete state space. The goal is to extend the mean field approach to support objects that have a hybrid state space, i.e., a state is composed by both a discrete and acontinuous component.

Another family of asymptotic techniques that we will consider is the one proposed to identify bottlenecks of a system and it is used to design adequate allocationpolicies. Although asymptotic techniques are well established, several open issues still remain to be investigated. In particular the task will study the impact of theco-called system power, an important performance measure never fully investigated. This index is defined as the ratio between the throughput and the response time:maximizing the system power means obtaining the highest throughput while reducing the response time.

Complex models are often composed of nearly independent subsystems. Exact solution of these models is unfeasible due to the state space explosion problem. Steadystate approximations can be obtained by an iterative fixed point scheme solving the submodels in isolation and expressing the dependencies through passingparameters. We propose to extend the fixed point approach to transient analysis of non-Markovian techniques. This extension requires that the information exchangedamong the submodels is not single parameters but distributions and we will use approximations by PH and ME distributions to this purpose. Convergence conditionswill have to be investigated.

An exact analysis technique for non-Markovian models is provided by stochastic state classes. With this technique vectors of times to events turn out to be supportedover difference bounds matrix (DBM) zones which accept compact encoding and efficient manipulation. However, this fortunate property depends on the assumptionof a preemptive repeat different (PRD) policy, and is not preserved in the case of preemptive resume (PRs) behavior. This rules out suspension and preventsrepresentation of systems running under preemptive scheduling, which is by far the most common approach in the practice of real-time systems. We will advance thetheory of stochastic state classes to encompass models combining different preemption policies, notably PRD, PRs. To this end, we will propose an approximateapproach that maintains timers supports in the limits of DBM encoding in order to make the implementation viable for systems of realistic size.

2.3 Model checking

When a non-Markovian process encounters regeneration points with probability one (i.e., when we deal with Markov regenerative processes), then the behavior of themodel can be described and analyzed by the so called local and global kernels. The method of stochastic state classes can be used to obtain a symbolic description ofthe entries of the two kernels. We will use this possibility to develop model checking procedures based on the stochastic state class approach. In particular, thegeneration of the classes will be guided by the formula to be verified. Moreover, as the entries of the kernel can be of notable complexity, we will test distributionapproximation techniques to simplify them.

Existing solvers for model checking problems over Markovian models provide a limited set of operators and ad-hoc methods for their solution. These procedures are“hard-coded” in the tool and make them inflexible because it is hard to extend them to operators that are not in the predefined set. To overcome this problem theCSL-TA logic was proposed providing a more general way of expressing formulas based on timed automata. The already existing CSL-TA model checking algorithmis flexible but not efficient. We will study how a more efficient one can be developed and integrate it to the MC4CSLTA tool. The performance of the new algorithm

9

will be evaluated both theoretically and experimentally and will be compared against that of other tools.

Abstraction, in the context of model-checking, is used to obtain approximations, meaning that a smaller model is used to compute bounds on the probability withwhich the system satisfies a certain property. An approach to abstraction in probabilistic systems replaces some probabilistic choice with nondeterministic choice.This idea will be applied to non-Markovian systems to obtain "discretizations" of continuous probability distributions. This approach has precedents relying on regiongraphs for the construction of the abstract model that generally leads to systems with large state spaces. For timed automata, alternative methods have been shown tobe successful. Noting this, we will develop abstraction methods for non-Markovian systems which avoid the explicit construction of the region graph.

Another approach of formal verification is statistical model checking. While this approach has received attention mostly for large scale Markovian models, there areopen questions when applied to non-Markovian models. We will study the use of stratified sampling to guide the generation of simulation runs in order to evaluate aformula with as much certainty as possible with a given number of runs. As non-Markovian models are more expressive than Markovian ones, also the logic toexpress formulas has to be more expressive. We will develop a logic by which it is possible to refer to the intrinsically non-Markovian part of the model, such ascontinuous state components (like temperature) or remaining activity durations (which can be non-exponential).

Finally, we will study techniques for supporting compositional specifications and quantitative analysis of timed concurrent systems. In particular, we will follow theapproaches developed for qualitative analysis. With these approaches only some parts of the system are completely specified and the rest is described as a set ofassumptions. Suitable formal algorithms will be then defined to verify whether properties are satisfied or not given that the specification is executed in an environmentsatisfying the considered assumptions.

11 - Stato dell'arte e riferimenti bibliograficiItaliano

Questa sezione è strutturata come la precedente.

1 Aree di applicazione

1.1 Cloud computing (CC)

La valutazione della qualità del servizio e delle prestazioni di applicazioni CC è un problema strategico e sono state proposte molte tecniche per risolverlo. Peresempio, in [Y09] è stato sviluppato un framework per analizzare l'acquisizione di risorse e i tempi di rilascio in Amazon EC2 in varie condizioni di carico. In[VBV09] è stato studiato l'effetto della migrazione dinamica di macchine virtuali sui SLAs. Aspetti riguardanti l'affidabilità sono invece presi in considerazione in[DY09]. [Ya09] illustra che il tempo di esecuzione aumenta se i sub-task di un lavoro falliscono. [BPA09] descrive la struttura di un sistema di memoria affidabile eproduttivo con elevata disponibilità malgrado i fallimenti dei server.

[BPA09] N. Bonvin, T. G. Papaioannou, K. Aberer. Dynamic cost efficient replications in data clouds, in ACDC, 2009[DY09] Y. S. Dai, B. Yang, J. Dongarra, G. Zhang. Cloud service reliability: Modeling and analysis, in PRDC, 2009.[VBV09] W. Voorsluys, J. Broberg, S. Venugopal, R. Buyya. Cost of virtual machine live migration in clouds: A performance evaluation, in CloudComp, 2009.[Y09] N. Yigitbasi et al. C-meter: A framework for performance analysis of computing clouds, in Cloud, 2009.[Ya09] B. Yang et al. Performance evaluation of cloud service considering fault recovery, in CloudComp, 2009.

1.2 Wireless sensor networks (WSN)

Le WSN sono oggetto di ricerca da circa dieci anni e i primi lavori si sono concentrati sugli aspetti di rete (una panoramica è riportata in [AY05]) e sulla gestionedei dati [ZG04]. L'affidabilità e la sicurezza, aspetti cruciali in molte applicazioni industriali, sono state considerate più recentemente [MSP09]. Una caratteristicapeculiare dei sensori è la capacità di passare in una modalità dormiente, che consente di risparmiare energia ma non di comunicare. Questo costituisce un problemaquando un nodo dormiente è coinvolto in una comunicazione multi-hop, interrompendo il collegamento. Possibili soluzioni consistono nell'applicare protocolli diinstradamento che si auto-adattano ai cambiamenti dell'ambiente o nel progettare reti ridondanti. [BPS10].

[AY05] K. Akkaya, M. Younis. A survey on routing protocols for wireless sensor networks. Ad Hoc Networks, 3:325-349, 2005.[BPS10] D. Bruneo, A. Puliafito, M. Scarpa. Dependability analysis of Wireless Sensor Networks with active-sleep cycles and redundant nodes. In DYADEM-FTS,2010.[MSP09] S. Mukhopadhyay, C. Schurgers, D. Panigrahi, S. Dey. Model-Based Techniques for Data Reliability in Wireless Sensor Networks. IEEE Tr. on MobileComputing, 8(4):528-543, 2009.[ZG04] F. Zhao, L. Guibas. Wireless sensor networks - An information processing approach. Morgan Kaufmann, 2004.

1.3 Predizione dinamica per infrastrutture di monitoraggio distribuito

Sono stati pubblicati pochi lavori sul tema. In [DGM05], le richieste inviate a una rete di nodi sono approssimate tenendo conto dello stato di un modello del sistemamonitorato, rappresentato come un processo Markoviano che evolve nel tempo per effetto delle misure acquisite. In [PAT05], i sensori sono integrati in unostrumento portabile per il monitoraggio dei parametri vitali di una persona. Per limitare la perdita di energia, si applica una strategia adattiva di campionamentoche traccia i parametri nel tempo rispetto a un Markov Decision Process. Nessuno di questi modelli adotta distribuzioni non-Markoviane, il che impedisce dirappresentare tempificazioni a supporto finito e di verificare requisiti real-time e meccanismi di comunicazione e tolleranza ai guasti.

[DGM05] A. Deshpande, C.Guestrin, S.R.Madden, J.M.Hellerstein, W.Hong. Model-based approximate querying in sensor networks. Int. J. on Very Large DataBases, vol. 14(4), 417-443, 2005.[PAT05] A. Panangadan, S. M. Ali, A. Talukder. Markov decision processes for control of a sensor network-based health monitoring system. Conf. InnovativeApplications of Artificial Intelligence IAAI, 2005.

1.4 Processo di sviluppo di SW real-time

Vari lavori riguardano l'applicazione di metodi formali allo sviluppo di SW real-time. In [FPY02,FKP07], il modello dei Timed Automata è impiegato a supportodello sviluppo di sistemi preemptive nell'ipotesi che il sistema non includa sia tempi di esecuzione non-deterministici sia dipendenze fra tempi di rilascio ecompletamento dei task. In [CRV], la teoria delle preemptive Time Petri Nets è integrata in un framework che supporta la specifica e l'implementazione di SWpreemptive real-time, la ricostruzione dei tempi di esecuzione e il testing real-time. Questi approcci affrontano il tema nella prospettiva della verifica di correttezza enon supportano la valutazione di misure di prestazione.

[CRV] L. Carnevali, L. Ridi, E. Vicario. Putting preemptive Time Petri Nets to work in a V-Model SW life cycle. Accepted for publication in IEEE Tr. on SW Eng.[FKP07] E. Fersman, P. Krcal, P. Pettersson, W. Yi. Task automata: Schedulability, decidability and undecidability. Inf. Comput., 205(8):1149-1172, 2007.[FPY02] E. Fersman and P. Pettersson, W. Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. TACAS'02, vol. 2280 of LNCS, 2002.

1.5 Diffusione di modelli organizzativi di business

10

La modellazione formale della diffusione di modelli organizzativi di business è stata studiata solo molto recentemente. Il lavori hanno considerato il modelloorganizzativo aperto [CVW06] e hanno applicato l'approccio mean field per descriverne la diffusione [PMG10].

[CVW06] H. Chesbrough, W. Vanhaverbeke, J. West, eds. Open Innovation: Researching a New Paradigm, Oxford University Press, 2006, Oxford.[PMG10] P. Pisano, D. Manini, M. Gribaudo, M. Pironti. Open Organization Model Diffusion : The Mean Field Analysis Approach. 6th European Conf. onManagement Leadership and Governance, 2010.

2 Direzioni di ricerca

2.1 Analisi di modelli Non-Markoviani attraverso approssimazione Markoviana

Le distribuzioni Phase Type (PH) introdotte in [N75] sono ampiamente utilizzate per la loro capacità di approssimare timer non-Markoviani con modelli Markoviani.Le distribuzioni Matrix Exponential (ME), che non hanno necessariamente un'interpretazione Markoviana [BN03], sono un sovrainsieme delle distribuzioni PH. Sonostate sviluppate tecniche di espansione capaci di trattare modelli con timer appartenenti ad entrambe le famiglie di distribuzioni [BS98]. I processi corrispondentialle distribuzioni PH e ME sono i Markovian Arrival Processes (MAP) [N79] e i Matrix Exponential Arrival Processes (MEP) [L08], entrambi capaci di catturaretraffico correlato e burst. Recenti sviluppi sullo studio delle caratteristiche di MAP e MEP sono descritti in [BHT08], senza tuttavia identificare procedure di fittingefficienti.

Uno dei primi tentativi per mitigare il problema dell'esplosione dello spazio degli stati di MAP e MEP è stato proposto in [BS98], descrivendo il grafo diraggiungibilità in modo simbolico sulla base delle matrici delle distribuzioni PH. Sebbene i risultati ottenuti siano incoraggianti, la memorizzazione del grafocontinua a costituire un collo di bottiglia. Tecniche simboliche basate sull'algebra di Kronecker sono state utilizzate in [CLS01] per la generazione e larappresentazione del grafo di raggiungibilità per sistemi asincroni. Più recentemente [M04] il formalismo dei Multi-Terminal Multi-Valued Decision Diagrams èutilizzato per rappresentare l'insieme dei task attivi ma non abilitati in ogni stato del sistema.

[BHT08] L. Bodrog, A. Horvath, M. Telek. Moment characterization of matrix exponential and Markovian arrival processes. Annals of Operations Research,160:51-68, 2008.[BN03] Bladt, M., Neuts, M. Matrix-exponential distributions: calculus and interpretations via flows. Stochastic Models, 19(1), 113-124, 2003.[BS98] A. Bobbio, M. Scarpa. Kronecker representation of stochastic petri nets with discrete PH distributions. Third IEEE Ann. Int'l Computer Performance andDependability Symp., 1998.[CLS01] G. Ciardo, G. Luttgen, R. Siminiceanu. Saturation: an efficient iteration strategy for symbolic state space generation. TACAS'01, vol. 2031 of LNCS, 2001.[L08] L. Lipsky. Queueing Theory: A Linear Algebraic Approach. Springer, 2008[M04] A. S. Miner. Symbolic representations and analysis of large probabilistic systems. In Validation of Stochastic Systems, 296-338. Springer, 2004.[N75] M. Neuts, Probability distributions of phase type, in: Liber Amicorum Prof. Emeritus H. Florin, University of Louvain, 173-206, 1975.[N79] Neuts, M. A versatile Markovian point process. J. of Applied Probability, 16, 764-779, 1979.

2.2 Analisi approssimata di modelli non-Markoviani

Un approccio per analizzare sistemi di grandi dimensioni è quello di applicare tecniche asintotiche che forniscono risultati accurati se applicate a modelli compostida molti sottomodelli simili. Una di queste tecniche, l'analisi mean-field presentata in [K70], ha recentemente guadagnato interesse nell'ambito della performanceevaluation [BGT08]. Una tecnica simile è stata sviluppata per l'analisi dei colli di bottiglia nelle reti di code [BS97].

Un altro approccio per modellare sistemi complessi di questo tipo è la decomposizione gerarchica. I modelli associati con i sottosistemi sono risolti iterativamente[TT91], e il teorema del punto fisso di Brouwer [OR70] può essere utilizzato per dimostrare l'esistenza di una soluzione. In [GTN10] è proposto un approcciogenerale, analitico e model-based per l'analisi di performability end-to-end di servizi cloud, che genera un modello trattabile e scalabile rimanendo al contempomolto accurato.

Questi due approcci, sviluppati per modelli Markoviani, costituiranno la base per tecniche asintotiche per modelli non-Markoviani di grandi dimensioni.

La valutazione di prestazioni e affidabilità di sistemi real-time con preemption è affrontata in vari lavori sotto l'assunzione di un modello discreto del tempo. Approccianalitici basati su un'astrazione continua sono stati proposti in [BT97] per modelli con timer esponenziali e deterministici, utilizzando la Markov Renewal Theorysotto la cosiddetta enabling restriction, che impedisce l'abilitazione concorrente di più di una transizione non-memoryless. [BPT00] estende l'approccio perconsentire l'utilizzo combinato di diverse politiche di preemption. Una ulteriore estensione che rilassa il limite dell'enabling restriction ed accetta qualsiasidistribuzione è stata implementata nel tool WebSPN [HPS00] con un'approssimazione discreta. In [BSV05] una variante delle time Petri Nets a tempo discretoutilizza una semantica di concorrenza maximal step per rappresentare il comportamento preemptive e associare probabilità a tempificazioni e scelte.

[BPT00] A. Bobbio, A. Puliafito, M. Telek. A Modelling Framework to implement preemption policies in non-Markovian SPNs. IEEE Tr. on SW Eng., 26(1), January2000.[BGT08] A. Bobbio, M.Gribaudo, M.Telek. Analysis of large scale interacting systems by mean field method. In QEST'08, St Malo, France, September 14-17, 2008[BS97] Balbo G., Serazzi G., Asymptotic Analysis of multiclass closed queueing networks: Multiple Bottlenecks, Perf. Eval., vol.30, n.3,115-152, 1997.[BSV05] G. Bucci, L. Sassoli, E. Vicario. Correctness verification and performance analysis of real time systems using stochastic preemptive Time Petri Nets. IEEETr. on SW Eng., 31(11):913-927, 2005.[BT97] A. Bobbio, M. Telek. Transient Analysis of a Preemptive Resume M/D/1/2/2 through Petri Nets, Periodica Politechnica, 41:123-146, 1997.[GTN10] R. Ghosh, K. Trivedi, V. Naik, D.S. Kim. End-to-End Performability Analysis for Infrastructure-as-a-Service Cloud: An Interacting Stochastic ModelsApproach. The 16th IEEE Pacific Rim Int. Symposium on Dependable Computing (PRDC'10), 2010.[HPS00] A. Horvath, A. Puliafito, M. Scarpa, M. Telek. Analysis and Evaluation of Non-Markovian Stochastic Petri Nets. TOOLS'00, vol. 1786 of LNCS, 2000.[K70] Thomas G. Kurtz, Solutions of Ordinary Differential Equations as Limits of Pure Jump Markov Processes ,J. of Applied Probability.Vol.: 7(1), 49-58,1970.[OR70] J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables. Academic Press, NY, 1970.[TT91] L. Tomek, K. Trivedi, Fixed-point iteration in availability modeling, in Informatik-fachberichte, Vol. 91: Fehlertolerierende Rechensysteme. 1991.

2.3 Model checking

Il model checking è un metodo di verifica per controllare che un modello formale del sistema soddisfi una specifica formale delle sue proprietà di correttezza. Lacomplessità computazionale del model checking dipende dalla logica, dal tipo di processo stocastico e dalla dimensione dello spazio degli stati. La verifica di formuledi Continuous Stochastic Logic su catene di Markov a tempo continuo (CTMC) si riduce all'analisi transitoria e/o a regime della CTMC e può quindi essere condottain modo efficiente [BHH03] anche per spazi degli stati relativamente grandi. Per CSL-TA [DHS09], un'estensione di CSL in cui le formule sono definite attraverso unTimed Automata (TA), la verifica può richiedere la soluzione di un Markov Regenerative Process. Il model checking su modelli non-Markoviani a tempo continuo èstato affrontato in [BBB08] per un one-clock TA, dove l'assunzione one-clock garantisce che il modello appartenga ai semi-Markov process [G89], per i quali lasimulazione è spesso l'unico approccio percorribile. Gli approcci basati su simulazione conducono al model checking statistico [YKP06,SVA05], che può essereconvenientemente utilizzato anche per trattare processi semplici (come CTMC) ma con un grande numero di stati.

I sistemi di grandi dimensioni possono essere trattati attraverso tecniche di astrazione; l'approccio di sostituire le scelte probabilistiche del sistema con scelte nondeterministiche [KNS00] è stato utilizzato per sistemi non-Markoviani in [ACD91]. Un'ulteriore soluzione è fornita anche dalle tecniche composizionali, proposte inletteratura per supportare sia l'analisi di sistemi non-deterministici [DL09] che quella di sistemi probabilistici [KNP10]; tali approcci analizzano i sistemi sottol'assunzione che il loro ambiente soddisfi specifiche proprietà.

11

[ACD91] R. Alur, C. Courcoubetis, D. L. Dill. Model-Checking for Probabilistic Real-Time Systems. ICALP'91, vol. 510 of LNCS, 1991.[BBB08] N. Bertrand, P. Bouyer, T. Brihaye, N. Markey. Quantitative model-checking of one-clock timed automata under probabilistic semantics. Int. Conf. onQuant. Eval. of Systems (QEST), 2008.[BHH03] C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen. Model-checking algorithms for Continuous-Time Markov Chains. IEEE Tr. on SW Eng., vol. 29, no. 6,2003.[DHS09] Donatelli S, Haddad S, Sproston J. Model checking timed and stochastic properties with CSLTA . IEEE Tr. on SW Eng. 2009; 35(2):224-240,[DL09] L. D'Errico, M. Loreti. Assume-Guarantee Verification of Concurrent Systems. COORDINATION 2009, vol. 5521 of LNCS, 2009.[G89] P. W. Glynn. A GSMP formalism for discrete-event systems. Proc. of the IEEE, vol. 77, 1989.[KNP10] M. Kwiatkowska, G. Norman, D. Parker, H. Qu. Assume-Guarantee Verification for Probabilistic Systems. TACAS'10, LNCS 6015, 2010.[KNS00] M. Kwiatkowska, G. Norman, R. Segala, J. Sproston. Verifying Quantitative Properties of Continuous Probabilistic Timed Automata. CONCUR '00, LNCS1877, 2000.[SVA05] K. Sen, M. Viswanathan, G. Agha. On statistical model checking of stochastic systems. CAV'05, vol 3576 of LNCS, 2005.[YKP06] G. N. H. Younes, M. Kwiatkowska, D. Parker. Numerical vs. statistical probabilistic model checking. Int. J. on SW Tools for Technology Transfer,8(3):216-228, 2006.

Inglese

This section has the same structure as the previous one.

1 Application areas

1.1 Cloud computing (CC)

Assessing QoS and performance in CC is a problem of strategic importance, and several techniques to address this problem have been proposed. For example, [Y09]developed a framework to analyze the resource acquisition and release times in Amazon EC2 subjected to various workloads. [VBV09] studies the effect of virtualmachine live migration on SLAs. Reliability aspects are instead considered in [DY09]. [Ya09] showed how execution time is increased when subtasks of a workloadfail. [BPA09] describes the design of a reliable and cost-effective storage system with high availability despite failures of the servers.

[BPA09] N. Bonvin, T. G. Papaioannou, K. Aberer. Dynamic cost efficient replications in data clouds, in ACDC, 2009[DY09] Y. S. Dai, B. Yang, J. Dongarra, G. Zhang. Cloud service reliability: Modeling and analysis, in PRDC, 2009.[VBV09] W. Voorsluys, J. Broberg, S. Venugopal, R. Buyya. Cost of virtual machine live migration in clouds: A performance evaluation, in CloudComp, 2009.[Y09] N. Yigitbasi et al. C-meter: A framework for performance analysis of computing clouds, in Cloud, 2009.[Ya09] B. Yang et al. Performance evaluation of cloud service considering fault recovery, in CloudComp, 2009.

1.2 Wireless sensor networks (WSN)

WSN have been studied for about ten years and the first works concentrated on networking aspects (a survey is provided in [AY05]) and on data management [ZG04].Reliability and dependability issues, two crucial aspects in several industrial applications, were considered only more recently [MSP09]. A characterizing feature ofsensors is that they can switch into a sleep mode in which they save energy but cannot communicate. This feature becomes a problem when a sleeping node is involvedin a multi-hop communication thus producing a broken link. Possible solutions are to to apply routing protocols that self-adapt to the environmental changes or todesign the WSN with redundancy [BPS10].

[AY05] K. Akkaya, M. Younis. A survey on routing protocols for wireless sensor networks. Ad Hoc Networks, 3:325-349, 2005.[BPS10] D. Bruneo, A. Puliafito, M. Scarpa. Dependability analysis of Wireless Sensor Networks with active-sleep cycles and redundant nodes. In DYADEM-FTS,2010.[MSP09] S. Mukhopadhyay, C. Schurgers, D. Panigrahi, S. Dey. Model-Based Techniques for Data Reliability in Wireless Sensor Networks. IEEE Tr. on MobileComputing, 8(4):528-543, 2009.[ZG04] F. Zhao, L. Guibas. Wireless sensor networks - An information processing approach. Morgan Kaufmann, 2004.

1.3 Online prediction for distributed monitoring infrastructures

Only a few experiences have been published on this topic. In [DGM05], queries to a network of nodes are approximated by taking into account the state of a model ofthe monitored system, represented as a Markovian process which evolves in time and gets affected by acquired measurements. In [PAT05], sensors are integrated intoa wearable device monitoring vital parameters of a human. To limit energy loss, an adaptive sensing strategy tracing the parameters in real-time together with aMarkov Decision Process is applied. None of these models adopts non-Markovian distributions of timing which limits the expressive power, excluding finite supporttiming and preventing hence the verification of real-time requirements, communication and fault-tolerance mechanisms.

[DGM05] A. Deshpande, C.Guestrin, S.R.Madden, J.M.Hellerstein, W.Hong. Model-based approximate querying in sensor networks. Int. J. on Very Large DataBases, vol. 14(4), 417-443, 2005.[PAT05] A. Panangadan, S. M. Ali, A. Talukder. Markov decision processes for control of a sensor network-based health monitoring system. Proc. Conf. InnovativeApplications of Artificial Intelligence IAAI, 2005.

1.4 Development process of real-time SW

Various works address the application of formal methods to the development of real-time SW. In [FPY02,FKP07], the formal nucleus of Timed Automata supports thedevelopment of preemptive systems under the assumption that the model does not include both non-deterministic execution times and dependencies among release andcompletion times of tasks. In [CRV], the theory of preemptive Time Petri nets is cast into a model driven development framework supporting specification of real-timepreemptive SW, real-time code generation, execution time profiling, and real-time testing. As a notable trait, all these approaches address the issue in the perspectiveof correctness verification and do not support the evaluation of performance.

[CRV] L. Carnevali, L. Ridi, E. Vicario. Putting preemptive Time Petri Nets to work in a V-Model SW life cycle. Accepted for publication in IEEE Trans. on SW Eng.[FKP07] E. Fersman, P. Krcal, P. Pettersson, W. Yi. Task automata: Schedulability, decidability and undecidability. Inf. Comput., 205(8):1149-1172, 2007.[FPY02] E. Fersman and P. Pettersson, W. Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. TACAS'02, vol. 2280 of LNCS, 2002.

1.5 Diffusion of business organization models

Formal modeling of diffusion of business organization models has been considered only very recently. The works considered the open organization model [CVW06]and applied the mean field approach to describe its diffusion [PMG10].

[CVW06] H. Chesbrough, W. Vanhaverbeke, J. West, eds. Open Innovation: Researching a New Paradigm, Oxford University Press, 2006, Oxford.[PMG10] P. Pisano, D. Manini, M. Gribaudo, M. Pironti. Open Organization Model Diffusion : The Mean Field Analysis Approach. 6th European Conf. onManagement Leadership and Governance, 2010.

2 Research directions

2.1 Analysis of Non-Markovian models by Markovianization

12

Phase type (PH) distributions were introduced in [N75] and are widespread used because of their power in approximating non-Markovian durations by Markovianmodels. Matrix exponential (ME) distributions, which do not necessarily have a Markovian interpretation [BN03], provide a superset of PH distributions. For bothfamilies an expansion technique was developed to handle models composed of durations belonging to them [BS98]. The process counterpart of the PH and MEdistributions are Markovian arrival processes (MAP) [N79] and matrix exponential arrival processes (MEP) [L08] and they have the important property of beingable to capture correlated, bursty traffic. Recent advances on characteristics of MAPs and MEPs are provided in [BHT08] but have not been transformed yet inefficient fitting procedures.

The expansion technique developed for PH and ME distributions often results in models with huge state space. One of the first attempts to alleviate this problem hasbeen done in [BS98] where the expanded reachability graph is symbolically described based on the matrices representing the PH distributions. Even if the obtainedresults were encouraging, storing the reachability graph remains a bottleneck. The problem of managing huge state spaces is not new and it has been faced in[CLS01] by exploiting Kronecker algebra-based symbolic techniques for the generation and the representation of the reachability graph of asynchronous systems.More recently [M04] multi-terminal multi-valued decision diagrams are used to represent the set of active but non-enabled tasks for all the system states.

[BHT08] L. Bodrog, A. Horvath, M. Telek. Moment characterization of matrix exponential and Markovian arrival processes. Annals of Operations Research,160:51-68, 2008.[BN03] Bladt, M., Neuts, M. Matrix-exponential distributions: calculus and interpretations via flows. Stochastic Models, 19(1), 113-124, 2003.[BS98] A. Bobbio, M. Scarpa. Kronecker representation of stochastic petri nets with discrete PH distributions. Third IEEE Ann. Int'l Computer Performance andDependability Symp., 1998.[CLS01] G. Ciardo, G. Luttgen, R. Siminiceanu. Saturation: an efficient iteration strategy for symbolic state space generation. TACAS'01, vol. 2031 of LNCS, 2001.[L08] L. Lipsky. Queueing Theory: A Linear Algebraic Approach. Springer, 2008[M04] A. S. Miner. Symbolic representations and analysis of large probabilistic systems. In Validation of Stochastic Systems, 296-338. Springer, 2004.[N75] M. Neuts, Probability distributions of phase type, in: Liber Amicorum Prof. Emeritus H. Florin, University of Louvain, 173-206, 1975.[N79] M. Neuts. A versatile Markovian point process. J. of Applied Probability, 16, 764-779, 1979.

2.2 Approximate analysis of non-Markovian models

One approach to analyze large scale systems is to apply asymptotic techniques that provide accurate results when applied to models composed of many similarsubmodels. Mean-field analysis, presented in [K70], is one such technique and it gained interest in performance evaluation recently [BGT08]. A similar technique hasbeen developed for bottleneck analysis in queuing networks [BS97].

Another approach to model complex systems composed of nearly independent subsystems is hierarchical decomposition. The models associated with the subsystemsare solved iteratively [TT91]. Brouwer's fixed point theorem [OR70] can be used to prove the existence of a solution. In [GTN10], a general, analytic and modelbased approach is proposed for end-to-end performability analysis of cloud service. In contrast to a single one-level monolithic model, the approach yields a tractableand scalable model and remains also highly accurate.

The above two approaches, developed for Markovian models, will be the basis of asymptotic techniques for large scale non-Markovian models.

With regards to real-time preemptive systems, the evaluation of performance and dependability is addressed in various works under the assumption of a discretemodel of time. Analytical approaches based on a continuous abstraction of time was proposed in [BT97] for models with exponential and deterministic timers usingMarkov renewal theory under the so-called enabling restriction that rules out concurrent enabling of multiple non memoryless transitions. In [BPT00], the approachis extended to manage a combined use of different preemption polices. A wider extension that relaxes both the enabling restriction limit and accepts any kind ofdistributions was implemented in the WebSPN tool [HPS00] through a discrete approximation. In [BSV05], a discrete-time variant of time Petri nets leverages amaximal step semantics of concurrency to support the representation of preemptive behavior and associate quantitative probabilities with timers and switches.

[BPT00] A. Bobbio, A. Puliafito, M. Telek. A Modelling Framework to implement preemption policies in non-Markovian SPNs. IEEE Tr. on SW Eng., 26(1), January2000.[BGT08] A. Bobbio, M.Gribaudo, M.Telek. Analysis of large scale interacting systems by mean field method. In Proc. of QEST'08, St Malo, France, September 14-17,2008[BS97] Balbo G., Serazzi G., Asymptotic Analysis of multiclass closed queueing networks: Multiple Bottlenecks, Perform. Eval., vol.30, n.3, pp.115-152, 1997. z[BSV05] G. Bucci, L. Sassoli, E. Vicario. Correctness verification and performance analysis of real time systems using stochastic preemptive Time Petri Nets. IEEETr. on SW Eng., 31(11):913-927, November 2005.[BT97] A. Bobbio, M. Telek. Transient Analysis of a Preemptive Resume M/D/1/2/2 through Petri Nets, Periodica Politechnica, 41:123-146, 1997.[GTN10] R. Ghosh, K. Trivedi, V. Naik, D.S. Kim. End-to-End Performability Analysis for Infrastructure-as-a-Service Cloud: An Interacting Stochastic ModelsApproach. The 16th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC'10), 2010.[HPS00] A. Horvath, A. Puliafito, M. Scarpa, M. Telek. Analysis and Evaluation of Non-Markovian Stochastic Petri Nets. TOOLS'00, vol. 1786 of LNCS, 2000.[K70] Thomas G. Kurtz, Solutions of Ordinary Differential Equations as Limits of Pure Jump Markov Processes ,J. of Applied Probability (1970) Volume: 7, Issue: 1,pp.49-58[OR70] J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables. Academic Press, NY, 1970.[TT91] L. Tomek, K. Trivedi, Fixed-point iteration in availability modeling, in Informatik-fachberichte, Vol. 91: Fehlertolerierende Rechensysteme. 1991.

2.3 Model checking

Model checking is a verification method for checking automatically that a formal model of the system satisfies a formal specification of its correctness properties. Thecomputational complexity of model checking depends on the logic, on the type of the stochastic process under study and on the size of the state space. Verifyingformulas of continuous stochastic logic (CSL) against continuous time Markov chains (CTMC) boils down to transient and/or steady state analysis of CTMCs andhence can be carried out in an efficient manner [BHH03] even for relatively large state spaces. For CSL-TA [DHS09], an extension of CSL, referring still to CTMCsbut where formulas are defined through a control timed automata (TA), the verification can require the solution of a Markov regenerative process. Model checkingover continuous time non-Markovian models was addressed in [BBB08] for one-clock TA where the one-clock assumption guarantees that the underlying model is asemi-Markov Process. If there are more clocks, we have a generalized semi-Markov process [G89], for which simulation is often advocated as the only viableapproach. The simulation based approach leads to statistical model checking [YKP06,SVA05]. Also in case of a simple underlying process (like CTMCs) but withhuge state spaces, statistical model checking can be carried out.

Large-scale systems can be handled by abstractions and one approach is to replace probabilistic choices of the system with non deterministic choices [KNS00] whichwas adopted for non-Markovian systems in [ACD91]. Also compositional approaches can alleviate the state space explosion problem. Such techniques have beenproposed in literature to support analysis of non-deterministic [DL09] and also probabilistic [KNP10] systems. Using these approaches a system is not analyzed inisolation but under the assumptions that its environment satisfies specific properties.

[ACD91] R. Alur, C. Courcoubetis, D. L. Dill. Model-Checking for Probabilistic Real-Time Systems. ICALP'91, vol. 510 of LNCS, 1991.[BBB08] N. Bertrand, P. Bouyer, T. Brihaye, N. Markey. Quantitative model-checking of one-clock timed automata under probabilistic semantics. Proc. Int. Conf. onQuant. Eval. of Systems (QEST), 2008.[BHH03] C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen. Model-checking algorithms for Continuous-Time Markov Chains. IEEE Tr. on SW Eng., vol. 29, no. 6,2003.[DHS09] Donatelli S, Haddad S, Sproston J. Model checking timed and stochastic properties with CSLTA . IEEE Tr. on SW Eng. 2009; 35(2):224-240,[DL09] L. D'Errico, M. Loreti. Assume-Guarantee Verification of Concurrent Systems. COORDINATION 2009, vol. 5521 of LNCS, 2009.[G89] P. W. Glynn. A GSMP formalism for discrete-event systems. Proc. of the IEEE, vol. 77, 1989.

13

[KNP10] M. Kwiatkowska, G. Norman, D. Parker, H. Qu. Assume-Guarantee Verification for Probabilistic Systems. TACAS'10, vol. 6015 of LNCS, 2010.[KNS00] M. Kwiatkowska, G. Norman, R. Segala, J. Sproston. Verifying Quantitative Properties of Continuous Probabilistic Timed Automata. CONCUR '00, vol.1877 LNCS, 2000.[SVA05] K. Sen, M. Viswanathan, G. Agha. On statistical model checking of stochastic systems. CAV'05, vol 3576 of LNCS, 2005.[YKP06] G. N. H. Younes, M. Kwiatkowska, D. Parker. Numerical vs. statistical probabilistic model checking. Int. J. on SW Tools for Technology Transfer,8(3):216--228, June 2006.

12 - Ruolo di ciascuna unità operativa in funzione degli obiettivi previsti e relative modalità diintegrazione e collaborazioneItaliano

1 Breve descrizione delle unità di ricerca

Università di Torino (UTo): L'unità è composta da membri di due gruppi di ricerca del dipartimento di Informatica. Il primo, il gruppo di Performance Evaluationand System Validation (PESV), ha avuto un ruolo prevalente nello sviluppo delle reti di Petri stocastiche, e da allora ha consolidato la propria esperienza da aspettiteorici dei processi stocastici e dei metodi formali a problemi pratici di modellazione. Il secondo, il gruppo di Management of Innovation, mira ad estendere l'uso dimetodi formali nella modellazione degli aspetti organizzativi di imprese di business.

Università di Firenze (UFi): L'unità è composta da membri del dipartimento di Sistemi e Informatica e combina competenze nelle aree dell'Informatica edell'Ingegneria Informatica. La principale competenza dell'unità si colloca nelle aree delle tecniche di model checking per algebre di processo stocastiche, analisi evalutazione simbolica di processi non-Markoviani, e applicazione di metodi formali allo sviluppo di sistemi concorrenti real-time.

Università di Messina (UMe): L'unità è composta da membri del Laboratorio di Mobile and Distributed System, che include ricercatori sia del settoredell'Informatica sia dell'Ingegneria Informatica. La ricerca è focalizzata sui sistemi distribuiti con particolare riguardo per i sistemi wireless, computazioni grid ecloud, modellazione e valutazione di prestazioni e affidabilità, e sistemi multimediali. Il gruppo ha esperienza nell'ambito di tecniche innovative applicabiliti a sistemiin larga scala.

Politecnico di Milano (PMi): L'unità è composta da membri del dipartimento di Elettronica e Informatica con competenze sia nell'ambito dell'Informatica siadell'Ingegneria Informatica. Il gruppo ha interesse nella modellazione di sistemi di code con speciale attenzione per l'analisi di colli di bottiglia e nell'uso diapprossimazioni fluide nella valutazione di prestazioni.

2 Struttura dei Work package

La ricerca è organizzata in work package (WP) e task secondo la seguente struttura (le unità responsabili sono indicate fra parentesi):

WP1 (UMe): Aree di applicazioneT1.1 Cloud computing (UMe)T1.2 Wireless sensor networks (UMe)T1.3 Predizione dinamica per infrastrutture di monitoraggio distribuito (UFi)T1.4 Processo di sviluppo di SW real-time (UFi)T1.5 Diffusione di modelli organizzativi di business (UTo)

WP2 (UTo): Analisi di modelli non-Markoviani attraverso MarkovianizzazioneT2.1 Approssimazione di distribuzioni (UTo)T2.2 Caratterizzazione del traffico (PMi)T2.3 Rappresentazione simbolica dello spazio degli stati (UMe)T2.4 Modelli con distribuzioni matrix exponential (UTo)

WP3 (PMi): Analisi approssimata di modelli non-MarkovianiT3.1 Tecniche asintotiche (PMi)T3.2 Iterazioni di punto fisso con distribuzioni (UMe)T3.3 Soluzioni di modelli con scheduling preemptive (UFi)

WP4 (UFi): Model checkingT4.1 Model checking di processi rigenerativi Markoviani (UFi)T4.2 Logica temporale stocastica unificata (UTo)T4.3 Model checking attraverso astrazioni (UTo)T4.4 Model checking statistico (UFi)T4.5 Specifica ed analisi composizionale di modelli (UFi)

3 Descrizione dei task e delle loro relazioni, del ruolo e della cooperazione delle unità

La maggior parte dei task applicativi prende avvio con lo studio dello stato dell'arte, dal momento che tali aree di applicazione, che rappresentano problemi crucialiin settori strategici (home-land security, sistemi di assistenza sanitaria, conservazione dell'energia e produttività in generale), ricevono una sempre maggioreattenzione.

T1.1 Cloud computing (UMe)

Una fase preliminare, portata avanti prevalentemente da UMe, riguarderà l'analisi dello stato dell'arte sui temi delle prestazioni e della disponibilità di applicazionicloud (CC). Parallelamente sarà avviata la raccolta di distribuzioni che descrivono tempificazioni tipiche di applicazioni cloud, che costituisce un input per T2.1 eT2.2, e sarà quindi condotta in cooperazione con UTo e PMi. In questa fase UMe definirà anche metriche e benchmark per applicazioni cloud. Sulla base di questeattività iniziali, saranno sviluppati modelli analitici di sistemi cloud e le tecnique sviluppate nel progetto saranno applicate alla loro analisi. Questa fase sarà portataavanti in cooperazione con tutti i task che si propongono di fornire tecniche di analisi, cioè l'intero WP2 (UTo,UMe,PMi), T3.1(PMi), T3.2(UMe) T4.4(UFi). Irisultati dell'analisi saranno impiegati per la progettazione di sistemi cloud (UMe).

T1.2 Wireless sensor networks (UMe)

Le fasi iniziali sono le stesse di T1.1. Sarà svolta un'analisi dello stato dell'arte su prestazioni e disponibilità in sensor network (UMe). Saranno raccolte distribuzionie pattern di traffico associati a WSN, che costituiscono un input per T2.1 (UTo) e T2.2 (UMe). Saranno definiti benchmark e metriche da UMe. Successivamente,UMe elaborerà modelli WSN riguardanti questi tre aspetti cruciali: (1) tecniche di risparmio energetico; (2) gestione della ridondanza; (3) valutazione della rete edella topoogia. Tali modelli coprono una vasta gamma di situazioni e si prevede che quasi tutti i task in WP2, WP3, e WP4 alla loro analisi, i cui risultati sarannosfruttati da UMe per la progettazione di WSN nelle fasi finali di T1.2.

14

T1.3 Predizione dinamica per infrastrutture di monitoraggio distribuito (UFi)

Le fasi iniziali saranno portate avanti da UFi. Anche questo task prenderà avvio con lo studio dello stato dell'arte. UFi definirà quindi uno specifico scenarioapplicativo, identificherà i criteri che l'infrastruttura di monitoraggio deve soddisfare, e progetterà e metterà in opera un ambiente di prova. Questo ultimo passosarà portato avanti in cooperazione con le altre unità allo scopo di identificare e integrare le tecniche più promettenti ai fini applicativi che saranno sviluppatenell'ambito di WP4 (UFi,UTo).

T1.4 Processo di sviluppo di SW real-time (UFi)

L'organizzazione del task è simile a quella di T1.3. I passi iniziali saranno portati avanti da UFi. Sarà studiato lo stato dell'arte, sarà delineato uno specificoscenario di sviluppo di SW real-time, saranno definiti i criteri che il sistema deve soddisfare e sarà creato un ambiente di prova. I passi rimanenti saranno dedicatiall'identificatione e all'integrazione di tool di analisi. I task T2.1(UTo), T3.2(UMe), T3.3(UFi), T4.1(UFi) e T4.4(UFi) contribuiranno all'analisi di sistemi preemptivereal-time.

T1.5 Diffusione di modelli organizzativi di business (UTo)

Il task prenderà avvio con l'identification delle industrie da analizzare. Sarà quindi caratterizzato il ruolo delle compagnie all'interno delle industrie in un arco ditempo, in termini di modello organizzativo e focus strategico, attraverso tool di analisi dei contenuti basati sui bilanci e sulle lettere inviate agli azionisti. Sulla basedei dati raccolti, saranno creati modelli che descrivono il comportamento temporale delle singole società considerando le dipendenze con le altre società. Fino a quiil task sarà portato avanti da UTo. L'ultima fase sarà dedicata ad analizzare il modello con tecniche sviluppate nel progetto. E' difficile prevedere con certezza qualitecniche saranno appropriate dato che l'area di applicazione è nuova. Con molta probabilità saranno impiegate le tecniche sviluppate in T3.1(PMi) e T4.5(UFi).

Nel seguito saranno descritti i task non specificamente orientati all'applicazione, omettendo di menzionare le aree in cui le tecniche proposte troverannoapplicazione.

T2.1 Approssimazione di distribuzioni (UTo)

Come già menzionato, il task T2.1 riceverà un insieme di distribuzioni dai passi preliminari dei task T1.1 e T1.2. Tali distribuzioni insieme a quelle usate nellamodellazione di affidabilità e a quelle risultanti dal task T3.2 di UMe (descritto nel seguito) costituiranno un benchmark per l'approssimazione di distribuzioni, chesarà usato da UTo per valutare le tecniche esistenti. In una fase successiva, realizzata da UTo, sarà definita la variante tempo-discreto delle distribuzini matrixexponential e saranno rielaborate nel dominio del tempo discreto le tecniche di approssimazione tempo-continuo più promettenti. Sia UTo sia UFi hanno esperienzanell'ambito delle tecniche di approssimazione basate su famiglie di polinomi e insieme considereranno famiglie di polinomi non ancora sperimentate. I risultati diquesto task sono tecniche che possono risolvere sotto-problemi di altri task, in particolare: T2.3(UMe),T2.4(UTo),T3.2(UMe),T3.3(UFi) e T4.1(UFi).

T2.2 Caratterizzazione del traffico (PMi)

Questo task studierà e caratterizzerà il traffico generato da applicazioni web complesse (come social network e altri servizi web 2.0) e da applicazioni cloud. Sarannosviluppati dei tool per la raccolta delle tracce del traffico e saranno usati durante tutto il progetto per raccogliere pattern statisticamente significativi. Sarannovalutate le tecniche esistenti e, se necessario, ne saranno sviluppate di nuove per costruire processi di arrivo che siano in grado di riprodurre i pattern osservati. Ilproblema è simile a quello affrontato nel task T2.1 and quindi si prevede una cooperazione continua fra PMi e UTo.

T2.3 Rappresentazione simbolica dello spazio degli stati(UMe)

I primi tre passi di questo task saranno portati avanti da UMe: (1) studio di multi-terminal multi-valued decision diagrams per la memorizzazione del grafo diraggiungibilità annotato; (2) sviluppo di tecniche di generazione dello spazio degli stati basate su saturazione; (3) implementazione delle tecniche sviluppate in (1) e(2). La parte restante dell'attività sarà dedicata a confronti con altre tecniche risultanti dai task T3.1(PMi), T3.2(UMe) e T3.3(UFi). Gli elementi caratterizzanti deimodelli considerati in questo task sono le distribuzioni phase type. Conseguentemente, ci sarà una continua connessione con il task T2.1(UTo).

T2.4 Modelli con distribuzioni matrix exponential (UTo)

Nella prima fase, UTo valuterà l'uso di solutori basati su equazioni differenziali general purpose e sistemi lineari per analizzare modelli con tempificazioni matrixexponential. La seconda fase è dedicata allo sviluppo di solutori ad-hoc che sfruttino le caratteristiche delle distribuzioni matrix exponential. Nella terza fase, saràsviluppata una variante tempo-discreto delle tecniche di espansione usate per trattare modelli con tempificazioni ME. Sarà pertanto impiegata la variantetempo-discreto delle distribuzioni ME sviluppata nel task T2.1. Dal momento che anche la tecnica di espansione sulla quale si basa task T2.3 può essere applicata amodelli con tempificazioni ME, si prevede una continua collaborazione con il task T2.3(UMe).

T3.1 Tecniche asintotiche (PMi)

Questo task sarà dedicato alle tecniche asintotiche di analisi mean-field e di analisi dei colli di bottiglia per modelli non-Markoviani di grandi dimensioni, il cuistudio sarà condotto in parallelo. La tecnica di analisi mean-field sarà estesa per consentire al calcolo di quantità continue nello spazio degli stati degli oggetti checompongono il sistema. La ricerca sull'analisi dei colli di bottiglia investigherà il modo in cui misure facilmente calcolabili, come la potenza del sistema, possanoessere utilizzate per definire migliori algoritmi di distribuzione del carico in sistemi complessi. I metodi risultanti saranno implementati e comparati con altretecniche approssimate.

T3.2 Iterazioni di punto fisso con distribuzioni (UMe)

UMe svilupperà un algoritmo di punto fisso per la soluzione a regime di modelli non-Markoviani composti da sottosistemi quasi indipendenti, utilizzando le tecnichedi approssimazione per distribuzioni sviluppate e testate in T2.1 (UTo); studierà poi le caratteristiche di convergenza di tale algoritmo, e lo estenderà all'analisitransiente. L'ultima fase sarà dedicata alla comparazione con altre tecniche sviluppate nei task T2.3(UMe), T2.4(UTo) e T3.1(PMi).

T3.3 Soluzioni di modelli con scheduling preemptive (UFi)

Questo task sarà sviluppato prevalentemente da UFi, che definirà una semantica formale che estende le classi di stato stocastiche per includere sistemi conpreemption. Saranno caratterizzate tecniche di analisi esatta e identificate le complessità derivanti dalla presenza di meccanismi di preemption. Per ridurre lacomplessità saranno sviluppate adeguate approssimazioni sul supporto dei timer e sulla forma analitica delle distribuzioni, utilizzando tecniche sviluppate in T2.1(UTo). Sarà infine implementato un prototipo per comparare l'algoritmo rispetto alle tecniche sviluppate nei task T2.3(UMe) e T4.4(UFi).

T4.1 Model checking di processi rigenerativi Markoviani (UFi)

La prima fase di questo task sarà sviluppata da UFi e UTo e condurrà alla definizione di un algoritmo di model checking probabilistico basato sulle classi di statostocastiche. La seconda fase (UTo,UFi) raffinerà l'algoritmo in modo che possa utilizzare i punti di rigenerazione del modello, grazie all'uso di una tecnica diderivazione dei kernel locale e globale del modello basata sulle formule da verificare. UFi implementerà un prototipo per la comparazione con altre tecnicherisultanti dai task T2.3(UMe), T4.3(UTo) e T4.4(UTo).

15

T4.2 Logica temporale stocastica unificata (UTo)

Questo task è condotto principalmente da UTo. La prima fase sarà dedicata alla classificazione dei linguaggi di logica temporale stocastica esistenti e allacomparazione della loro espressività rispetto a CSL-TA. Nella seconda fase sarà implementato un algoritmo efficiente di model checking per CSL-TA, che verràintegrato nel tool MC4CSLTA. Le prestazioni del tool saranno studiate sia teoricamente che sperimentalmente e comparate a quelle delle tecniche sviluppate nel taskT4.4 (UFi).

T4.3 Model checking attraverso astrazioni (UTo)

Il task è condotto principalmente da UTo. La prima fase definirà un algoritmo per la costruzione di modelli astratti di sistemi non-Markoviani nella forma diProbabilistic Timed Automata (PTA). Nella seconda fase sarà studiato come l'output dell'algoritmo della prima fase può essere analizzato dagli strumenti di modelchecking per PTA esistenti. Nella terza fase, saranno identificate e/o sviluppate tecniche di verifica adattate in modo particolare alla verifica dei PTA che risultanocome modelli astratti di sistemi non-Markoviani; tali tecniche saranno poi comparate agli approcci sviluppati nei task T4.1(UFi) e T4.4(UFi).

T4.4 Model checking statistico (UFi)

Il model checking statistico può essere applicato ad un gran numero di sistemi non-Markoviani. UFi definirà una logica temporale per esprimere le proprietà di talisistemi e svilupperà un algoritmo per il model checking statistico della logica definita su sistemi non-Markoviani, lavorando in cooperazione con i membri di UTo chehanno esperienza nella simulazione di modelli non-Markoviani. Sarà poi implementato un prototipo per effettuare comparazioni con i metodi risultanti dai taskT4.1(UFi) e T4.3(UTo).

T4.5 Specifica ed analisi composizionale di modelli (UFi)

Questo task sarà condotto prevalentemente da UFi. Nella prima fase, saranno studiate specifiche e tecniche di analisi composizionali per sistemi tempificati econcorrenti ma non probabilistici. Queste tecniche saranno poi portate sul dominio probabilistico ed applicate a sistemi Markoviani; saranno infine consideratianche modelli non-Markoviani.

Inglese

1 Brief description of the research units

Univ. of Turin (UTo): Composed of members of two research groups of the Comp. Sc. department. The first, the Performance Evaluation and System Validation(PESV) group has had a prevalent role in the development of stochastic Petri nets, and since then has experience ranging from theoretical aspects of stochasticprocesses and formal methods to practical modeling problems. The second, the Management of Innovation group aims at widening the use of formal methods inmodeling organizational aspects of business enterprises.

Univ. of Florence (UFi): Composed of members of the Comp. Sc. department and combines expertise in the areas of computer science and engineering. Mainexpertise of the unit is in the areas of model checking techniques for stochastic process algebras, symbolic analysis and evaluation of non-Markovian processes,application of formal methods in the engineering of real-time concurrent systems.

Univ. of Messina (UMe): Composed of members of the Mobile and Distributed System LABoratory that embraces researchers in both the fields of engineering andcomputer science. The research focus is on distributed systems with particular regards to wireless systems, Grid and Cloud computing, performance and reliabilitymodeling and evaluation, multimedia systems. The group has experience in innovative techniques for the treatment of large-scale models.

Politecnico of Milano (PMi): Composed of members of the department of Electronics and Comp. Sc. with expertise in both computer science and engineering. Thegroup has interest in queuing models with special attention to bottleneck analysis and in the use of fluid approximations in performance evaluation.

2 Work package structure

The research is organized into work packages (WP) and tasks. The structure is as follows (responsible units are indicated in parenthesis):

WP1 (UMe): Application areasT1.1 Cloud computing (UMe)T1.2 Wireless sensor networks (UMe)T1.3 Online prediction for distributed monitoring infrastructures (UFi)T1.4 Development process of real-time SW (UFi)T1.5 Diffusion of business organization models (UTo)

WP2 (UTo): Analysis of non-Markovian models by MarkovianizationT2.1 Distribution approximation (UTo)T2.2 Traffic characterization (PMi)T2.3 Symbolic state space representation (UMe)T2.4 Models with matrix exponential durations (UTo)

WP3 (PMi): Approximate analysis of non-Markovian modelsT3.1 Asymptotic techniques (PMi)T3.2 Fixed point iteration with distributions (UMe)T3.3 Solution of models with preemptive scheduling (UFi)

WP4 (UFi): Model checkingT4.1 Model checking Markov regenerative processes (UFi)T4.2 Unified model checking (UTo)T4.3 Model checking by abstraction (UTo)T4.4 Statistical model checking (UFi)T4.5 Compositional model specification and analysis (UFi)

3 Description of tasks and their relation, role and cooperation of the units

A common trait of most of the application oriented tasks is that they start with the study of the state of the art. This is because these application areas, representingcrucial engineering problems of strategic areas (like home-land security, health care systems, energy conservation and productivity in general), receive muchresearch attention.

T1.1 Cloud computing (UMe)

16

A preliminary phase, carried out by UMe, will be dedicated to gathering the state of the art on performance and availability issues regarding cloud computing (CC).In parallel, we will collect distributions describing typical durations and traffic patterns of CC. This collection will be input for T2.1 and T2.2 and hence will becarried out in cooperation with UTo and PMi. In this phase also metrics and benchmarks of CC will be defined by UMe. Based on these initial activities, analyticalmodels of cloud systems will be designed. Having defined the models, the techniques developed throughout the project will be applied for their analysis. This phasewill be carried out in cooperation with all those tasks that provide techniques for the analysis; these are the whole WP2 (UTo,UMe,PMi),T3.1(PMi),T3.2(UMe) andT4.4(UFi). The results of the analysis will be exploited for the design of CC systems (UMe).


The early phases are identical to those of T1.1. State of the art of wireless sensor networks (WSN) with respect to performance and availability will be studied (UMe).We will collect distributions and traffic patterns associated with WSN which give input to T2.1 (UTo) and T2.2 (UMe). Metrics and benchmarks will be defined byUMe. Subsequently, UMe will design WSN models regarding three crucial aspects: (1) power saving techniques; (2) redundancy management; (3) network andtopology evaluation. The models will cover a wide range of situations and we foresee that almost all tasks in WP2, WP3 and WP4 will contribute in their analysis. Inthe last stages of T1.2, the results of the analysis will be exploited for design issues of WSN by UMe.

T1.3 Online prediction for distributed monitoring infrastructures (UFi)

The early phases will be carried out by UFi. This task as well will be started with the study of the state of the art. Then UFi will define a specific application settingand identify the criteria that the monitoring infrastructure has to satisfy. Afterwards, a test bed environment will be designed and set up by UFi. The last stage will becarried out in cooperation with other units. In this stage, we will first identify and then integrate the techniques that are most promising to adapt well for beingapplied in monitoring infrastructures. Considering the characteristics of monitoring infrastructures, these techniques will be most probably developed in WP4(involving UFi and UTo) where model checking is considered.

T1.4 Development process of real-time SW (UFi)

This task has a similar organization to that of T1.3. Initial stages are carried out by UFi. First, the state of the art will be studied. Then, a specific real time SWdevelopment problem will be set up together with the definition of the criteria that the system has to fulfill. Also a test bed will be created. The remaining stage will bededicated to the identification and integration of analysis tools. The tasks whose results can contribute to the analysis of preemptive real time SW areT2.1(UTo),T3.2(UMe),T3.3(UFi),T4.1(UFi)and T4.4(UFi).

T1.5 Diffusion of business organization models (UTo)

The task will start with identifying the industries to study. Then the companies playing a role in the industries will be characterized, over a period of time, in terms oftheir organization model and strategic focus. The characterization will be carried out by content analysis tools based on the balance sheets of the companies and theletters to the shareholders. Based on the data collected, models will be created that describe the temporal behavior of the individual companies considering alsodependency among other players of the industry. Up to this point the task will be carried out by UTo. The last stage will be dedicated to analyze the model withtechniques developed in the project. Being a novel application area, it is hard to foresee with certainty which techniques will be appropriate. Most probablecandidates are T3.1 (PMi) and T4.5 (UFi) but other tasks will be considered as well.

From now on we describe the non application oriented tasks. We will omit to mention the application areas where the techniques resulting from these tasks are usedbecause they were listed in the description of the application oriented tasks.

T2.1 Distribution approximation (UTo)

As already mentioned, task T2.1 will receive a set of distributions from the early stages of T1.1 and T1.2. These distributions together with distributions used inreliability modeling and distributions coming from task T3.2 of UMe (see later) will form a benchmark for distribution approximation. UTo will use this benchmark toevaluate existing techniques. In a subsequent stage, performed by UTo, we will define the discrete time counterpart of matrix exponential (ME) distributions and bringthe most promising continuous time fitting techniques to discrete time. Both UTo and UFi have experience in fitting techniques based on families of polynomials andtogether will consider families of polynomials that have not been used yet for fitting. The results of this task are techniques that can solve subproblems of other tasks,namely, T2.3(UMe),T2.4(UTo),T3.2(UMe),T3.3(UFi) and T4.1(UFi).

T2.2 Traffic characterization (PMi)

In this task, the traffic generated by complex web applications (such as social networks and other web 2.0 services) and by clouds will be studied and characterized.Tools will be created for the collection of traffic traces and they will be used throughout the project life cycle in order to gather statistically significant amount oftraffic patterns. We will evaluate existing techniques and, if necessary, develop new ones for the construction of arrival processes that are able to reproduce thecollected traffic patterns. The problem tackled in this task is similar to the one faced in T2.1 and hence a continuous cooperation is foreseen between PMi and UTo.

T2.3 Symbolic state space representation (UMe)

The first stages of this task will be carried out by UMe: (1) study the use of multi-terminal multi-valued decision diagrams to store the augmented reachability graph;(2) development of saturation based state space generation techniques; (3) implementation of the techniques developed in (1) and (2). The remaining stage will bededicated to comparisons with other techniques resulting from task T3.1 (PMi), T3.2 (UMe) and T3.3 (UFi). The building blocks of the models considered in this taskare phase type distributions. Accordingly, there will be a continuous connection with T2.1 (UTo).

T2.4 Models with matrix exponential durations (UTo)

In the first phase, UTo will evaluate the use of general purpose differential equation and linear system solvers for the analysis of models with matrix exponential (ME)durations. The second stage (UTo) is dedicated to develop ad-hoc solvers that exploit characteristics of ME distributions. In the third phase we will develop thediscrete time counterpart of the expansion technique used to handle models with ME durations. To carry out this phase, the discrete time counterpart of MEdistribution is necessary, which will be defined by task T2.1. As the expansion technique on which T2.3 is based can be applied to models with ME timings as well,there will be continuous connection with T2.3 (UMe).

T3.1 Asymptotic techniques (PMi)

Devoted to two asymptotic techniques: mean-field analysis and bottleneck analysis for large scale non-Markovian models. Studies of both the techniques will beconducted in parallel. For what concerns mean-field analysis, the technique will be extended to allow for continuous quantities in the state space of the objectscomposing the system. The efforts on bottleneck analysis will study how simply computable measures, like system power, can be exploited to define better loaddistribution algorithms in complex systems. The resulting methods will be implemented and compared to the other approximate techniques.

T3.2 Fixed point iteration with distributions (UMe)

In the first phase UMe will develop a fixed point algorithm for the steady state solution of non-Markovian models composed of nearly independent subsystems. Thiswill require distribution approximation techniques that are tested and developed in T2.1 (UTo). The second phase will be dedicated to study convergencecharacteristics of the algorithm and will be carried out by UMe. In the third phase UMe will extend the algorithm to transient analysis. The last phase is dedicated to

17

comparison with other techniques developed in tasks T2.3 (UMe), T2.4 (UTo) and T3.1 (PMi).

T3.3 Solution of models with preemptive scheduling (UFi)

Carried out mainly by UFi. UFi will first define formal semantics that extends stochastic state classes to encompass systems with preemption. In the second phase,exact analysis techniques will be characterized together with the identification of complexities deriving from the presence of preemption mechanisms. The third phaseis devoted to develop suitable approximation for the support of timers and for the analytic form of distributions in order to reduce complexity. This phase will usetechniques developed in T2.1 (UTo). In the fourth phase a prototype tool will be implemented. The algorithms provided by the tool will be compared againsttechniques developed in tasks T2.3 (UMe), T4.4 (UFi).

T4.1 Model checking Markov regenerative processes (UFi)

The first phase of this task will be carried out by UFi and UTo and will lead to the definition of a probabilistic model checking algorithm based on stochastic stateclasses. The second phase (UTo,UFi) will refine the algorithm in such a way that it will be capable of exploiting regeneration points of the model. This will requireformula driven derivation of the local and global kernel of the model. The third phase will be dedicated by UFi to implement a prototype tool. The tool will be used tocompared against other techniques resulting from T2.3 (UMe), T4.3 (UTo) and T4.4 (UTo).

T4.2 Unified model checking (UTo)

Carried out mainly by UTo. The first phase will be dedicated to classify the existing stochastic temporal logic languages and compare their expressivity against thatof CSL-TA. In the second phase an efficient model checking algorithm for CSL-TA will be designed. The algorithm will be implemented and integrated into theMC4CSLTA tool. The performance of the tool will be studied both theoretically and experimentally and it will be compared to the performance of techniquesdeveloped in task T4.4 (UFi).

T4.3 Model checking by abstraction (UTo)

Carried out mainly by UTo. The first phase will define an algorithm for the construction of abstract models of non-Markovian systems in the form of probabilistictimed automata (PTA). In the second phase, we will study how the output of the algorithm of the first phase can be analyzed by existing PTA model checking tools. Inthe third phase, we will identify and/or develop verification techniques particularly adapted to the verification of PTA resulting as abstract models of non-Markoviansystems. The approach will be compared against approaches developed in tasks T4.1(UFi) and T4.4(UFi).

T4.4 Statistical model checking (UFi)

In the first phase UFi will define a temporal logic for expressing properties of non-Markovian systems. Then, algorithms for statistical model checking of the definedlogic against non-Markovian systems will be developed. This step will be carried out by UFi in cooperation with the members of UTo having experience in simulationof non-Markovian models. Subsequently, a prototype tool will be implemented. Comparisons will be carried against methods resulting from tasks T4.1(UFi) andT4.3(UTo).

T4.5 Compositional model specification and analysis (UFi)

Carried out prevalently by UFi. In the first phase, compositional specifications and reasoning for timed and concurrent but not probabilistic systems will be studied.Subsequently, these techniques will be brought to the probabilistic domain and applied to Markovian systems. In the third phase, we will consider non-Markovianmodels.

13 - Obiettivi finali che il progetto si propone di raggiungereItaliano

L'applicabilità degli approcci di modellazione formale per sistemi concorrenti e probabilistici è limitata dai seguenti fattori: (1) la maggior parte delle tecnicheutilizza modelli Markoviani che spesso presentano un potere espressivo troppo limitato per potersi adattare a casi reali; (2) anche qualora si riesca ad utilizzare imodelli Markoviani mediante la tecnica di Markovianization, l'esplosione dello spazio degli stati può renderne impraticabile l'analisi; (3) le modalità per formuare ledomande alle quali l'analisi deve fornire una risposta sono spesso limitate e/o poco naturali per utenti non esperti.

Per superare le succitate limitazioni, alla fine del presente progetto saranno disponibili i seguenti risultati teorici concreti:

1. Tecniche innovative per l'approssimazione di eventi non-Markoviani.2. Un benchmark di distribuzioni per la valutazione delle tecniche disponibili per la rappresentazione di eventi non-Markoviani mediante approssimazioniMarkoviane.3. Nuove metodologie per la caratterizzazione del traffico in grado di riprodurne correttamente la correlazione e l'andamento a picchi.4. Nuove tecniche simboliche per la memorizzazione ed il calcolo del grafo di raggiungibilità associato ai modelli con distribuzioni Phase type.5. Tecniche efficienti per la soluzione di modelli con distribuzioni e processi matrix exponential.6. Nuove estensioni dell'approccio mean field per il supporto di oggetti con spazio degli stati ibridi.7. Tecniche innovative per l'analisi in transiente di sistemi non-Markoviani basati sull'approccio a punto fisso con passaggio di distribuzioni di probabilità.8. Un'estesa teoria sulle classi di stato stocastiche per la rappresentazione di modelli che presentano differenti politiche di prelazione.9. Nuove procedure di model checking basate sull'approccio delle classi di stato stocastiche.10. La specifica di una logica temporale probabilistica unificata e di un efficiente algoritmo di model checking associato ad essa.11. Nuovi metodi di astrazione per sistemi non-Markoviani che evitano la costruzione esplicita dei region graph.12. Una logica temporale stocastica per descrivere le proprietà caratterizzanti dei sistemi non-Markoviani.13. Nuovi algoritmi di model checking, basati su di un approccio stocastico, per supportare l'analisi di sistemi concorrenti e temporizzati.14. Nuovi algoritmi di model checking per l'analisi in transiente di processi semi-Markoviani generalizzati e di processi di Markov rigenerativi.15. Un insieme di tool formali per il supporto di specifiche composizionali di sistemi concorrenti temporizzati.

Inglese

The applicability of formal modeling approaches for probabilistic timed concurrent systems is limited by the following factors: (1) most techniques addressMarkovian models whose expressive power is often too low for real problems; (2) even if by Markovianization a Markovian model can be used to model the system,the state space explosion problem can inhibit the analysis;(3) the ways of expressing the questions that the analysis has to answer are often limited and/or not naturalfor non-experts.

To overcome these limitations, at the end of the project the following concrete theoretical results will be available:

1. Novel techniques for approximation of non-Markovian durations.2. A benchmark of distributions for the evaluation of the available techniques for representing non-Markovian durations by Markovian approximations.3. New methodologies for traffic characterization that properly reproduce the correlation and the burstiness structure of the traffic.

18

4. New symbolic techniques for storing and computing reachability graphs associated with models with Phase type distributed timings.5. Efficient solution techniques for models with matrix exponential durations and matrix exponential processes.6. Novel extensions of the mean field approach to support objects with hybrid state space.7. New techniques for transient analysis of non-Markovian systems based on a “distribution passing” fixed point approach.8. An extended theory of stochastic state classes to encompass models combining different preemption policies.9. New model checking procedures based on the stochastic state class approach.10. Specification of a unified probabilistic temporal logic and an efficient associated model checking algorithm.11. New abstraction methods for non-Markovian systems which avoid the explicit construction of region graphs.12. A stochastic temporal logic for describing distinguished properties of non-Markovian systems.13. New model checking algorithms, based on the statistical approach, to support analysis of timed concurrent systems.14. New model checking algorithms for transient analysis of generalized semi-Markov processes and Markov regenerative processes.15. A set of formal tools supporting compositional specifications of timed concurrent systems.

14 - Risultati attesi dalla ricerca, e loro interesse per l'avanzamento della conoscenza e per le eventualipotenzialità applicativeItaliano

I risultati del progetto, costituiti da metodologie e strumenti per il progetto e la gestione di sistemi distribuiti, saranno utilizzati per supportare l'analisi dei casiapplicativi presi in esame:1. Cloud computing.2 Reti di sensori wireless.3 Predizione dinamica per infrastrutture di monitoraggio distribuito.4 Processo di sviluppo di SW real-time.5 Diffusione di modelli organizzativi di business.

L'utilizzo di queste applicazioni, che ricadono nelle aree di interesse enfatizzate dal programma FIRB, per la valutazione delle tecniche considerate metterà inevidenza l'impatto dei risultati del progetto nel campo dell'analisi dei modelli concorrenti e temporizzati. In particolare:

1. I modelli analitici basati sullo spazio degli stati e le tecniche descritte nel WP2 (T2.3) troveranno applicazione nel dimensionamento delle risorse dei sistemi cloudIaaS per la gestione del carico, dei consumi energetici, della disponibilità e degli SLA. In particolare, tali strumenti permetteranno di stabilire la capacità ottimale (intermini di risorse fisiche) e la configurazione minima (in termini di numero di server in hot, warm e cold standby) per soddisfare i requisiti stabiliti dagli SLAminimazzando al contempo il costo totale ed il consumo energetico.

2. Le tecniche di valutazione quantitativa, sviluppate nel WP2, nel WP3 e nel WP4, saranno utilizzate per il progetto e la valutazione delle reti di sensori wireless. Gliambiti presi in esame saranno: le tecniche di risparmio energetico, gli approcci di gestione mediante ridondanza, la valutazione delle topologie di rete, la definizionedi protocolli di routing multi-hop orientati alle prestazioni.

3. Le tecniche per il model checking di sistemi non-Markoviani descritte nel WP4 (T4.1,T4.3) saranno utilizzate per supportare il monitoraggio di applicazioni disistemi critici. In particolare, tali strumenti permetteranno lo sviluppo di un motore di predizione on-line in grado di supervisionare l'evoluzione del sistemamonitorato attraverso l'acquisizione di misure e di quantificare di conseguenza le probabilità dei possibili comportamenti futuri.

4. Le tecniche per la valutazione quantitativa dei sistemi non-Markoviani con prelazione, descritte nel WP3 (T3.3), saranno utilizzate per supportare le fasi disviluppo di SW real time. In particolare, sarà possibile stabilire indici prestazionali che permetteranno di svolgere in maniera più rigorosa le fasi di progetto e diverifica del ciclo di vita del SW.

5. Le tecniche mean-field saranno applicate all'analisi della diffusione di modelli organizzativi di business. In particolare, tali tecniche permetteranno dicaratterizzare i modelli organizzativi e gli obiettivi strategici delle aziende di un settore industriale, in modo tale da investigare l'evoluzione del settore e delle sueaziende catturando la correlazione tra i modelli organizzativi, gli obiettivi strategici e le prestazioni delle aziende.

Inglese

Project outcomes, providing methodologies and tools for the design and maintenance of distributed systems, will be applied to support the analysis of the applicationcases considered in the project:1. Cloud computing2. Wireless sensor networks3. Online prediction for distributed monitoring infrastructures4. Development process of real-time SW5. Diffusion of business organization models

The use of these applications, which are in the areas of interest emphasized by the FIRB program, to validate the considered techniques will address the impact of theproject outcomes in the field of the analysis of timed concurrent models. More specifically:

1. Analytical state-space models and techniques described in WP2 (T2.3) will found application in capacity planning of IaaS clouds with respect to load, energyconsumption, availability, and SLA guaranties. In particular, they will support the derivation of the optimal capacity (in terms of physical resources) andconfiguration (in terms of number of servers that are in hot, warm, and cold pools) to uphold the cloud SLA requirements while minimizing the total cost and energyconsumption.

2. Quantitative evaluation techniques, developed in WP2, WP3, and WP4, will be employed in design and evaluation of WSN to support: power saving techniques,redundancy management approaches, network and topology evaluation, definition of performance-oriented multi-hop routing protocols.

3. Techniques for model checking of non-Markovian systems described in WP4 (T4.1,T4.3) will be used to support monitoring of safety-critical applications. Inparticular, they will enable the development of an on-line prediction engine that supervises the evolution of the system through the acquisition of measurements andquantifies the probability of the possible future behaviors.

4. Techniques for quantitative evaluation of non-Markovian preemtive systems described in WP3 (T3.3) will be employed to support the steps of development ofreal-time SW. In particular, they will support the derivation of performance rewards that permit to attain to a higher degree of rigor in design and verificationactivities of the SW life cycle.

5. Mean-field techniques will be applied to the analysis of the diffusion of open business organization models. In particular, they will permit to characterize theorganization model and the strategic focus of companies of an industry, so as to gain insight into the evolution of the industry and its companies by capturing thecorrelation among the organizational model, the strategic focus, and the performance of the companies.

19

15 - Articolazione del progetto e tempi di realizzazioneItaliano

Ogni task del progetto è organizzato in due fasi. Come fattore comune, la maggior parte dei task non orientati alle applicazioni terminano con una fase nella quale letecniche sviluppate sono applicate ai modelli delle aree applicative. Queste fasi si collocano indicativamente tra il mese 15 ed il mese 36. Questo non significa che lefasi saranno attive in tutto il periodo. Saranno piuttosto attive quando sarà necessario e riceveranno feedback dai task delle applicazioni. Molti task prevedono ladefinizione e lo sviluppo di algoritmi. La realizzazione di queste fasi sarà favorita dall'esperienza delle unità di ricerca accumulata nell'ambito dello sviluppo di tool,e si realizzerà anche attraverso l'estensione degli strumenti esistenti precedentemente sviluppati dalle varie unità.

Di seguito, verranno descritte le fasi con la rispettiva temporizzazione. In fondo vengono riportate la diagramma di Gantt del progetto e la matrice task-unità dicoinvolgimenti.WP1 (UMe): Aree di ApplicazioneT1.1 Cloud computing (UMe)

Il Cloud Computing rappresenta un'area di applicazione complessa. Per il disegno, questa richiede un'accurata fase di configurazione, una lunga fase di analisi, euno sfruttamento dei risultati ottenuti. Il task sarà attivo per tutta la durata del progetto.

1. Mesi 01-02: Studio dello stato dell'arte sulle problematiche di performance e di availability del cloud computing e su infrastrutture distribuite su larga scala ingenerale2. Mesi 02-03: Raccolta dei pattern di distribuzione di traffico tipici del cloud computing; identificazione degli indici di performance e di availability e deibenchmarks.3. Mesi 04-12: Disegno di modelli di infrastrutture per il cloud computing.4. Mesi 15-30: Applicazione delle tecniche di soluzione sviluppate durante il progetto per l'analisi dei modelli.5. Mesi 25-36: Uso dei risultati dell'analisi dei modelli per pianificare la capacità del cloud (analisi di sensitività, identificazione dei colli di bottiglia, modellipredittivi), rafforzamento del SLA ed ottimizzazione delle risorse.


Anche le WSN costituiscono una applicazione complessa in cui la configurazione, l'analisi, e corretto sfruttamento hanno un ruolo importante. Per evitaresovrapposizioni con il T1.1 questo task non viene attivato immediatamente all'inizio del progetto.

1. Mesi 03-04: Stato dell'arte sulle WSN e sulle problematiche di performance e availability di WSN.2. Mesi 04-05: Raccolta delle distribuzioni e dei pattern tipici del traffico delle WSN; individuazione degli indici di performance e availability e dei benchmark.3. Mesi 04-14: Disegno di modelli delle WSN con particolare riferimento a: (i) tecniche per il risparmio energetico (politiche active-sleep policies, sleep multipli); (ii)gestione della ridondanza; (iii) valutazione della rete e della topologia.4. Mesi 15-30: Applicazione delle tecniche di soluzione sviluppate durante il progetto per l'analisi dei modelli.5. Mesi 25-36: Disegno di protocolli di instradamento multi-hop orientati alle performance.6. Mesi 25-36: Disegno di algoritmi auto adattivi per WSN.

T1.3 Predizione dinamica per infrastrutture di monitoraggio distribuito (UFi)

Questa rappresenta una area più circostanziata rispetto a quelle dei task T1.1 e T1.2. Per questa ragione e per evitare conflitti con T1.1 e T1.2, il task verrà attivatodopo sei mesi dall'inizio del progetto.

1. Mesi 07-11: Studio dello stato dell'arte sulle tecniche di monitoring per i sistemi safety-critical e WSN.2. Mesi 12-16: Caratterizzazione dei contesti applicativi e identificazione dei criteri che il sistema deve soddisfare.3. Mesi 17-23: Configurazione di un ambiente di test.4. Mesi 22-36: Applicazione delle tecniche di model checking per la predizione online dell'evoluzione del sistema.

T1.4 Processo di sviluppo di SW real-time (UFi)

Questo task condivide alcuni aspetti con quello precedente e quindi le loro temporizzazioni sono sincronizzate.

1. Mesi 07-11: Studio dello stato dell'arte sui processi di sviluppo e degli standard di certificazione per le componenti SW real-time.2. Mesi 12-16: Caratterizzazione dei contesti applicativi e identificazione dei criteri che il sistema deve soddisfare.3. Mesi 17-23: Configurazione di un ambiente di test.4. Mesi 22-36: Uso di tecniche di modellizzazione e di tecniche di analisi quantitativa ai sistemi preemptive per il supporto al disegno, implementazione e verifica delSW real-time.

T1.5 Diffusione di modelli organizzativi di business (UTo)

Questa area di applicazione è meno complessa ed ha una collocazione temporale più limitata.

1. Mesi 18-21: Identificazione delle industrie di studio, caratterizzazione delle compagnie in termini del modello di organizzazione e focus strategico.2. Mesi 22-25: Disegno di modelli per descrivere il comportamento temporale delle singole compagnie considerando anche le dipendenze con gli altri attori delprocesso produttivo.3. Mesi 26-30: Analisi dei modelli con le tecniche sviluppate nel progetto per verificare se l'approccio proposto può agevolare le compagnie fornendo loro unapercezione del processo produttivo.

Viene ora descritta la temporizzazione dei task non orientati alle applicazioni. La definizione delle tempistiche è basata su (i) requisiti identificati dalle applicazioni,(ii) relazioni tra i task, (iii) e un bilanciamento dell'uso delle risorse umane rispetto alle tempistiche del progetto.WP2 (UTo): Analisi di modelli non-Markoviani attraverso MarkovianizzazioneT2.1 Approssimazione di distribuzioni(UTo)

1. Mesi 01-04: Raccolta di benchmark di distribuzioni che descrivano (i) durate tipiche nelle aree di applicazione, (ii) durate tipiche nel reliability engineering, (iii)durate che sono usate nell'approccio basato su punto fisso (T3.2).2. Mesi 04-07: Sviluppo e valutazione delle tecniche di approssimazione di distribuzioni esistenti.3. Mesi 08-10: Definizione della controparte discreta delle distribuzioni matrix exponential (ME) e ridefinizione delle più promettenti tecniche di fitting a tempocontinuo nel tempo discreto.4. Mesi 11-14: Sviluppo ed implementazione di tecniche di approssimazione basate su famiglie di polinomi ortogonali.5. Mesi 12-16: Implementazione di un toolkit di tecniche di approssimazione di distribuzioni da utilizzare negli altri task e nelle aree di applicazione (T1.1, T1.2 and

20

T1.4).

T2.2 Caratterizzazione del traffico(PMi)

1. Mesi 01-06: Realizzazione di strumenti per la collezione di tracce di traffico: (i) sonde software, (ii) tecniche basate su ricerche avviate dall'utente.2. Mesi 07-36: Collezionamento di tracce. Questa fase continuerà fino alla fine dl progetto in modo da collezionare il maggior quantità possibile di dati. L'analisi deidati inizierà non appena una quantità adeguata di campionamenti statistici sarà disponibile.3. Mesi 12-17: Identificazione e sviluppo di metodi per la costruzione dei processi di arrivo che sono in grado di riprodurre gli schemi di traffico collezionati.4. Mesi 18-36: Uso degli strumenti sviluppati per l'analisi dei modelli delle aree di applicazione (principalmente T1.1 e T1.2) e confronto con altre tecniche.

T2.3 Rappresentazione simbolica dello spazio degli stati (UMe)

1. Mesi 04-07: Sviluppo di un algoritmo per l'uso di diagrammi di decisione multi-valore e multi-terminali per la memorizzazione di grafi di raggiungibilitàaumentati.2. Mesi 06-10: Sviluppo di algoritmi di generazione degli stati basati su saturazione.3. Mesi 11-18: Implementazione degli algoritmi sviluppati nelle fasi 1 e 2.4. Mesi 16-36: Uso dei tool sviluppati per l'analisi dei modelli delle aree di applicazione(principalmente T1.1 e T1.2) e confronto con altre tecniche.

T2.4 Modelli con distribuzioni matrix exponential (UTo)

1. Mesi 01-03: Valutazione delle equazioni differenziali generali e dei risolutori di sistemi lineari nell'analisi di modelli con durate matrix exponential.2. Mesi 04-09: Sviluppo di un risolutore ad-hoc che sfrutta le caratteristiche delle distribuzioni matrix exponential.3. Mesi 10-14: Sviluppo della controparte a tempo discreto della tecnica di espansione usata per gestire i modelli con durate matrix exponential.4. Mesi 15-36: Uso dei tool sviluppati per l'analisi dei modelli delle aree di applicazione(principalmente T1.1 e T1.2) e confronto con altre tecniche.

WP3 (PMi): Analisi approssimata di modelli non-MarkovianiT3.1 Tecniche asintotiche (PMi)

1. Mesi 04-07: Studio dell'importanza dell'importanza della potenza dei sistemi nelle tecniche di analisi multi classe di colli di bottiglia.2. Mesi 08-17: Estensione delle analisi mean-field per considerare uno spazio degli stati misto continuo-discreto.3. Mesi 18-36: Uso delle analisi bottleneck nel trattamento dei modelli delle aree di applicazione (mainly T1.1 and T1.2) e confronto con altre tecniche.4. Mesi 18-36: Uso di approcci mean-field estesi nell'analisi dei modelli (principalmente T1.2 e T1.5) delle aree di applicazione e confronto con altre tecniche.

T3.2 Iterazione di punto fisso con distribuzioni (UMe)

1. Mesi 04-07: Sviluppo, per l'analisi steady state di modelli non-Markoviani composti da sottosistemi indipendenti, di un approccio basato su iterazione di puntofisso nel quale le distribuzioni sono passate tra i sottomodelli.2. Mesi 08-11: Studio di caratteristiche di convergenza dell'algoritmo sviluppato nella fase 1.3. Mesi 10-14: Estensione dei metodi sviluppati nella fase 1 all'analisi transiente.4. Mesi 12-16: Implementazione degli algoritmi sviluppati.5. Mesi 15-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (principalmente T1.1, T1.2 e T1.4) e confronto con altre tecniche.

T3.3 Soluzione di modelli con scheduling preemptive (UFi)

1. Mesi 01-02: Definizione di una semantica formale che estende le classi stocastiche per considerare sistemi con preemption.2. Mesi 03-08: Caratterizzazione delle tecniche di analisi ed identificazione delle complicazioni derivanti dalla presenza dei meccanismi di preemption.3. Mesi 09-12: Definizione di approssimazioni per ridurre la complessità dell'analisi.4. Mesi 10-16: Implementazione dei metodi delle fasi 2 e 3 in un tool prototipale.5. Mesi 15-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (principalmente T1.2 e T1.4) e confronto con altre tecniche.WP4 (UFi): Model checkingT4.1 Model checking di processi rigenerativi Markoviani (UFi)

1. Mesi 05-08: Sviluppo, per i processi semi-Makoviani generalizzati, di un algoritmo di model checking per le formule limitate nel tempo su classi di statostocastiche.2. Mesi 09-14: Raffinamento dell'algoritmo sviluppato nella fase 1 in modo da considerare eventuali punti di rigenerazione, per la definizione di un algoritmo dimodel checking per processi Markoviani rigenerativi.3. Mesi 15-20: Implementazione prototipale degli algoritmi sviluppati nella fase 1 e 2.4. Mesi 21-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (principalmente T1.2, T1.3 e T1.4) e confronto con altre tecniche.

T4.2 Logica temporale stocastica unificata (UTo)

1. Mesi 06-10: Classificazione delle logiche temporali stocastiche in termini delle loro complessità.2. Mesi 11-15: Definizione di un algoritmo efficiente per il model checking di formule CSL-TA su catene di Markov a tempo continuo.3. Mesi 16-22: Implementazione dell'algoritmo sviluppato nella fase 2 ed integrazione nel tool MC4CSLTA.4. Mesi 23-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (principalmente T1.2 e T1.3) e confronto con altre tecniche.

T4.3 Model checking attraverso astrazioni (UTo)

1. Mesi 08-12: Sviluppo di un algoritmo per la costruzione di modelli astratti di sistemi non-Markoviani nella forma di automi probabilistici temporizzati (PTA).2. Mesi 13-17: Uso dei tool di model checking per PTA esistenti per l'analisi degli automi generati dall'algoritmo sviluppato nella fase 1.3. Mesi 18-22: Identificazione e/o sviluppo di tecniche di verifica particolarmente adatte all'analisi dei PTA ottenuti come astrazione di sistemi non-Markoviani.4. Mesi 23-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (principalmente T1.2 e T1.3) e confronto con altre tecniche.

T4.4 Model checking statistico (UFi)

1. Mesi 08-11: Definizione di una logica temporale adeguata ad esprimere le proprietà tipiche dei sistemi non-Markoviani.2. Mesi 12-16: Sviluppo di un algoritmo per il model checking statistico per sistemi non-Markoviani che utilizzi la logica introdotta nella fase 1.3. Mesi 15-18: Studio dei miglioramenti di performance per gli algoritmi di model checking statistico esistenti basati sampling stratificato.4. Mesi 19-22: Implementazione prototipale degli algoritmi sviluppati nelle fasi 2 e 3.5. Mesi 23-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (T1.1, T1.2, T1.3 e T1.4) e confronto con altre tecniche.

T4.5 Specifica ed analisi composizionale di modelli (UFi)

21

1. Mesi 05-07: Studio di metodi per la specifica composizionale ed il ragionamento su sistemi temporizzati e concorrenti ma non probabilistici.2. Mesi 08-12: Sviluppo di tecniche di specifica e ragionamento composizionale per modelli Markoviani.3. Mesi 10-16: Studio delle possibili estensioni dei risultati della fase 2 a sistemi non-Markoviani.4. Mesi 15-20: Implementazione prototipale degli algoritmi sviluppati nelle fasi 2 e 3.5. Mesi 21-36: Uso degli strumenti sviluppati nell'analisi dei modelli delle aree di applicazione (principalmente T1.1 e T1.3) e confronto con altre tecniche.

Diagramma di Gantt del progetto

22

Matrice task-unità di coinvolgimenti

Inglese

Every task of the project is organized into phases. As a common trait, most non application oriented tasks finish with a phase in which the developed techniques areapplied to the models of the application areas. These phases will be open from around month 15 to month 36. This does not mean that these phases will becontinuously active in this period. They will be active when necessary and will receive feedback from the application tasks. Many tasks include the implementation ofthe developed algorithms which will be possible thanks to the experience of the units in tools and will be carried out as extensions to existing tools that were createdby the units.

In the following we provide the phases along with the respective timing. After that, the Gantt diagram and the task-unit matrix of the project are depicted.WP1 (UMe): Application areasT1.1 Cloud computing (UMe)

Cloud computing is a complex application area. It requires careful set up of the problems, a long analysis phase, and exploitation of the results for design issues.Accordingly, the task starts at the beginning of the project and ends at the end of the project.

1. Month 01-02: Study of the state of the art on performance and availability issues of cloud computing and of large scale-distributed infrastructures in general.2. Month 02-03: Collection of typical distributions and traffic patterns of cloud computing; identification of performance and availability indices and benchmarks.3. Month 04-12: Design of models of cloud computing infrastructures.4. Month 15-30: Application of the solution techniques developed during the project for the analysis of the models.5. Month 25-36: Exploitation of the analysis of the models for cloud capacity planning (sensitivity analysis, bottlenecks identification, prediction models), SLAenforcement and resource optimization.


Also WSN constitute a complex application are in which set up, analysis, and exploitation are all important issues. In order to avoid conflict with T1.1 this task doesnot start right at the beginning of the project.

1. Month 03-04: State of the art on WSN and on performance and availability issues of WSN.2. Month 04-05: Collection of typical distributions, traffic pattern of WSN; identification of performance and availability indices and benchmarks.3. Month 04-14: Design of models of WSN regarding: (i) power saving techniques (active-sleep policies, multiple sleep); (ii) redundancy management; (iii) networkand topology evaluation.4. Month 15-30: Application of the solution techniques developed during the project for the analysis of the models.5. Month 25-36: Design of performance-oriented routing protocols in multi-hop WSN.6. Month 25-36: Design of self adaptive algorithms for WSN.

T1.3 Online prediction for distributed monitoring infrastructures (UFi)

23

A more circumscribed area than those of T1.1 and T1.2. Both for this reason and in order to avoid conflict with T1.1 and T1.2, the task is started six month after thebeginning of the project.

1. Month 07-11: Study of the state of the art on monitoring techniques for safety-critical systems and wireless sensor networks.2. Month 12-16: Characterization of the specific application setting and identification of criteria that the system has to fulfill.3. Month 17-23: Set up of a testbed environment.4. Month 22-36: Application of model checking techniques to online prediction of system evolution.

T1.4 Development process of real-time SW (UFi)

This task shares some of the challenges with the previous one and hence their schedule is synchronized.

1. Month 07-11: Study of the state of the art on development processes and certification standards for real-time SW components.2. Month 12-16: Characterization of the specific application setting and identification of criteria for the development process.3. Month 17-23: Set up of a testbed environment.4. Month 22-36: Application of modeling and quantitative analysis techniques for preemptive systems to support the steps of design, implementation, and verificationof real-time SW.

T1.5 Diffusion of business organization models (UTo)

This application area is the less complex and has a more limited timeframe.

1. Month 18-21: Identification of the industries to study, characterization of the companies in terms of their organization model and strategic focus.2. Month 22-25: Design of models to describe the temporal behavior of the individual companies considering also the dependencies among other players of theindustry.3. Month 26-30: Analysis of the models with techniques developed in the project to verify if the approach can be beneficial to the companies by providing them insightto the industry.

From now on the timing of the non application oriented tasks is described. The definition of these timings are based on (i) requirements put up by the applications, (ii)the relation of the tasks, (iii) and a balanced usage of human resources over the time frame of the project.

WP2 (UTo): Analysis of non-Markovian models by Markovianization

T2.1 Distribution approximation (UTo)

1. Month 01-04: Collection of a benchmark of distributions describing (i) typical durations in the application areas, (ii) typical durations in reliability engineering,(iii) durations that are used in the fixed point approach (T3.2).2. Month 04-07: Implementation and evaluation of existing techniques of distribution approximation.3. Month 08-10: Definition of the discrete time counterpart of matrix exponential (ME) distributions and redefinition of the most promising continuous time fittingtechniques in discrete time.4. Month 11-14: Development and implementation of approximation techniques based on families of orthogonal polynomials.5. Month 12-16: Implementation of a toolkit of distribution approximation techniques to use in other tasks and in the application areas (T1.1, T1.2 and T1.4).

T2.2 Traffic characterization (PMi)

1. Month 01-06: Realization of tools to collect traffic traces: (i) software probes, (ii) user initiated query based techniques.2. Month 07-36: Collection of traces. This phase will last until the end of the project in order to collect the largest possible amount of data. The analysis of the datawill start as soon as a statistically significant amount of samples will be available.3. Month 12-17: Identification and development of methods for the construction of arrival processes that are able to reproduce the collected traffic patterns.4. Month 18-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.1 and T1.2) and comparison with othertechniques.

T2.3 Symbolic state space representation (UMe)

1. Month 04-07: Development of an algorithm for the use of multi-terminal multi-valued decision diagrams for the storage of augmented reachability graphs.2. Month 06-10: Development of saturation based state space generation algorithms.3. Month 11-18: Implementation of the algorithms developed in phase 1 and 2.4. Month 16-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.1 and T1.2) and comparison with othertechniques.

T2.4 Models with matrix exponential durations (UTo)

1. Month 01-03: Evaluation of general purpose differential equation and linear system solvers in the analysis of models with matrix exponential durations.2. Month 04-09: Development of ad-hoc solvers that exploit characteristics of matrix exponential distributions3. Month 10-14: Development of the discrete time counterpart of the expansion technique used to handle models with matrix exponential durations.4. Month 15-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.1 and T1.2) and comparison with othertechniques.

WP3 (PMi): Approximate analysis of non-Markovian models

T3.1 Asymptotic techniques (PMi)

1. Month 04-07: Investigation of the importance of the system power in the multiclass bottleneck analysis technique.2. Month 08-17: Extension of the mean-field analysis technique to include mixed continuous-discrete state spaces.3. Month 18-36: Utilization of bottleneck analysis in the treatment of the models of the application areas (mainly T1.1 and T1.2) and comparison with othertechniques.4. Month 18-36: Utilization of the extended mean-field approach in the analysis of the models (mainly T1.2 and T1.5) of the application areas and comparison withother techniques.

T3.2 Fixed point iteration with distributions (UMe)

24

1. Month 04-07: Development, for the steady state analysis of non-Markovian models composed of nearly independent subsystems, of a fixed point iteration approachin which distributions are passed among submodels.2. Month 08-11: Study of convergence characteristics of the algorithm defined in phase 1.3. Month 10-14: Extension of the method developed in phase 1 to transient analysis.4. Month 12-16: Implementation of the developed algorithms.5. Month 15-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.1, T1.2 and T1.4) and comparison with othertechniques.

T3.3 Solution of models with preemptive scheduling (UFi)

1. Month 01-02: Definition of a formal semantics that extends stochastic state classes to encompass systems with preemption.2. Month 03-08: Characterization of an exact analysis technique and identification of complexities deriving from the presence of preemption mechanisms.3. Month 09-12: Definition of approximations in order to reduce analysis complexity.4. Month 10-16: Implementation of a prototype tool of methods of phase 2 and 3.5. Month 15-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.2 and T1.4) and comparison with othertechniques.

WP4 (UFi): Model checking

T4.1 Model checking Markov regenerative processes (UFi)

1. Month 05-08: Development, for generalized semi-Markov processes, of a model checking algorithm for time bounded formulas based on stochastic state classes.2. Month 09-14: Refinement of the algorithm developed in phase 1 in order to exploit eventual regeneration points, leading to a model checking algorithm for Markovregenerative processes.3. Month 15-20: Prototype implementation of the algorithms developed in phase 1 and 2.4. Month 21-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.2, T1.3 and T1.4) and comparison with othertechniques.

T4.2 Unified model checking (UTo)

1. Month 06-10: Classification of existing stochastic temporal logics in terms of their complexity.2. Month 11-15: Development of en efficient algorithm for model checking CSL-TA formula on continuous time Markov chains.3. Month 16-22: Implementation of the algorithm developed in phase 2 and integration to the tool MC4CSLTA.4. Month 23-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.2 and T1.3) and comparison with othertechniques.

T4.3 Model checking by abstraction (UTo)

1. Month 08-12: Development of an algorithm for the construction of abstract models of non-Markovian systems in the form of probabilistic timed automata (PTA).2. Month 13-17: Utilization of existing PTA model checking tools for the analysis of automata generated by the algorithm developed in phase 1.3. Month 18-22: Identification and/or development of verification techniques particularly adapted to the analysis of PTA resulting as abstract models ofnon-Markovian systems.4. Month 23-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.2 and T1.3) and comparison with othertechniques.

T4.4 Statistical model checking (UFi)

1. Month 08-11: Definition of a suitable temporal logic for expressing properties of non-Markovian systems.2. Month 12-16: Development of a basic algorithm for statistical model checking of the defined logic against non-Markovian systems.3. Month 15-18: Study of performance enhancements for the existing statistical model checking algorithms based on stratified sampling.4. Month 19-22: Prototype implementation of the algorithms of developed in phase 2 and 3.5. Month 23-36: Utilization of the developed tools in the analysis of the models of the application areas (T1.1, T1.2, T1.3 and T1.4) and comparison with othertechniques.

T4.5 Compositional model specification and analysis (UFi)1. Month 05-07: Study of methods for compositional specifications and reasoning for timed and concurrent but not probabilistic systems.2. Month 08-12: Development of compositional specifications and reasoning for Markovian models.3. Month 10-16: Study of possible extensions of the results of phase 2 to non-Markovian systems.4. Month 15-20: Prototype implementation of the algorithms of developed in phase 2 and 3.5. Month 21-36: Utilization of the developed tools in the analysis of the models of the application areas (mainly T1.2 and T1.3) and comparison with othertechniques.

25

Gantt diagram of the project

26

Task-unit matrix of the project

16 - Elementi e criteri proposti per la verifica dei risultati raggiuntiItaliano

Sarà effettuata una valutazione continuativa lungo la durata temporale del progetto, tenendo in considerazione:1. milestone, meeting e prodotti del progetto,2. metodologia di lavoro adottata,3. aspetti economici,4. impatto scientifico delle tecniche sviluppate,5. visibilità dei risultati del progetto.

1. Milestone, meeting e prodotti del progetto

Sono stati pianificati quattro meeting durante il corso del progetto. Un kick-off meeting tenuto nel mese 2 servirà a riportare le iniziative preliminari e a definire lafutura organizzazione di cooperazione tra le unità. Il secondo meeting, intorno al mese 16, segnerà una milestone del progetto. Infatti, entro il mese 16 per i task T1.1e T1.2 devono essere definiti i modelli e molte delle tecniche proposte devono essere pronte per l'applicazione. Il terzo meeting è pianificato per il mese 30, ecostituisce la seconda milestone. Entro il mese 30 tutte le tecniche devono essere state sviluppate, molte di esse saranno disponibili in tool e per molte di esse sarannoraccolte esperienze applicative. Il meeting finale è previsto per la fine del progetto, entro la quale tutti i prodotti saranno stati sviluppati. Tenendo anche conto degliaspetti economici, sarà tenuta in considerazione l'ipotesi di effettuare i meeting in videoconferenza. Se possibile, uno dei milestone meeting sarà organizzato comeevento satellite di una conferenza o un workshop internazionale tenuto in Italia, in cui la disseminazione dei risultati possa essere effettuata istantaneamente e lapresenza di esperti internazionali fornisca feedback per il progetto.

I prodotti della ricerca saranno utilizzati per documentare gli sforzi effettuati. Quando possibile, i prodotti potranno interessare più di un task e più di una unità, inmodo da intensificare la collaborazione tra i gruppi di ricerca. Saranno sviluppati i seguenti prodotti (il mese e le unità interessate sono indicati dopo il titolo):

1. Documento di design con la definizione di una struttura dati basata su MTMDD per memorizzare grafi di raggiungibilità annotati. M5, UMe.2. Stato dell'arte sugli aspetti di prestazioni, affidabilità e disponibilità di sistemi cloud e Wireless Sensor Network (WSN). M6, UMe.3. Studio dell'importanza della potenza del sistema nelle tecniche di analisi multiclasse per i colli di bottiglia. M8, PMi.4. Caratterizzazione delle quantità, metriche, distribuzioni, pattern di traffico e benchmark per sistemi cloud e WSN. M8, UMe, UTo, PMi.5. Valutazione delle tecniche esistenti per l'approssimazione di distribuzioni e la caratterizzazione del traffico. M8, UMe, UTo, PMi.6. Definizione di un algoritmo basato su saturazione per calcolare e memorizzare il grafo di raggiungibilità di un sistema non-Markoviano. M10, UMe.7. Tecnica di analisi esatta per modelli con preemption e studio delle sue limitazioni. M10, UFi.8. Model checking per Generalized semi-Markov Process basato sulle classi di stato stocastiche. M10, UFi, UTo.9. Stato dell'arte per le tecniche di monitoraggio di sistemi safety-critical e WSN. M12, UFi.10. Stato dell'arte sullo sviluppo di software real-time. M12, UFi.11. Definizione di un insieme di criteri per la decomposizione di un modello e la validazione del modello risultante. M12, UMe.12. Soluzioni efficienti per modelli con distribuzioni e processi Matrix Exponential. M12, UTo.

27

13. Classificazione delle logiche temporali stocastiche esistenti. M12, UTo.14. Definizione di un'appropriata logica temporale per esprimere proprietà di modelli non-Markoviani. M12, UFi.15. Specifiche e tecniche di analisi composizionale per modelli Markoviani. M14, UFi.16. Studio di strumenti di model checking per modelli Probabilistic Timed Automata. M14, UTo.17. Documento di design con la definizione di un algoritmo completo per la soluzione di iterazioni a punto fisso. M14, UMe.18. Definizione e uso come approssimante della variante tempo-discreto di distribuzioni e processi Matrix Exponential. M14, UTo, PMi.19. Tecnica di analisi approssimata per modelli con preemption e studio delle sue limitazioni. M14, UFi.20. Model checking per Markov Regenerative Process basato sulle classi di stato stocastiche. M15, UFi, UTo.21. Modelli per la valutazione di sistemi cloud e WSN. M15, UMe.22. Estensione dell'analisi mean-field per includere spazi degli stati ibridi (continuo-discreto). M18, PMi.23. Sviluppo e design dell'implementazione di un algoritmo efficiente per il model checking di CSL-TA. M18, UTo.24. Metodi innovativi per l'approssimazione di distribuzioni e processi con Matrix Exponentials. M18, UTo, PMi.25. Uso di sampling stratificato nel model checking statistico. M20, UFi, UTo.26. Specifiche e tecniche di analisi composizionale per modelli non-Markoviani. M20, UFi, UTo.27. Definizione di uno specifico scenario applicativo e allestimento di un ambiente di prova per un'infrastruttura dinamica di monitoraggio. M24, UFi.28. Identificazione e/o sviluppo di tecniche per la verifica basata su astrazione di modelli non-Markoviani. M24, UTo.29. Definizione di uno specifico scenario applicativo e allestimento di un ambiente di prova per il processo di sviluppo di software real-time. M24, UFi.30. Definizione di un modello per la diffusione di modelli organizzativi di business. M26, UTo.31. Applicazione delle tecniche sviluppate in WP2 per l'analisi di sistemi cloud e WSN. M30, UMe.32. Conoscenze acquisite dall'applicazione di tecniche di Markovianizzazione per l'analisi di sistemi cloud e WSN. M30, UMe, UTo, PMi.33. Conoscenze acquisite dall'applicazione di tecniche di approssimazione per modelli non-Markoviani nell'analisi di sistemi cloud e WSN. M30, UMe, UFi, PMi.34. Conoscenze acquisite dall'applicazione di tecniche di model checking nell'analisi di WSN. M30, UMe, UFi. UTo.35. Analisi del modello per la diffusione di modelli organizzativi di business. M32, UTo, PMi.36. Utilizzo dell'analisi di sistemi cloud per il loro design e manutenzione. M36, UMe.37. Utilizzo dell'analisi di WSN per il loro design e manutenzione. M36, UMe.38. Applicazione delle tecniche di model checking all'infrastruttura dinamica di monitoraggio. M36, UFi, UTo.39. Applicazione delle tecniche di model checking nel processo di sviluppo di software real-time. M36, UFi, UTo.40. Applicazione di modelli preemptive non-Markoviani nel processo di sviluppo di software real-time. M36, UFi, UTo, UMe.

Inoltre, saranno redatti manuali e rapporti sullo stato di avanzamento per monitorare lo sviluppo degli strumenti.

2. Metodologia di lavoro adottata

La credibilità degli sforzi portati avanti nel progetto sarà suffragata dalla creazione di ambienti di prova e benchmark. Questi non solo forniranno alle unità unapiattaforma sulla quale testare le nuove tecniche proposte e i tool sviluppati, ma apriranno anche la strada a ricercatori non direttamente coinvolti nel progetto,consentendo loro di investigare e comparare gli avanzamenti scientifici e pratici raggiunti.

3. Apetti economici

L'articolazione del budget tiene conto della corrente situazione finanziaria. Infatti, si prevede che una porzione significativa del budget sarà usata per assumeregiovani ricercatori. Il budget di ogni unità è stato contenuto entro un basso limite per poter includere nella proposta di progetto quattro unità con un totale di 20ricercator i. L'attenzione per questo aspetto sarà mantenuta anche durante tutto il progetto. Quando possibile, le partecipazioni a conferenze e a incontri non sarannofinanziate usando le risorse del progetto.

4. Impatto scientifico delle tecniche sviluppate

Saranno monitorate la quantità e la qualità delle pubblicazioni scientifiche prodotte dalle unità, che document ano i risultati raggiunti nelle attività di ricerca. Laqualità delle pubblicazioni può essere valutata attraverso metriche che considerano le citazioni e sulla base della collocazione editoriale. Il numero di partecipantinon appartenenti alla comunità scientifica direttamente coinvolta nel progetto costituirà una metrica per valutare l'interesse verso i risultati raggiunti. Possibilicooperazioni con ricercatori internazionali che emergeranno durante le attività di ricerca rappresenteranno una ulteriore metrica di valutazione.

5. Visibilità dei risultati del progetto

Sarà sviluppato un sito web allo scopo di esporre direttamente le attività del progetto alla comunità scientifica e a quella industriale e allo scopo di monitorare passopasso lo stato di avanzamento del progetto. Il sito includerà una parte pubblica per la divulgazione dei risultati raggiunti e una riservata per lo scmabio di materialefra i partecipanti al progetto. Il sito conterrà i prodotti sviluppati e elencherà le pubblicazioni sottomesse e accettate. Per divulgare la conoscenza delle tematiche delprogetto, il sito web conterrà una bibliografia estesa e commentata sugli argomenti di ricerca.

Altri aspetti salienti

Il progetto promuoverà lo scambio e l'integrazione delle concoscenze fra loro complementari delle varie unità, grazie alla sua struttura multi-argomento (relativa siaalla conoscenza metodologica sia a quella applicativa).

I giovani ricercatori impiegati per mezzo di contratti di ricerca trarranno beneficio dall'acquisizione di capacità e di un maggior livello di professionalità attraversola loro partecipazione alle attività del progetto, che includono la partecipazione attiva a lavori sperimentali.

Le attività sperimentali interesseranno anche i contenuti dei programmi didattici accademici e delle attività di laboratorio.

Inglese

Continuous evaluation will be carried out along the time frame of the projectby taking into account:1. milestones, meetings and deliverables of the project,2. adopted work methodology,3. financial issues,4. scientific impact of the developed techniques,5. visibility of the project results.

1. Milestones, meetings and deliverables

We plan to have four meetings during the project. A kick-off meeting will be held in month 2 where preliminary efforts will be reported and future organization ofcooperation among the units will be defined. The second meeting, at around month 16, marks a milestone of the project. Indeed, by month 16, T1.1 and T1.2 have todefine the models and many techniques have to be ready to applied. The third meeting is planned for month 30, constituting the second mile stone. By month 30 alltechniques will be developed, most of them will be available in tools and for many of them application experiences will have been gathered. The final meeting isplanned for the end of the project by which all deliverables will be produced. Depending also on financial issues, we will consider to carry out the meetings by videoconference. If feasible, one of the two milestone meetings will be organized as a satellite event of an international conference or workshop held in Italy where resultsdissemination can be instantly done and the presence of international experts provide feedback for the project.

28

Deliverables will be used to document the efforts. When possible, deliverables involve more than one task and more than one unit in order to intensify cooperationamong the research groups. The following deliverables will be produced (with month and units involved indicated after the title):

1. Design document with the definition of a new MTMDD-based data structure to store augmented reachability graphs. M5, UMe.2. State of the art on performance, reliability and availability issues of clouds and wireless sensor networks (WSN). M6, UMe3. Investigation of the importance of the system power in the multiclass bottleneck analysis technique. M8, PMi.4. Characterization of quantities, metrics, distributions, traffic patterns and benchmarks of clouds and WSN. M8, UMe, UTo, PMi.5. Evaluation of existing techniques of distribution approximation and traffic characterization. M10, UTo, PMi.6. Definition of a Saturation based algorithm to compute and store the expanded reachability graph of a non-Markovian system. M10. UMe.7. Exact analysis technique for models with preemption and study of its limits. M10, UFi.8. Model checking for generalized semi-Markov processes based on stochastic state classes. M10, UFi, UTo.9. State of the art monitoring techniques for safety-critical systems and wireless sensor networks. M12, UFi.10. State of the art on real time SW development. M12, UFi.11. Definition of a set of criteria for the decomposability of a model and the validation of the decomposed model . M12, UMe.12. Efficient solution for models with matrix exponential distributions and processes. M12, UTo.13. Classification of existing stochastic temporal logics. M12, UTo.14. Definition of a suitable temporal logic for expressing properties of non-Markovian systems. M12, UFi.15. Compositional specifications and reasoning for Markovian models. M14, UFi.16. Study of existing probabilistic timed automata model checking tools. M14, UTo.17. Design document with the definition of a complete fixed point solution algorithm. M14, UMe.18. Definition of and approximation with the discrete counterpart of matrix exponential distributions and processes. M14, UTo, PMi.19. Approximate analysis techniques for models with preemption and study of their limits. M14, UFi.20. Model checking for Markov regenerative processes based on stochastic state classes. M15, UFi, UTo.21. Models for the evaluation of clouds and WSN. M15, UMe.22. Extension of the mean-field analysis technique to include mixed continuous-discrete state spaces. M18, PMi.23. Development and implementation design of en efficient algorithm for model checking CSL-TA. M18, UTo.24. Novel methods of distributions and process approximation with matrix exponential distributions and processes. M18, UTo, PMi.25. Use of stratified sampling in statistical model checking. M20, UFi, UTo.26. Compositional specifications and reasoning for non-Markovian models. M20, UFi.27. Definition of a specific application setting and set up of test bed for an online monitoring infrastructure. M24, UFi.28. Identification and/or development of techniques for abstraction based verification of non-Markovian models. M24. UTo.29. Definition of a specific application setting and set up of test bed for a development process of real time SW. M24, UFi.30. Model definition for diffusion of business organization models. M26, UTo.31. Application of the techniques developed in WP2 for the analysis clouds and WSN. M30, UMe.32. Lessons learnt by the application of Markovianization techniques for the analysis of WSM and clouds. M30, UMe, UTo, PMi.33. Lessons learnt by the application of approximate technique for non-Markovian models in the analysis of WSM and clouds. M30, UMe, UFi, PMi.34. Lessons learnt by the application of model checking techniques in the analysis of WSM. M30, UMe, UFi, PTo.35. Analysis of the model of diffusion of business organization models. M32, UTo, PMi.36. Exploitation of the analysis of clouds for their design and maintenance. M36, UMe.37. Exploitation of the analysis of SWN for their design and maintenance. M36, UMe.38. Application of model checking techniques for the online monitoring infrastructure. M36, UFi, UTo.39. Application of model checking techniques in the development process of real time SW. M36, UFi, UTo.40. Application of non-Markovian preemptive models in the development process of real time SW. M36, UFi, UTo, UMe.

Moreover, manuals and progress reports will be written to monitor the development of tools.

2. Adopted work methodology

The credibility of efforts carried out in the project will be increased by the creation of test beds and benchmark. These will not only provide a direct platform for theunits to test their own techniques and tools but it will open the door to researchers directly not involved in the project to probe and compare the provided scientificand practical advances.

3. Financial issues

During the creation of the budget we have considered the current financial situation. Indeed, it is foreseen that a significant portion of the budget is used to hireyoung researchers. We kept low the budget per unit and this way we were able to include four units with a total of 20 researchers in the project proposal. Thisattention will be maintained during the project as well. When possible, meetings and cooperation will be carried out without using the resources of the project.

4. Quality of the scientific implications of the work

Quantity and quality of the scientific publications produced by the units, documenting the results achieved during the research activities, will be monitored. Thequality of the publications can be assessed through citation counting metrics and by their editorial location. The number of participants not belonging to the scientificcommunity directly involved in the project will be a metric to evaluate the interest gathered for the achieved results. Possible cooperation with international researchthat will emerge during the research activities will be a further project assessment metric.

5. Visibility of the obtained results

To expose directly the project activities in the scientific and industrial communities, and to allow point to point checking of the project progresses, a project web sitewill be prepared. This site will include a public part devoted to show the achieved results and a reserved one for the project partners used for exchanging of the workmaterial. The site will contain the deliverables and highlight the accepted and submitted publications. To extend the knowledge on the topics of the project, the website will contain an extensive and commented bibliography on the subjects of the project.

Other salient aspects

The project will promote the exchange and integration of complementary knowledge among the involved units, thanks to its multi-topic structure (involving bothmethodological and applicative knowledge).

Young researchers employed through research contracts will benefit in terms of skills' acquisition and higher level of professionalism acquired, through theirparticipation to the project activities, including the significant hands-on experimental work.

The experimental activities will also affect the contents of the academic teaching programs and laboratory classes.

29

17 - Riassunto Spese delle Unità di Ricercanº Responsabile

scientificoSpesaA.1.1

SpesaA.1.2

SpesaA.2

Spesa B SpesaC.1

SpesaC.2

Spesa D Spesa E Spesa F Spesa G TOTALE

1. HORVATHAndras

98.662 0 86.000 110.797 0 0 4.000 30.000 0 0 329.459

2. GRIBAUDOMarco

56.842 0 55.000 67.105 0 0 2.000 10.000 0 0 190.947

3. BRUNEODario

64.842 0 0 124.705 143.000 0 5.000 22.000 0 0 359.547

4. LORETIMichele

93.152 0 80.000 103.891 0 0 5.000 30.000 3.000 1.000 316.043

TOTALE 313.498 0 221.000 406.498 143.000 0 16.000 92.000 3.000 1.000 1.195.996

Legenda voce di spesa:-Spesa A: Spese di personale (A.1.1 dipendente a tempo indeterminato; A.1.2 dipendente a tempo determinato; A.2 personale non dipendente, esclusi i contratti pergiovani ricercatori e/o ricercatori di chiara fama internazionale di cui alla voce C)-Spesa B: Spese generali direttamente imputabili all'attività di ricerca (obbligatoriamente nella misura forfettizzata del 60% del costo del personale di cui alle voci A eC)-Spesa C: Spese per contratti almeno triennali per giovani ricercatori (C.1) ed almeno semestrali per ricercatori di chiara fama internazionale (C.2)-Spesa D: Spese per l'acquisizione di strumentazioni, attrezzature e prodotti software-Spesa E: Spese per stage e missioni all'estero di docenti/ricercatori coinvolti nel progetto-Spesa F: Costo dei servizi di consulenza e simili utilizzati per l'attività di ricerca-Spesa G: Altri costi di esercizio direttamente imputabili all'attività di ricerca

18 - Informazioni generali e durata del progettoDurata del Progetto di Ricerca 36 Mesi

Mesi/persona complessivi dedicati al Progetto di Ricerca 240

Costo totale del Progetto 1.195.996

Finanziamento richiesto 737.097

Numero di contratti per giovani ricercatori 1

Costo totale 143.000

Numero di contratti per ricercatori di chiara fama 0

Costo totale 0

19 - Costo complessivo del Progetto di Ricerca risorse disponibilinº Responsabile scientifico Risorse finanziarie

richieste al MIURGiovani

ricercatoriRicercatori dichiara fama

internazionale

Costo totale dellaproposta

progettuale1. HORVATH Andras 230.621 0 0 329.459

2. GRIBAUDO Marco 133.663 0 0 190.947

3. BRUNEO Dario 151.583 143.000 0 359.547

4. LORETI Michele 221.230 0 0 316.043

TOTALE 737.097 143.000 0 1.195.996

A carico del MIUR A carico del Proponente TOTALECosto delle attività di ricerca 737.097 315.899 1.052.996Costo dei contratti dei giovani ricercatori 143.000 143.000Costo dei contratti dei ricercatori di chiara fama 0 0Costo complessivo dell'Unità di Ricerca 880.097 315.899 1.195.996

Si ricorda che il cofinanziamento a carico del proponente deve essere pari al 30% del costo complessivo del progetto di Ricerca, detratti i costi dei contratti triennaliper giovani ricercatori e per ricercatori di chiara fama, che sono finanziati al 100%.

I dati contenuti nella domanda di finanziamento sono trattati esclusivamente per lo svolgimento delle funzioni istituzionali del MIUR. Incaricato del trattamento è ilCINECA- Dipartimento Servizi per il MIUR. La consultazione è altresì riservata al MIUR - D.G. della Ricerca -- Ufficio V, alla Commissione FIRB e ai refereescientifici. Il MIUR potrà anche procedere alla diffusione dei principali dati economici e scientifici relativi ai progetti finanziati.

30

Firma del Coordinatore ............................. Data........... (inserita dal sistema al termine della redazione della domanda)

31

MINISTERO DELL'ISTRUZIONE, DELL'UNIVERSITÀ E DELLA …horvath/firb2010/final/all.pdfMINISTERO...

Documents

Transcript of MINISTERO DELL'ISTRUZIONE, DELL'UNIVERSITÀ E DELLA …horvath/firb2010/final/all.pdfMINISTERO...