Y. Driouich, M. Parente, and E. Tronci. "Modeling cyberphysical systems for automatic verification." In 14th International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design (SMACD 2017), 1–4., 2017. DOI: 10.1109/SMACD.2017.7981621.
Keywords: cyberphysical systems;formal verification;maximum power point trackers;power engineering computing;Modelica;automatic verification;complex power electronics systems;cyberphysical systems modeling;distributed maximum power point tracking system;open standard modeling language;Computational modeling;Control systems;Integrated circuit modeling;Mathematical model;Maximum power point trackers;Object oriented modeling;Radiation effects;Automatic Formal Verification;CyberPhysical Systems;DMPPT;Modeling;Photovoltaic systems;Simulation;System Analysis and Design

Y. Driouich, M. Parente, and E. Tronci. "A methodology for a complete simulation of CyberPhysical Energy Systems." In EESMS 2018 – Environmental, Energy, and Structural Monitoring Systems, Proceedings, 1–5., 2018. DOI: 10.1109/EESMS.2018.8405826.

T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, M. Prodanovic, and L. Elmegaard. "Parallel Statistical Model Checking for Safety Verification in Smart Grids." In 2018 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm), 1–6., 2018. DOI: 10.1109/SmartGridComm.2018.8587416.

Y. Driouich, M. Parente, and E. Tronci. "Model Checking CyberPhysical Energy Systems." In Proceedings of 2017 International Renewable and Sustainable Energy Conference, IRSEC 2017. Institute of Electrical and Electronics Engineers Inc., 2018. DOI: 10.1109/IRSEC.2017.8477334.

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.

L. Tortora, G. Meynen, J. Bijlsma, E. Tronci, and S. Ferracuti. "Neuroprediction and A.I. in Forensic Psychiatry and Criminal Justice: A Neurolaw Perspective." Frontiers in Psychology 11 (2020): 220. ISSN: 16641078. DOI: 10.3389/fpsyg.2020.00220.
Abstract: Advances in the use of neuroimaging in combination with A.I., and specifically the use of machine learning techniques, have led to the development of brainreading technologies which, in the nearby future, could have many applications, such as lie detection, neuromarketing or braincomputer interfaces. Some of these could, in principle, also be used in forensic psychiatry. The application of these methods in forensic psychiatry could, for instance, be helpful to increase the accuracy of risk assessment and to identify possible interventions. This technique could be referred to as Ã‚â€˜A.I. neuroprediction,Ã‚â€™ and involves identifying potential neurocognitive markers for the prediction of recidivism. However, the future implications of this technique and the role of neuroscience and A.I. in violence risk assessment remain to be established. In this paper, we review and analyze the literature concerning the use of brainreading A.I. for neuroprediction of violence and rearrest to identify possibilities and challenges in the future use of these techniques in the fields of forensic psychiatry and criminal justice, considering legal implications and ethical issues. The analysis suggests that additional research is required on A.I. neuroprediction techniques, and there is still a great need to understand how they can be implemented in risk assessment in the field of forensic psychiatry. Besides the alluring potential of A.I. neuroprediction, we argue that its use in criminal justice and forensic psychiatry should be subjected to thorough harms/benefits analyses not only when these technologies will be fully available, but also while they are being researched and developed.

A. Pappagallo, A. Massini, and E. Tronci. "Monte Carlo Based Statistical Model Checking of CyberPhysical Systems: A Review." Information 11, no. 558 (2020). DOI: 10.3390/info11120588.

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
