|   | 
Details
   web
Records
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title (down) 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 Maggioli, F.; Mancini, T.; Tronci, E.
Title (down) 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 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 Bobbio, Andrea; Ciancamerla, Ester; Di Blasi, Saverio; Iacomini, Alessandro; Mari, Federico; Melatti, Igor; Minichino, Michele; Scarlatti, Alessandro; Tronci, Enrico; Terruggia, Roberta; Zendri, Emilio
Title (down) Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks Type Conference Article
Year 2009 Publication Proceedings of Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS) Abbreviated Journal
Volume Issue Pages 90-97
Keywords
Abstract The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation.
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 Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS)
Notes Approved yes
Call Number Sapienza @ mari @ crisis09 Serial 17
Permanent link to this record
 

 
Author Hayes, B. P. ; Melatti, I.; Mancini, T.; Prodanovic, M.; Tronci, E.
Title (down) Residential Demand Management using Individualised Demand Aware Price Policies Type Journal Article
Year 2017 Publication IEEE Transactions On Smart Grid Abbreviated Journal
Volume 8 Issue 3 Pages 1284-1294
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 157
Permanent link to this record
 

 
Author Cecconi, Michele; Tronci, Enrico
Title (down) Requirements Formalization and Validation for a Telecommunication Equipment Protection Switcher Type Conference Article
Year 2000 Publication Hase Abbreviated Journal
Volume Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher IEEE Computer Society Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0-7695-0927-4 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ CeTro00 Serial 29
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title (down) Regular Systems of Equations in λ-calculus Type Journal Article
Year 1990 Publication Int. J. Found. Comput. Sci. Abbreviated Journal
Volume 1 Issue 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
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title (down) Regular Systems of Equations in λ-calculus Type Conference Article
Year 1989 Publication Ictcs Abbreviated Journal
Volume Issue Pages
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 Mantova - Italy 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 @ ictcs89 Serial 61
Permanent link to this record
 

 
Author Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.
Title (down) 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 1569-190x ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Sinisi2021102277 Serial 186
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title (down) Quantized Feedback Control Software Synthesis from System Level Formal Specifications for Buck DC/DC Converters Type Report
Year 2011 Publication Abbreviated Journal
Volume abs/1105.5640 Issue Pages
Keywords
Abstract Many Embedded Systems are indeed Software Based Control Systems (SBCSs), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of SBCS control software. In previous works we presented an algorithm, along with a tool QKS implementing it, that from a formal model (as a Discrete Time Linear Hybrid System, DTLHS) of the controlled system (plant), implementation specifications (that is, number of bits in the Analog-to-Digital, AD, conversion) and System Level Formal Specifications (that is, safety and liveness requirements for the closed loop system) returns correct-by-construction control software that has a Worst Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. In this technical report we present full experimental results on using it to synthesize control software for two versions of buck DC-DC converters (single-input and multi-input), a widely used mixed-mode analog circuit.
Address
Corporate Author Thesis
Publisher CoRR, Technical Report 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 @ Serial 106
Permanent link to this record
 

 
Author Tronci, E.; Mancini, T.; Salvo, I.; Mari, F.; Melatti, I.; Massini, A.; Sinisi, S.; Davì, F.; Dierkes, T.; Ehrig, R.; Röblitz, S.; Leeners, B.; Krüger, T.; Egli, M.; Ille, F.
Title (down) Patient-Specific Models from Inter-Patient Biological Models and Clinical Records Type Conference Article
Year 2014 Publication Formal Methods in Computer-Aided Design (FMCAD) 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 Sapienza @ mari @ Serial 120
Permanent link to this record