| Records |
| Author |
Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti |
| Title |
Computing Biological Model Parameters by Parallel Statistical Model Checking |
Type |
Journal Article |
| Year |
2015 |
Publication |
International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) |
Abbreviated Journal |
|
| Volume |
9044 |
Issue |
|
Pages |
542-554 |
| 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 |
|
Approved |
no |
| Call Number |
MCLab @ davi @ |
Serial |
124 |
| 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 |
Pugliese, Rosario; Tronci, Enrico |
| Title |
Automatic Verification of a Hydroelectric Power Plant |
Type |
Conference Article |
| Year |
1996 |
Publication |
Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3 |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
425-444 |
| Keywords |
|
| Abstract |
We analyze the specification of a hydroelectric power plant by ENEL (the Italian Electric Company). Our goal is to show that for the specification of the plant (its control system in particular) some given properties hold. We were provided with an informal specification of the plant. From such informal specification we wrote a formal specification using the CCS/Meije process algebra formalism. We defined properties using μ-calculus. Automatic verification was carried out using model checking. This was done by translating our process algebra definitions (the model) and μ-calculus formulas into BDDs. In this paper we present the informal specification of the plant, its formal specification, some of the properties we verified and experimental results. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
Oxford, UK |
Editor |
Gaudel, M.-C.; Woodcock, J. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
1051 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-60973-3 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ fme96 |
Serial |
53 |
| Permanent link to this record |
| |
|
| |
| Author |
Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico |
| Title |
A Symbolic Model Checker for ACTL |
Type |
Conference Article |
| Year |
1998 |
Publication |
International Workshop on Current Trends in Applied Formal Method (FM-Trends) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
228-242 |
| Keywords |
|
| Abstract |
We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications). |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
Boppard, Germany |
Editor |
Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
1641 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-66462-9 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ fm-trends98 |
Serial |
51 |
| Permanent link to this record |
| |
|
| |
| Author |
Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele |
| Title |
Model-Checking Based on Fluid Petri Nets for the Temperature Control System of the ICARO Co-generative Plant |
Type |
Conference Article |
| Year |
2002 |
Publication |
21st International Conference on Computer Safety, Reliability and Security (SAFECOMP) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
273-283 |
| Keywords |
|
| Abstract |
The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain for conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPN). It is shown that the same FPN model can be fed to a functional analyser for model checking as well as to a stochastic analyser for performance evaluation. We illustrate our approach and show its usefulness by applying it to a “real world†hybrid system: the temperature control system of a co-generative plant. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
Catania, Italy |
Editor |
Anderson, S.; Bologna, S.; Felici, M. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
2434 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-44157-3 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ safecomp02 |
Serial |
42 |
| Permanent link to this record |
| |
|
| |
| Author |
Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa |
| Title |
Exploiting Transition Locality in Automatic Verification |
Type |
Conference Article |
| Year |
2001 |
Publication |
11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
259-274 |
| Keywords |
|
| Abstract |
In this paper we present an algorithm to contrast state explosion when using Explicit State Space Exploration to verify protocols. We show experimentally that protocols exhibit transition locality. We present a verification algorithm that exploits transition locality as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm is compatible with all Breadth First (BF) optimization techniques present in the Mur$\varphi$ verifier and it is by no means a substitute for any of them. In fact, since our algorithm trades space with time, it is typically most useful when one runs out of memory and has already used all other state reduction techniques present in the Mur$\varphi$ verifier. Our experimental results show that using our approach we can typically save more than 40% of RAM with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
Livingston, Scotland, UK |
Editor |
Margaria, T.; Melham, T.F. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
2144 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-42541-1 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ charme01 |
Serial |
44 |
| Permanent link to this record |
| |
|
| |
| Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Minichino, Michele; Ciancamerla, Ester; Parisse, Andrea; Tronci, Enrico; Venturini Zilli, Marisa |
| Title |
Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier |
Type |
Conference Article |
| Year |
2003 |
Publication |
Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
141-155 |
| Keywords |
|
| Abstract |
Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
|
Editor |
Maler, O.; Pnueli, A. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
2623 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-00913-2 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Dimmcptz03 |
Serial |
88 |
| 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; Tronci, Enrico; Venturini Zilli, Marisa |
| Title |
Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier |
Type |
Conference Article |
| Year |
2002 |
Publication |
4th International Conference on Formal Methods in Computer-Aided Design (FMCAD) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
202-219 |
| Keywords |
|
| Abstract |
The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
Portland, OR, USA |
Editor |
Aagaard, M.; O'Leary, J.W. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
2517 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-00116-6 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ fmcad02 |
Serial |
41 |
| Permanent link to this record |
| |
|
| |
| Author |
Melatti, Igor; Palmer, Robert; Sawaya, Geoffrey; Yang, Yu; Kirby, Robert Mike; Gopalakrishnan, Ganesh |
| Title |
Parallel and Distributed Model Checking in Eddy |
Type |
Conference Article |
| Year |
2006 |
Publication |
Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30 – April 1, 2006, Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
108-125 |
| Keywords |
|
| Abstract |
Model checking of safety properties can be scaled up by pooling the CPU and memory resources of multiple computers. As compute clusters containing 100s of nodes, with each node realized using multi-core (e.g., 2) CPUs will be widespread, a model checker based on the parallel (shared memory) and distributed (message passing) paradigms will more efficiently use the hardware resources. Such a model checker can be designed by having each node employ two shared memory threads that run on the (typically) two CPUs of a node, with one thread responsible for state generation, and the other for efficient communication, including (i) performing overlapped asynchronous message passing, and (ii) aggregating the states to be sent into larger chunks in order to improve communication network utilization. We present the design details of such a novel model checking architecture called Eddy. We describe the design rationale, details of how the threads interact and yield control, exchange messages, as well as detect termination. We have realized an instance of this architecture for the Murphi modeling language. Called Eddy_Murphi, we report its performance over the number of nodes as well as communication parameters such as those controlling state aggregation. Nearly linear reduction of compute time with increasing number of nodes is observed. Our thread task partition is done in such a way that it is modular, easy to port across different modeling languages, and easy to tune across a variety of platforms. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer - Verlag |
Place of Publication |
|
Editor |
Valmari, A. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
3925 |
Series Issue |
|
Edition |
|
| ISSN |
0302-9743 |
ISBN |
978-3-540-33102-5 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Mpsykg06 |
Serial |
81 |
| Permanent link to this record |
