Records |
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, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
Title |
Anytime system level verification via parallel random exhaustive hardware in the loop simulation |
Type |
Journal Article |
Year |
2016 |
Publication |
Microprocessors and Microsystems |
Abbreviated Journal |
|
Volume |
41 |
Issue |
|
Pages |
12-28 |
Keywords |
Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation |
Abstract |
Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability. |
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 |
0141-9331 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
MCLab @ davi @ Mancini201612 |
Serial |
155 |
Permanent link to this record |
|
|
|
Author |
Alimguzhin, V.; Mari, F.; Melatti, I.; Tronci, E.; Ebeid, E.; Mikkelsen, S.A.; Jacobsen, R.H.; Gruber, J.K.; Hayes, B.; Huerta, F.; Prodanovic, M. |
Title |
A Glimpse of SmartHG Project Test-bed and Communication Infrastructure |
Type |
Conference Article |
Year |
2015 |
Publication |
Digital System Design (DSD), 2015 Euromicro Conference on |
Abbreviated Journal |
|
Volume |
|
Issue |
|
Pages |
225-232 |
Keywords |
Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis |
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 |
Sapienza @ preissler @ Alimguzhin_etal2015 |
Serial |
127 |
Permanent link to this record |
|
|
|
Author |
Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico |
Title |
Simulator Semantics for System Level Formal Verification |
Type |
Conference Article |
Year |
2015 |
Publication |
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), |
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 |
125 |
Permanent link to this record |
|
|
|
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 |
Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
Title |
Linearising Discrete Time Hybrid Systems |
Type |
Journal Article |
Year |
2017 |
Publication |
IEEE Transactions on Automatic Control |
Abbreviated Journal |
|
Volume |
62 |
Issue |
10 |
Pages |
5357-5364 |
Keywords |
|
Abstract |
Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool. |
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 |
0018-9286 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
no |
Call Number |
Sapienza @ mari @ ref7902199 |
Serial |
164 |
Permanent link to this record |
|
|
|
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 |
Intrigila, Benedetto; Melatti, Igor; Tofani, Alberto; Macchiarelli, Guido |
Title |
Computational models of myocardial endomysial collagen arrangement |
Type |
Journal Article |
Year |
2007 |
Publication |
Computer Methods and Programs in Biomedicine |
Abbreviated Journal |
|
Volume |
86 |
Issue |
3 |
Pages |
232-244 |
Keywords |
|
Abstract |
Collagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude /net extension is intended to model the stress /strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress /strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size. |
Address |
|
Corporate Author |
|
Thesis |
|
Publisher |
Elsevier North-Holland, Inc. |
Place of Publication |
New York, NY, USA |
Editor |
|
Language |
|
Summary Language |
|
Original Title |
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
Series Volume |
|
Series Issue |
|
Edition |
|
ISSN |
0169-2607 |
ISBN |
|
Medium |
|
Area |
|
Expedition |
|
Conference |
|
Notes |
|
Approved |
yes |
Call Number |
Sapienza @ mari @ Imtm07 |
Serial |
82 |
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 |
|
|
|
Author |
Melatti, Igor; Palmer, Robert; Sawaya, Geoffrey; Yang, Yu; Kirby, Robert Mike; Gopalakrishnan, Ganesh |
Title |
Parallel and distributed model checking in Eddy |
Type |
Journal Article |
Year |
2009 |
Publication |
Int. J. Softw. Tools Technol. Transf. |
Abbreviated Journal |
|
Volume |
11 |
Issue |
1 |
Pages |
13-25 |
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 (1) performing overlapped asynchronous message passing, and (2) 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 |
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 @ Mpsykg09 |
Serial |
80 |
Permanent link to this record |