Records |
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico |
Title |
Exploiting Hub States in Automatic Verification |
Type |
Conference Article |
Year |
2005 |
Publication |
Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
54-68 |
Keywords |
|
Abstract |
In this paper we present a new algorithm to counteract state explosion when using Explicit State Space Exploration to verify protocol-like systems. We sketch the implementation of our algorithm within the Caching Mur$\varphi$ verifier and give experimental results showing its effectiveness. We show experimentally that, when memory is a scarce resource, our algorithm improves on the time performances of Caching Mur$\varphi$ verification algorithm, saving between 16% and 68% (45% on average) in computation time. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Springer |
Place of Publication |
|
Editor |
D.A. Peled; Y.-K. Tsay |
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
Series Volume |
3707 |
Series Issue |
|
Edition |
|
ISSN |
3-540-29209-8 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ Dimt04 |
Serial |
83 |
Permanent link to this record |
|
|
|
Author |
Bobbio, Andrea; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico |
Title |
Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections |
Type |
Journal Article |
Year |
2005 |
Publication |
Archives of Transport – International Journal of Transport Problems |
Abbreviated Journal |
|
Volume |
17 |
Issue |
3-4 |
Pages |
|
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 |
yes |
Call Number |
Sapienza @ mari @ jtp05 |
Serial |
31 |
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; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa |
Title |
Synchronized regular expressions |
Type |
Journal Article |
Year |
2003 |
Publication |
Acta Inf. |
Abbreviated Journal |
|
Volume |
39 |
Issue |
1 |
Pages |
31-70 |
Keywords |
|
Abstract |
Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday also increases the need of more powerful tools to interact with texts. Indeed, much work has been done to provide simple and versatile tools that can be useful for the most common text manipulation tasks. Regular Expressions (RE), introduced by Kleene, are well known in the formal language theory. RE have been extended in various ways, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [15] UNIX command, or the Perl [20] language pattern matching constructs) we find backreferences, i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. In this paper we introduce the Synchronized Regular Expressions (SRE) as an extension of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are dealing with formalisms that should have a practical utility and be used in real applications, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user-friendly syntax for SRE to be used in implementations of SRE-powered search algorithms. |
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 @ actainf03 |
Serial |
39 |
Permanent link to this record |
|
|
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
Title |
Model Based Synthesis of Control Software from System Level Formal Specifications |
Type |
Journal Article |
Year |
2014 |
Publication |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Abbreviated Journal |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Volume |
23 |
Issue |
1 |
Pages |
Article 6 |
Keywords |
|
Abstract |
|
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
ACM |
Place of Publication |
|
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
1049-331X |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
Sapienza @ melatti @ |
Serial |
110 |
Permanent link to this record |
|
|
|
Author |
Martinelli, Marco; Tronci, Enrico; Dipoppa, Giovanni; Balducelli, Claudio |
Title |
Electric Power System Anomaly Detection Using Neural Networks |
Type |
Conference Article |
Year |
2004 |
Publication |
8th International Conference on: Knowledge-Based Intelligent Information and Engineering Systems (KES) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
1242-1248 |
Keywords |
|
Abstract |
The aim of this work is to propose an approach to monitor and protect Electric Power System by learning normal system behaviour at substations level, and raising an alarm signal when an abnormal status is detected; the problem is addressed by the use of autoassociative neural networks, reading substation measures. Experimental results show that, through the proposed approach, neural networks can be used to learn parameters underlaying system behaviour, and their output processed to detecting anomalies due to hijacking of measures, changes in the power network topology (i.e. transmission lines breaking) and unexpected power demand trend. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Springer |
Place of Publication |
Wellington, New Zealand |
Editor |
Negoita, M.G.; Howlett, R.J.; Jain, L.C. |
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
Series Volume |
3213 |
Series Issue |
|
Edition |
|
ISSN |
3-540-23318-0 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ kes04 |
Serial |
35 |
Permanent link to this record |
|
|
|
Author |
Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa |
Title |
A Probabilistic Approach to Automatic Verification of Concurrent Systems |
Type |
Conference Article |
Year |
2001 |
Publication |
8th Asia-Pacific Software Engineering Conference (APSEC) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
317-324 |
Keywords |
|
Abstract |
The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead it just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that by using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Macau, China |
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0-7695-1408-1 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ apsec01 |
Serial |
43 |
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 |
Tronci, Enrico |
Title |
Formally Modeling a Metal Processing Plant and its Closed Loop Specifications |
Type |
Conference Article |
Year |
1999 |
Publication |
4th IEEE International Symposium on High-Assurance Systems Engineering (HASE) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
151 |
Keywords |
|
Abstract |
We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design followed by automatic verification. The system to be controlled (plant) models a metal processing facility near Karlsruhe. We succeeded in automatically generating C code implementing a (correct by construction) embedded controller for such a plant from closed loop formal specifications. Our experimental results show that for industrial automation control systems automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design followed by automatic verification. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
IEEE Computer Society |
Place of Publication |
Washington, D.C, USA |
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0-7695-0418-3 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ hase99 |
Serial |
50 |
Permanent link to this record |
|
|
|
Author |
Mancini, T.; Tronci, E.; Scialanca, A.; Lanciotti, F.; Finzi, A.; Guarneri, R.; Di Pompeo, S. |
Title |
Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network |
Type |
Conference Article |
Year |
2018 |
Publication |
25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018) |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
|
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 |
174 |
Permanent link to this record |