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 horvath@di.unito.it

(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

LECTURE NOTES IN COMPUTERSCIENCE

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

PERFORMANCE EVALUATION

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

LECTURE NOTES IN COMPUTERSCIENCE

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

PERFORMANCE EVALUATION

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

LECTURE NOTES IN COMPUTERSCIENCE

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

LECTURE NOTES IN COMPUTERSCIENCE

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

LECTURE NOTES IN COMPUTERSCIENCE

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 752. GRIBAUDO Marco Ricercatore confermato Politecnico di MILANO Dipartimento di ELETTRONICA E INFORMAZIONE 403. BRUNEO Dario Ricercatore confermato Università degli Studi di MESSINA Dipartimento di MATEMATICA 734. 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. Spri