
T. Mancini, E. Tronci, A. Scialanca, F. Lanciotti, A. Finzi, R. Guarneri, and S. Di Pompeo. "Optimal FaultTolerant Placement of Relay Nodes in a Mission Critical Wireless Network." In 25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018)., 2018. DOI: 10.29007/grw9.



T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, S. Sinisi, E. Tronci, R. Ehrig, S. RÃ¶blitz, and B. Leeners. "Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction." In 25th RCRA International Workshop on “Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion” (RCRA 2018)., 2018. DOI: 10.29007/g864.



S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, and B. Leeners. "Complete populations of virtual patients for in silico clinical trials." Bioinformatics (2021): 1–8. ISSN: 13674803. DOI: 10.1093/bioinformatics/btaa1026.
Abstract: Modelbased 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 nonidentifiable 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 (nonidentifiable) 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 userprovided criteria. This enables full granularity control on the size of the population to employ in an ISCT, guaranteeing representativeness while avoiding overrepresentation of behaviours.We proved the effectiveness of our algorithm on a nonidentifiable ODEbased model of the female HypothalamicPituitaryGonadal 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).



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



S. Sinisi, V. Alimguzhin, T. Mancini, and E. Tronci. "Reconciling interoperability with efficient Verification and Validation within open source simulation environments." Simulation Modelling Practice and Theory (2021): 102277. ISSN: 1569190x. DOI: 10.1016/j.simpat.2021.102277.
Abstract: A CyberPhysical System (CPS) comprises physical as well as software subsystems. Simulationbased 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 simulationbased 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 Mockup Interface (FMI) has been proposed as an open standard to support both Model Exchange (ME) and CoSimulation (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 Mockup Units (FMUs). Indeed FMUs play an essential role in defining complex CPSs through, e.g., the System Structure and Parametrization (SSP) standard. Simulationbased 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 simulationbased 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 opensource simulation environments. This motivates developing such a feature for opensource CPS simulation environments. Accordingly, in this paper, we focus on JModelica, an opensource modelling and simulation environment for CPSs based on an open standard modelling language, namely Modelica. We describe how we have endowed JModelica with our opensource 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 simulationbased V&V is, on average, 22 times faster with our get/set functionality than without it.
Keywords: Simulation, Verification and Validation, Interoperability, FMI/FMU, Model Exchange, CyberPhysical Systems



I. Melatti, F. Mari, T. Mancini, M. Prodanovic, and E. Tronci. "A TwoLayer NearOptimal Strategy for Substation Constraint Management via Home Batteries." IEEE Transactions on Industrial Electronics (2021): 1. Notes: To appear. DOI: 10.1109/TIE.2021.3102431.
Abstract: Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and useroblivious substation constraints management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy. We present a novel twolayer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields nearoptimal substation constraints management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraints management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy.



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.



Adolfo Piperno, and Enrico Tronci. "Regular Systems of Equations in λcalculus." Int. J. Found. Comput. Sci. 1, no. 3 (1990): 325–340. DOI: 10.1142/S0129054190000230.
Abstract: Many problems arising in equational theories like Lambdacalculus 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 wellknown properties of Lambdacalculus 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.



Roberto Gorrieri, Ruggero Lanotte, Andrea MaggioloSchettini, Fabio Martinelli, Simone Tini, and Enrico Tronci. "Automated analysis of timed security: a case study on web privacy." International Journal of Information Security 2, no. 34 (2004): 168–186. DOI: 10.1007/s1020700400379.
Abstract: This paper presents a case study on an automated analysis of realtime 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: LHTimed Automata (analyzed using the model checker HyTech), finitestate automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWBNC). A comparative analysis of these three approaches is given.



Federico Mari, Igor Melatti, Enrico Tronci, and Alberto Finzi. "A multihop advertising discovery and delivering protocol for multi administrative domain MANET." Mobile Information Systems 3, no. 9 (2013): 261–280. IOS Press. ISSN: 1574017x (Print) 1875905X (Online). DOI: 10.3233/MIS130162.

