toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links (down)
Author Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti pdf  doi
openurl 
  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 Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele pdf  doi
openurl 
  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 Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso pdf  doi
openurl 
  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 pdf  doi
openurl 
  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 pdf  doi
isbn  openurl
  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 Campagnano, Edoardo; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico pdf  doi
openurl 
  Title Automatic Analysis of a Safety Critical Tele Control System Type Conference Article
  Year 2005 Publication 24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP) Abbreviated Journal  
  Volume Issue Pages 94-107  
  Keywords  
  Abstract We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Fredrikstad, Norway Editor Winther, R.; Gran, B. A.; Dahll, G.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 3688 Series Issue Edition  
  ISSN 3-540-29200-4 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ safecomp05 Serial 32  
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico pdf  doi
openurl 
  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 Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri pdf  openurl
  Title Model Checking Satellite Operational Procedures Type Conference Article
  Year 2011 Publication DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace. Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.  
  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 @ Dasia11 Serial 13  
Permanent link to this record
 

 
Author Mazzini, Silvia; Puri, Stefano; Mari, Federico; Melatti, Igor; Tronci, Enrico pdf  openurl
  Title Formal Verification at System Level Type Conference Article
  Year 2009 Publication In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques.  
  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 @ Dasia09 Serial 20  
Permanent link to this record
 

 
Author Bobbio, Andrea; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico openurl 
  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
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: