|   | 
Details
   web
Records
Author Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
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 (down) 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
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 (down) 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 Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title On Checking Equivalence of Simulation Scripts Type Journal Article
Year 2021 Publication Journal of Logical and Algebraic Methods in Programming Abbreviated Journal
Volume Issue Pages 100640
Keywords Formal verification, Simulation based formal verification, Formal Verification of cyber-physical systems, System-level formal verification
Abstract To support Model Based Design of Cyber-Physical Systems (CPSs) many simulation based approaches to System Level Formal Verification (SLFV) have been devised. Basically, these are Bounded Model Checking approaches (since simulation horizon is of course bounded) relying on simulators to compute the system dynamics and thereby verify the given system properties. The main obstacle to simulation based SLFV is the large number of simulation scenarios to be considered and thus the huge amount of simulation time needed to complete the verification task. To save on computation time, simulation based SLFV approaches exploit the capability of simulators to save and restore simulation states. Essentially, such a time saving is obtained by optimising the simulation script defining the simulation activity needed to carry out the verification task. Although such approaches aim to (bounded) formal verification, as a matter of fact, the proof of correctness of the methods to optimise simulation scripts basically relies on an intuitive semantics for simulation scripting languages. This hampers the possibility of formally showing that the optimisations introduced to speed up the simulation activity do not actually omit checking of relevant behaviours for the system under verification. The aim of this paper is to fill the above gap by presenting an operational semantics for simulation scripting languages and by proving soundness and completeness properties for it. This, in turn, enables formal proofs of equivalence between unoptimised and optimised simulation scripts.
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 (down) 2352-2208 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Mancini2021100640 Serial 183
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Synthesizing Control Software from Boolean Relations Type Journal Article
Year 2012 Publication International Journal on Advances in Software Abbreviated Journal Intern. Journal on Advances in SW
Volume vol. 5, nr 3&4 Issue Pages 212-223
Keywords Control Software Synthesis; Embedded Systems; Model Checking
Abstract Many software as well digital hardware automatic
synthesis methods define the set of
implementations meeting the given system
specifications with a boolean relation K. In
such a context a fundamental step in the software
(hardware) synthesis process is finding effective
solutions to the functional equation defined by
K. This entails finding a (set of) boolean
function(s) F (typically represented using
OBDDs, Ordered Binary Decision Diagrams)
such that: 1) for all x for which K is
satisfiable, K(x, F(x)) = 1 holds; 2) the
implementation of F is efficient with respect
to given implementation parameters such as code
size or execution time. While this problem has
been widely studied in digital hardware synthesis,
little has been done in a software synthesis
context. Unfortunately, the approaches developed
for hardware synthesis cannot be directly used in
a software context. This motivates investigation
of effective methods to solve the above problem
when F has to be implemented with software. In
this paper, we present an algorithm that, from an
OBDD representation for K, generates a C code
implementation for F that has the same size as
the OBDD for F and a worst case execution time
linear in nr, being n = |x| the number of
input arguments for functions in F and r the
number of functions in F. Moreover, a formal
proof of the proposed algorithm correctness is
also shown. Finally, we present experimental
results showing effectiveness of the proposed
algorithm.
Address
Corporate Author Thesis
Publisher IARIA Place of Publication Editor Luigi Lavazza
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (down) 1942-2628 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ melatti @ Serial 108
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems Type Journal Article
Year 2013 Publication International Journal on Advances in Software Abbreviated Journal Intern. Journal on Advances in SW
Volume vol. 6, nr 1&2 Issue Pages 155-169
Keywords Model-based software design; Linear predicates; Hybrid systems
Abstract Model based design is particularly appealing in
software based control systems (e.g., embedded
software) design, since in such a case system
level specifications are much easier to define
than the control software behavior itself. In
turn, model based design of embedded systems
requires modeling both continuous subsystems
(typically, the plant) as well as discrete
subsystems (the controller). This is typically
done using hybrid systems. Mixed Integer Linear
Programming (MILP) based abstraction techniques
have been successfully applied to automatically
synthesize correct-by-construction control
software for discrete time linear hybrid systems,
where plant dynamics is modeled as a linear
predicate over state, input, and next state
variables. Unfortunately, MILP solvers require
such linear predicates to be conjunctions of
linear constraints, which is not a natural way of
modeling hybrid systems. In this paper we show
that, under the hypothesis that each variable
ranges over a bounded interval, any linear
predicate built upon conjunction and disjunction
of linear constraints can be automatically
translated into an equivalent conjunctive
predicate. Since variable bounds play a key role
in this translation, our algorithm includes a
procedure to compute all implicit variable bounds
of the given linear predicate. Furthermore, we
show that a particular form of linear predicates,
namely guarded predicates, are a natural and
powerful language to succinctly model discrete
time linear hybrid systems dynamics. Finally, we
experimentally show the feasibility of our
approach on an important and challenging case
study taken from the literature, namely the
multi-input Buck DC-DC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6-inputs Buck DC-DC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes.
Address
Corporate Author Thesis
Publisher IARIA Place of Publication Editor Luigi Lavazza
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN (down) 1942-2628 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ melatti @ Serial 115
Permanent link to this record
 

 
Author Mancini, T.; Melatti, I.; Tronci, E.
Title Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification Type Journal Article
Year 2021 Publication IEEE Transactions on Software Engineering Abbreviated Journal
Volume Issue Pages 1-1
Keywords
Abstract Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.
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 (down) 1939-3520 ISBN Medium
Area Expedition Conference
Notes To appear Approved no
Call Number MCLab @ davi @ ref9527998 Serial 191
Permanent link to this record
 

 
Author Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B.
Title Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins Type Journal Article
Year 2020 Publication Abbreviated Journal Fundamenta Informaticae
Volume 174 Issue Pages 283-310
Keywords Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation
Abstract In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.
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 (down) 1875-8681 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 187
Permanent link to this record
 

 
Author Chen, Q.M.; Finzi, A.; Mancini, T.; Melatti, I.; Tronci, E.
Title MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks Type Journal Article
Year 2020 Publication Abbreviated Journal Fundamenta Informaticae
Volume 174 Issue Pages 229-258
Keywords
Abstract In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes . As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance. In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance ). We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.
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 (down) 1875-8681 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 188
Permanent link to this record
 

 
Author Fischer, S.; Ehrig, R.; Schaefer, S.; Tronci, E.; Mancini, T.; Egli, M.; Ille, F.; Krueger, T.H.C.; Leeners, B.; Roeblitz, S.
Title Mathematical Modeling and Simulation Provides Evidence for New Strategies of Ovarian Stimulation Type Journal Article
Year 2021 Publication Frontiers in Endocrinology Abbreviated Journal
Volume 12 Issue Pages 117
Keywords
Abstract New approaches to ovarian stimulation protocols, such as luteal start, random start or double stimulation, allow for flexibility in ovarian stimulation at different phases of the menstrual cycle. It has been proposed that the success of these methods is based on the continuous growth of multiple cohorts (“waves”) of follicles throughout the menstrual cycle which leads to the availability of ovarian follicles for ovarian controlled stimulation at several time points. Though several preliminary studies have been published, their scientific evidence has not been considered as being strong enough to integrate these results into routine clinical practice. This work aims at adding further scientific evidence about the efficiency of variable-start protocols and underpinning the theory of follicular waves by using mathematical modeling and numerical simulations. For this purpose, we have modified and coupled two previously published models, one describing the time course of hormones and one describing competitive follicular growth in a normal menstrual cycle. The coupled model is used to test ovarian stimulation protocols in silico. Simulation results show the occurrence of follicles in a wave-like manner during a normal menstrual cycle and qualitatively predict the outcome of ovarian stimulation initiated at different time points of the menstrual cycle.
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 (down) 1664-2392 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ ref10.3389/fendo.2021.613048 Serial 189
Permanent link to this record
 

 
Author Leeners, B.; Krueger, T.H.C.; Geraedts, K.; Tronci, E.; Mancini, T.; Egli, M.; Roeblitz, S.; Saleh, L.; Spanaus, K.; Schippert, C.; Zhang, Y.; Ille, F.
Title Associations Between Natural Physiological and Supraphysiological Estradiol Levels and Stress Perception Type Journal Article
Year 2019 Publication Frontiers in Psychology Abbreviated Journal
Volume 10 Issue Pages 1296
Keywords
Abstract Stress is a risk factor for impaired general, mental and reproductive health. The role of physiological and supraphysiological estradiol concentrations in stress perception and stress processing is less well understood. We therefore, conducted a prospective observational study to investigate the association between estradiol, stress perception and stress-related cognitive performance within serial measurements either during the natural menstrual cycle or during fertility treatment, where estradiol levels are strongly above the physiological level of a natural cycle and consequently, represent a good model to study dose-dependent effects of estradiol. Data from 44 women receiving in vitro fertilization at the Department of Reproductive Endocrinology in Zurich, Switzerland was compared to data from 88 women with measurements during their natural menstrual cycle. The german version of the Perceived Stress Questionnaire (PSQ) and the Cognitive Bias Test (CBT), in which cognitive performance is tested under time stress were used to evaluate subjective and functional aspects of stress. Estradiol levels were investigated at four different time points during the menstrual cycle and at two different time points during a fertility treatment. Cycle phase were associated with PSQ worry and cognitive bias in normally cycling women, but different phases of fertility treatment were not associated with subjectively perceived stress and stress-related cognitive bias. PSQ lack of joy and PSQ demands related to CBT in women receiving fertility treatment but not in women with a normal menstrual cycle. Only strong changes of the estradiol level during fertility treatment were weakly associated with CBT, but not with subjectively experienced stress. Our research emphasises the multidimensional character of stress and the necessity to adjust stress research to the complex nature of stress perception and processing. Infertility is associated with an increased psychological burden in patients. However, not all phases of the process to overcome infertility do significantly increase patient stress levels. Also, research on the psychological burden of infertility should consider that stress may vary during the different phases of fertility treatment.
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 (down) 1664-1078 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ ref10.3389/fpsyg.2019.01296 Serial 178
Permanent link to this record