|
|
Marco Gribaudo, Andras Horváth, Andrea Bobbio, Enrico Tronci, Ester Ciancamerla, and Michele Minichino. "Model-Checking Based on Fluid Petri Nets for the Temperature Control System of the ICARO Co-generative Plant." In 21st International Conference on Computer Safety, Reliability and Security (SAFECOMP), edited by S. Anderson, S. Bologna and M. Felici, 273–283. Lecture Notes in Computer Science 2434. Catania, Italy: Springer, 2002. ISSN: 3-540-44157-3. DOI: 10.1007/3-540-45732-1_27.
Abstract: The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain for conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPN). It is shown that the same FPN model can be fed to a functional analyser for model checking as well as to a stochastic analyser for performance evaluation. We illustrate our approach and show its usefulness by applying it to a “real world  hybrid system: the temperature control system of a co-generative plant.
|
|
|
|
Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo-Schettini, 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. 3-4 (2004): 168–186. DOI: 10.1007/s10207-004-0037-9.
Abstract: This paper presents a case study on an automated analysis of real-time 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: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given.
|
|
|
|
Riccardo Focardi, Roberto Gorrieri, Ruggero Lanotte, Andrea Maggiolo-Schettini, Fabio Martinelli, Simone Tini, and Enrico Tronci. "Formal Models of Timing Attacks on Web Privacy." Electronic Notes in Theoretical Computer Science 62 (2002): 229–243. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types. DOI: 10.1016/S1571-0661(04)00329-9.
Abstract: We model a timing attack on web privacy proposed by Felten and Schneider by using three different approaches: HL-Timed Automata, SMV model checker, and tSPA Process Algebra. Some comparative analysis on the three approaches is derived.
|
|
|
|
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: 1664-2392. 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 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.
|
|
|
|
Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, Rosario Pugliese, and Enrico Tronci. "A Symbolic Model Checker for ACTL." In International Workshop on Current Trends in Applied Formal Method (FM-Trends), edited by D. Hutter, W. Stephan, P. Traverso and M. Ullmann, 228–242. Lecture Notes in Computer Science 1641. Boppard, Germany: Springer, 1998. ISSN: 3-540-66462-9. DOI: 10.1007/3-540-48257-1_14.
Abstract: We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).
|
|
|
|
R. Ehrig, T. Dierkes, S. Schaefer, S. Roeblitz, E. Tronci, T. Mancini, I. Salvo, V. Alimguzhin, F. Mari, I. Melatti et al. "An integrative approach for model driven computation of treatments in reproductive medicine." In Proceedings of the 15th International Symposium on Mathematical and Computational Biology (BIOMAT 2015), Rorkee, India., 2015. DOI: 10.1142/9789813141919_0005.
|
|
|
|
Y. Driouich, M. Parente, and E. Tronci. "Modeling cyber-physical 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: cyber-physical systems;formal verification;maximum power point trackers;power engineering computing;Modelica;automatic verification;complex power electronics systems;cyber-physical 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;Cyber-Physical Systems;DMPPT;Modeling;Photovoltaic systems;Simulation;System Analysis and Design
|
|
|
|
Y. Driouich, M. Parente, and E. Tronci. "A methodology for a complete simulation of Cyber-Physical Energy Systems." In EESMS 2018 – Environmental, Energy, and Structural Monitoring Systems, Proceedings, 1–5., 2018. DOI: 10.1109/EESMS.2018.8405826.
|
|
|
|
Y. Driouich, M. Parente, and E. Tronci. "Model Checking Cyber-Physical 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.
|
|
|
|
G. Dipoppa, G. D'Alessandro, R. Semprini, and E. Tronci. "Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design." In High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on, 209–219. Albuquerque, NM, USA: IEEE Computer Society, 2001. ISSN: 0-7695-1275-5. DOI: 10.1109/HASE.2001.966821.
Abstract: A railway interlocking system (RIS) is an embedded system (namely a supervisory control system) that ensures the safe, operation of the devices in a railway station. RIS is a safety critical system. We explore the possibility of integrating automatic formal verification methods in a given industry RIS design flow. The main obstructions to be overcome in our work are: selecting a formal verification tool that is efficient enough to solve the verification problems at hand; and devising a cost effective integration strategy for such tool. We were able to devise a successful integration strategy meeting the above constraints without requiring major modification in the pre-existent design flow nor retraining of personnel. We run verification experiments for a RIS designed for the Singapore Subway. The experiments show that the RIS design flow obtained from our integration strategy is able to automatically verify real life RIS designs.
|
|
