|   | 
Details
   web
Records
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico
Title System Level Formal Verification via Model Checking Driven Simulation Type Conference Article
Year 2013 Publication Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia Abbreviated Journal CAV 2013
Volume Issue Pages 296-312
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer - Verlag Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 8044 Series Issue Edition
ISSN (up) 0302-9743 ISBN 978-3-642-39798-1 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 113
Permanent link to this record
 

 
Author Intrigila, Benedetto; Salvo, Ivano; Sorgi, Stefano
Title A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser Type Journal Article
Year 2001 Publication Information and Computation Abbreviated Journal
Volume 171 Issue 2 Pages 137-155
Keywords
Abstract Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church-Rosser, CR) and weak confluence (or weak Church-Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the Newmanââ¬â¢s lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties.
Address
Corporate Author Thesis
Publisher Academic Press, Inc. Place of Publication Duluth, MN, USA Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) 0890-5401 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Intrigila-Salvo-Sorgi:01 Serial 68
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico
Title CGMurphi: Automatic synthesis of numerical controllers for nonlinear hybrid systems Type Journal Article
Year 2013 Publication European Journal of Control Abbreviated Journal European Journal of Control
Volume 19 Issue 1 Pages 14-36
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Elsevier North-Holland, Inc. Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (up) 0947-3580 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 114
Permanent link to this record
 

 
Author Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano
Title Intersection types and λ-definability Type Journal Article
Year 2003 Publication Mathematical Structures in Computer Science Abbreviated Journal
Volume 13 Issue 1 Pages 15-53
Keywords
Abstract This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
Address
Corporate Author Thesis
Publisher Cambridge University Press 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 (up) 0960-1295 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03 Serial 69
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 (up) 1049-331X ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 110
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 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 (up) 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 Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Leeners, B.
Title Complete populations of virtual patients for in silico clinical trials Type Journal Article
Year 2021 Publication Bioinformatics Abbreviated Journal
Volume Issue Pages 1-8
Keywords
Abstract Model-based approaches to safety and efficacy assessment of pharmacological drugs, treatment strategies, or medical devices (In Silico Clinical Trial, ISCT) aim to decrease time and cost for the needed experimentations, reduce animal and human testing, and enable precision medicine. Unfortunately, in presence of non-identifiable models (e.g., reaction networks), parameter estimation is not enough to generate complete populations of Virtual Patient (VPs), i.e., populations guaranteed to show the entire spectrum of model behaviours (phenotypes), thus ensuring representativeness of the trial.We present methods and software based on global search driven by statistical model checking that, starting from a (non-identifiable) quantitative model of the human physiology (plus drugs PK/PD) and suitable biological and medical knowledge elicited from experts, compute a population of VPs whose behaviours are representative of the whole spectrum of phenotypes entailed by the model (completeness) and pairwise distinguishable according to user-provided criteria. This enables full granularity control on the size of the population to employ in an ISCT, guaranteeing representativeness while avoiding over-representation of behaviours.We proved the effectiveness of our algorithm on a non-identifiable ODE-based model of the female Hypothalamic-Pituitary-Gonadal axis, by generating a population of 4 830 264 VPs stratified into 7 levels (at different granularity of behaviours), and assessed its representativeness against 86 retrospective health records from Pfizer, Hannover Medical School and University Hospital of Lausanne. The datasets are respectively covered by our VPs within Average Normalised Mean Absolute Error of 15%, 20%, and 35% (90% of the latter dataset is covered within 20% error).
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 (up) 1367-4803 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ ref10.1093/bioinformatics/btaa1026 Serial 182
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 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 (up) 1433-2779 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimtz06 Serial 78
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 (up) 1433-2779 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Mpsykg09 Serial 80
Permanent link to this record
 

 
Author Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.
Title Reconciling interoperability with efficient Verification and Validation within open source simulation environments Type Journal Article
Year 2021 Publication Simulation Modelling Practice and Theory Abbreviated Journal
Volume Issue Pages 102277
Keywords Simulation, Verification and Validation, Interoperability, FMI/FMU, Model Exchange, Cyber-Physical Systems
Abstract A Cyber-Physical System (CPS) comprises physical as well as software subsystems. Simulation-based approaches are typically used to support design and Verification and Validation (V&V) of CPSs in several domains such as: aerospace, defence, automotive, smart grid and healthcare. Accordingly, many simulation-based tools are available to support CPS design. This, on one side, enables designers to choose the toolchain that best suits their needs, on the other side poses huge interoperability challenges when one needs to simulate CPSs whose subsystems have been designed and modelled using different toolchains. To overcome such an interoperability problem, in 2010 the Functional Mock-up Interface (FMI) has been proposed as an open standard to support both Model Exchange (ME) and Co-Simulation (CS) of simulation models created with different toolchains. FMI has been adopted by several modelling and simulation environments. Models adhering to such a standard are called Functional Mock-up Units (FMUs). Indeed FMUs play an essential role in defining complex CPSs through, e.g., the System Structure and Parametrization (SSP) standard. Simulation-based V&V of CPSs typically requires exploring different simulation scenarios (i.e., exogenous input sequences to the CPS under design). Many such scenarios have a shared prefix. Accordingly, to avoid simulating many times such shared prefixes, the simulator state at the end of a shared prefix is saved and then restored and used as a start state for the simulation of the next scenario. In this context, an important FMI feature is the capability to save and restore the internal FMU state on demand. This is crucial to increase efficiency of simulation-based V&V. Unfortunately, the implementation of this feature is not mandatory and it is available only within some commercial software. As a result, the interoperability enabled by the FMI standard cannot be fully exploited for V&V when using open-source simulation environments. This motivates developing such a feature for open-source CPS simulation environments. Accordingly, in this paper, we focus on JModelica, an open-source modelling and simulation environment for CPSs based on an open standard modelling language, namely Modelica. We describe how we have endowed JModelica with our open-source implementation of the FMI 2.0 functions needed to save and restore internal states of FMUs for ME. Furthermore, we present experimental results evaluating, through 934 benchmark models, correctness and efficiency of our extended JModelica. Our experimental results show that simulation-based V&V is, on average, 22 times faster with our get/set functionality than without it.
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 (up) 1569-190x ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Sinisi2021102277 Serial 186
Permanent link to this record