
Giuseppe Della Penna, Antinisca Di Marco, Benedetto Intrigila, Igor Melatti, and Alfonso Pierantonio. "Xere: Towards a Natural Interoperability between XML and ER Diagrams." In 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 711, 2003, Proceedings, edited by M. PezzÃ¨, 356–371. Lecture Notes in Computer Science 2621. Springer, 2003. ISSN: 3540008993. DOI: 10.1007/3540365788_25.
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 preexisting ones. In this paper, we introduce a technique for the automatic XMLDB 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 EntityRelationship diagrams.



Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, and Marisa Venturini Zilli. "Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier." In 4th International Conference on Formal Methods in ComputerAided Design (FMCAD), edited by M. Aagaard and J. W. O'Leary, 202–219. Lecture Notes in Computer Science 2517. Portland, OR, USA: Springer, 2002. ISSN: 3540001166. DOI: 10.1007/354036126X_13.
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$.



T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. "On Checking Equivalence of Simulation Scripts." Journal of Logical and Algebraic Methods in Programming (2021): 100640. ISSN: 23522208. DOI: 10.1016/j.jlamp.2021.100640.
Abstract: To support Model Based Design of CyberPhysical 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.
Keywords: Formal verification, Simulation based formal verification, Formal Verification of cyberphysical systems, Systemlevel formal verification



Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Synthesizing Control Software from Boolean Relations." International Journal on Advances in Software vol. 5, nr 3&4 (2012): 212–223. IARIA. ISSN: 19422628.
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.
Keywords: Control Software Synthesis; Embedded Systems; Model Checking



Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems." International Journal on Advances in Software vol. 6, nr 1&2 (2013): 155–169. IARIA. ISSN: 19422628.
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 correctbyconstruction 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
multiinput Buck DCDC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6inputs Buck DCDC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes.
Keywords: Modelbased software design; Linear predicates; Hybrid systems



T. Mancini, I. Melatti, and E. Tronci. "Anyhorizon uniform random sampling and enumeration of constrained scenarios for simulationbased formal verification." IEEE Transactions on Software Engineering (2021): 1. ISSN: 19393520. Notes: To appear. DOI: 10.1109/TSE.2021.3109842.
Abstract: Modelbased approaches to the verification of nonterminating CyberPhysical 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 simulationbased statistical model checking. Unfortunately, in case of nontrivial 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 anyhorizon 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 simulationbased 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.



S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, F. Mari, and B. Leeners. "Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins." Fundamenta Informaticae 174 (2020): 283–310. IOS Press. ISSN: 18758681. DOI: 10.3233/FI20201943.
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 simulationbased 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.
Keywords: Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation



Q. M. Chen, A. Finzi, T. Mancini, I. Melatti, and E. Tronci. "MILP, PseudoBoolean, and OMT Solvers for Optimal FaultTolerant Placements of Relay Nodes in Mission Critical Wireless Networks." Fundamenta Informaticae 174 (2020): 229–258. IOS Press. ISSN: 18758681. DOI: 10.3233/FI20201941.
Abstract: In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference. Protection of such missioncritical 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 faulttolerance 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 faulttolerance. 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 (faulttolerance ). We show that, by means of a computationintensive preprocessing 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, PBSAT, 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.



S. Fischer, R. Ehrig, S. Schaefer, E. Tronci, T. Mancini, M. Egli, F. Ille, T. H. C. Krueger, B. Leeners, and S. Roeblitz. "Mathematical Modeling and Simulation Provides Evidence for New Strategies of Ovarian Stimulation." Frontiers in Endocrinology 12 (2021): 117. ISSN: 16642392. DOI: 10.3389/fendo.2021.613048.
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 variablestart 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 wavelike manner during a normal menstrual cycle and qualitatively predict the outcome of ovarian stimulation initiated at different time points of the menstrual cycle.



B. Leeners, T. H. C. Krueger, K. Geraedts, E. Tronci, T. Mancini, M. Egli, S. Roeblitz, L. Saleh, K. Spanaus, C. Schippert et al. "Associations Between Natural Physiological and Supraphysiological Estradiol Levels and Stress Perception." Frontiers in Psychology 10 (2019): 1296. ISSN: 16641078. DOI: 10.3389/fpsyg.2019.01296.
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 stressrelated 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 dosedependent 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 stressrelated 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.

