|   | 
Details
   web
Records
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 (down) 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
 

 
Author Maggioli, F.; Mancini, T.; Tronci, E.
Title SBML2Modelica: Integrating biochemical models within open-standard simulation ecosystems Type Journal Article
Year 2019 Publication Bioinformatics Abbreviated Journal
Volume 36 Issue (down) 7 Pages 2165–2172
Keywords
Abstract SBML is the most widespread language for the definition of biochemical models. Although dozens of SBML simulators are available, there is a general lack of support to the integration of SBML models within open-standard general-purpose simulation ecosystems. This hinders co-simulation and integration of SBML models within larger model networks, in order to, e.g., enable in-silico clinical trials of drugs, pharmacological protocols, or engineering artefacts such as biomedical devices against Virtual Physiological Human models.Modelica is one of the most popular existing open-standard general-purpose simulation languages, supported by many simulators. Modelica models are especially suited for the definition of complex networks of heterogeneous models from virtually all application domains. Models written in Modelica (and in 100+ other languages) can be readily exported into black-box Functional Mock-Up Units (FMUs), and seamlessly co-simulated and integrated into larger model networks within open-standard language-independent simulation ecosystems.In order to enable SBML model integration within heterogeneous model networks, we present SBML2Modelica, a software system translating SBML models into well-structured, user-intelligible, easily modifiable Modelica models. SBML2Modelica is SBML Level 3 Version 2 -compliant and succeeds on 96.47% of the SBML Test Suite Core (with a few rare, intricate, and easily avoidable combinations of constructs unsupported and cleanly signalled to the user). Our experimental campaign on 613 models from the BioModels database (with up to 5438 variables) shows that the major open-source (general-purpose) Modelica and FMU simulators achieve performance comparable to state-of-the-art specialised SBML simulators.SBML2Modelica is written in Java and is freely available for non-commercial use at https://bitbucket.org/mclab/sbml2modelica
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 1367-4803 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ ref10.1093/bioinformatics/btz860 Serial 179
Permanent link to this record
 

 
Author Pappagallo, A.; Massini, A.; Tronci, E.
Title Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review Type Journal Article
Year 2020 Publication Information Abbreviated Journal
Volume 11 Issue (down) 558 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 181
Permanent link to this record
 

 
Author Tronci, Enrico
Title Introductory Paper Type Journal Article
Year 2006 Publication Sttt Abbreviated Journal
Volume 8 Issue (down) 4-5 Pages 355-358
Keywords
Abstract In today’s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21–24 October 2003 in L’Aquila, Italy. Authors of well regarded papers from CHARME’03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.
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 @ sttt06 Serial 30
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 Journal Article
Year 2006 Publication Int. J. Softw. Tools Technol. Transf. Abbreviated Journal
Volume 8 Issue (down) 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 Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems Type Journal Article
Year 2004 Publication Sttt Abbreviated Journal
Volume 6 Issue (down) 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 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 (down) 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 Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico
Title Automated analysis of timed security: a case study on web privacy Type Journal Article
Year 2004 Publication International Journal of Information Security Abbreviated Journal
Volume 2 Issue (down) 3-4 Pages 168-186
Keywords
Abstract This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given.
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 @ ijis04 Serial 33
Permanent link to this record
 

 
Author Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele
Title Fluid Petri Nets and hybrid model checking: a comparative case study Type Journal Article
Year 2003 Publication Int. Journal on: Reliability Engineering & System Safety Abbreviated Journal
Volume 81 Issue (down) 3 Pages 239-257
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 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 (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a ’real world’ hybrid system: the temperature control system of a co-generative plant.
Address
Corporate Author Thesis
Publisher Elsevier 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 @ ress03 Serial 40
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title Regular Systems of Equations in λ-calculus Type Journal Article
Year 1990 Publication Int. J. Found. Comput. Sci. Abbreviated Journal
Volume 1 Issue (down) 3 Pages 325-340
Keywords
Abstract Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
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 @ ijfcs90 Serial 60
Permanent link to this record