IRIS Institutional Research Information System - AIR Archivio Istituzionale della Ricerca
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Milano.
AIR nasce in UNIMI nel 2006 con lo scopo di raccogliere, documentare e conservare le informazioni sulla produzione scientifica dell'Università degli Studi di Milano e costituisce di fatto l'Anagrafe della ricerca dell'Ateneo.
EnglishThe recent extensive availability of 'cloud' computing platforms is very appealing for the formal verification community. In fact, these platforms represent a great opportunity to run massively parallel jobs and analyze 'big data' problems, although classical formal verification tools and techniques must undergo a deep technological transformation to take advantage of the available powerful architectures. A distributed approach to verification of computation tree logic formulas on very large state spaces is described. The approach exploits and integrates our parametric state-space builder, designed to ease the adoption of 'big data' platforms. The whole framework adopts a MAPREDUCEapproach as the core computational model and can be tailored to different modeling formalisms. This paper includes proofs of correctness, a short theoretical discussion about complexity, and reports a practical experience with some benchmarking Petri net models. The outcomes of several tests are presented, thus showing the convenience of the proposed approach.
Distributed CTL model checking using MapReduce : theory and practice / C. Bellettini, M. Camilli, L. Capra, M. Monga. - In: CONCURRENCY AND COMPUTATION. - ISSN 1532-0626. - 28:11(2016), pp. 3025-3041.
| Titolo: | Distributed CTL model checking using MapReduce : theory and practice |
| Autori: | BELLETTINI, CARLO NICOLA MARIA (Primo) CAPRA, LORENZO (Penultimo) MONGA, MATTIA (Ultimo) |
| Parole Chiave: | Cloud computing; CTL; Distributed algorithms; Formal verification; MapReduce; Computer Networks and Communications; Computer Science Applications1707 Computer Vision and Pattern Recognition; Software; Computational Theory and Mathematics; Theoretical Computer Science |
| Settore Scientifico Disciplinare: | Settore INF/01 - Informatica |
| Data di pubblicazione: | 2016 |
| Rivista: | |
| Tipologia: | Article (author) |
| Data ahead of print / Data di stampa: | 20-set-2015 |
| Digital Object Identifier (DOI): | http://dx.doi.org/10.1002/cpe.3652 |
| Appare nelle tipologie: | 01 - Articolo su periodico |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| Bellettini_et_al-2015-Concurrency_and_Computation-_Practice_and_Experience.pdf | Publisher's version/PDF | Administrator Richiedi una copia |
http://hdl.handle.net/2434/365774
Copyright © 2020