|
Federico Cavaliere, Federico Mari, Igor Melatti, Giovanni Minei, Ivano Salvo, Enrico Tronci, Giovanni Verzino, and Yuri Yushtein. "Model Checking Satellite Operational Procedures." In DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace., 2011.
Abstract: We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.
|
|
|
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.
|
|
|
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
|
|
|
A. Pappagallo, A. Massini, and E. Tronci. "Monte Carlo Based Statistical Model Checking of Cyber-Physical Systems: A Review." Information 11, no. 558 (2020). DOI: 10.3390/info11120588.
|
|
|
M. P. Hengartner, T. H. C. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. Röblitz, R. Ehrig, L. Saleh et al. "Negative affect is unrelated to fluctuations in hormone levels across the menstrual cycle: Evidence from a multisite observational study across two successive cycles." Journal of Psychosomatic Research 99 (2017): 21–27. DOI: 10.1016/j.jpsychores.2017.05.018.
|
|
|
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: 1664-1078. 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 brain-reading technologies which, in the nearby future, could have many applications, such as lie detection, neuromarketing or brain-computer 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 brain-reading 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.
|
|
|
T. Mancini. "Now or Never: negotiating efficiently with unknown counterparts." In proceedings of the 22nd RCRA International Workshop. Ferrara, Italy. CEUR, 2015 (Co-located with the 14th Conference of the Italian Association for Artificial Intelligence (AI*IA 2015)). (2015).
|
|
|
T. Mancini. "Now or Never: Negotiating Efficiently with Unknown or Untrusted Counterparts." Fundamenta Informaticae 149, no. 1-2 (2016): 61–100. DOI: 10.3233/FI-2016-1443.
|
|
|
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: 2352-2208. DOI: 10.1016/j.jlamp.2021.100640.
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.
Keywords: Formal verification, Simulation based formal verification, Formal Verification of cyber-physical systems, System-level formal verification
|
|
|
Enrico Tronci. "On Computing Optimal Controllers for Finite State Systems." In CDC '97: Proceedings of the 36th IEEE International Conference on Decision and Control. Washington, DC, USA: IEEE Computer Society, 1997.
|
|