| |
Records |
Links |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier |
Type |
Journal Article |
| |
Year |
2006 |
Publication |
Int. J. Softw. Tools Technol. Transf. |
Abbreviated Journal |
|
|
| |
Volume |
8 |
Issue |
4 |
Pages  |
397-409 |
|
| |
Keywords |
|
|
| |
Abstract |
In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems). |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer-Verlag |
Place of Publication |
Berlin, Heidelberg |
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
1433-2779 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Dimtz06 |
Serial |
78 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier |
Type |
Conference Article |
| |
Year |
2003 |
Publication |
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
394-409 |
|
| |
Keywords |
|
|
| |
Abstract |
In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems). |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
Geist, D.; Tronci, E. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2860 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Dimtz03 |
Serial |
84 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe |
|
| |
Title |
Disk Based Software Verification via Bounded Model Checking |
Type |
Conference Article |
| |
Year |
2007 |
Publication |
APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
358-365 |
|
| |
Keywords |
|
|
| |
Abstract |
One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, DC, USA |
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
0-7695-3057-5 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Bmtd07 |
Serial |
76 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso |
|
| |
Title |
Xere: Towards a Natural Interoperability between XML and ER Diagrams |
Type |
Conference Article |
| |
Year |
2003 |
Publication |
Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
356-371 |
|
| |
Keywords |
|
|
| |
Abstract |
XML (eXtensible Markup Language) is becoming the standard format for documents on Internet and is widely used to exchange data. Often, the relevant information contained in XML documents needs to be also stored in legacy databases (DB) in order to integrate the new data with the pre-existing ones. In this paper, we introduce a technique for the automatic XML-DB integration, which we call Xere. In particular we present, as the first step of Xere, the mapping algorithm which allows the translation of XML Schemas into Entity-Relationship diagrams. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
Pezzè, M. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2621 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-00899-3 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Ddimp03 |
Serial |
86 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems |
Type |
Journal Article |
| |
Year |
2004 |
Publication |
Sttt |
Abbreviated Journal |
|
|
| |
Volume |
6 |
Issue |
4 |
Pages |
320-341 |
|
| |
Keywords |
|
|
| |
Abstract |
In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms. We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Mur$\varphi$ verifier distribution. We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Mur$\varphi$ verifier. Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Mur$\varphi$ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Mur$\varphi$ was able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 GB of memory using standard Mur$\varphi$. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ DIMTZ04j |
Serial |
91 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
|
| |
Title |
An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks |
Type |
Conference Article |
| |
Year |
2018 |
Publication |
Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
302-312 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
|
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
Best Paper |
Approved |
no |
|
| |
Call Number |
MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 |
Serial |
176 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico |
|
| |
Title |
System Level Formal Verification via Model Checking Driven Simulation |
Type |
Conference Article |
| |
Year |
2013 |
Publication |
Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia |
Abbreviated Journal |
CAV 2013 |
|
| |
Volume |
|
Issue |
|
Pages |
296-312 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
8044 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
0302-9743 |
ISBN |
978-3-642-39798-1 |
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ |
Serial |
113 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Tofani, Alberto; Pecorari, Marcello; Raparelli, Orazio; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico |
|
| |
Title |
A Case Study on Automated Generation of Integration Tests |
Type |
Conference Article |
| |
Year |
2006 |
Publication |
Fdl |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
278-284 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Ecsi |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-3-00-019710-9 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Dtprimt06 |
Serial |
27 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier |
Type |
Conference Article |
| |
Year |
2003 |
Publication |
Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
277-282 |
|
| |
Keywords |
|
|
| |
Abstract |
We present a verification algorithm that can automatically switch from RAM based verification to disk based verification without discarding the work done during the RAM based verification phase. This avoids having to choose beforehand the proper verification algorithm. Our experimental results show that typically our integrated algorithm is as fast as (sometime faster than) the fastest of the two base (i.e. RAM based and disk based) verification algorithms. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
|
Editor |
Geist, D.; Tronci, E. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2860 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-20363-X |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ DIMTZ03a |
Serial |
85 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto |
|
| |
Title |
A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET |
Type |
Journal Article |
| |
Year |
2013 |
Publication |
Mobile Information Systems |
Abbreviated Journal |
Mobile Information Systems |
|
| |
Volume |
3 |
Issue |
9 |
Pages |
261-280 |
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IOS Press |
Place of Publication |
|
Editor |
|
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
1574-017x (Print) 1875-905X (Online) |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
no |
|
| |
Call Number |
Sapienza @ melatti @ |
Serial |
109 |
|
| Permanent link to this record |
