|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation." In In Proceedings of 17th EuroMicro Conference on Digital System Design (DSD 2014)., 2014. DOI: 10.1109/DSD.2014.91.
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "SyLVaaS: System Level Formal Verification as a Service." In Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD)., 2015. DOI: 10.1109/PDP.2015.119.
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. Quantized Feedback Control Software Synthesis from System Level Formal Specifications for Buck DC/DC Converters. Vol. abs/1105.5640. CoRR, Technical Report, 2011. http://arxiv.org/abs/1105.5640 (accessed May 9, 2024).
Abstract: Many Embedded Systems are indeed Software Based Control Systems (SBCSs), that is control systems whose controller consists of control software running on a microcontroller device. This motivates investigation on Formal Model Based Design approaches for automatic synthesis of SBCS control software. In previous works we presented an algorithm, along with a tool QKS implementing it, that from a formal model (as a Discrete Time Linear Hybrid System, DTLHS) of the controlled system (plant), implementation specifications (that is, number of bits in the Analog-to-Digital, AD, conversion) and System Level Formal Specifications (that is, safety and liveness requirements for the closed loop system) returns correct-by-construction control software that has a Worst Case Execution Time (WCET) linear in the number of AD bits and meets the given specifications. In this technical report we present full experimental results on using it to synthesize control software for two versions of buck DC-DC converters (single-input and multi-input), a widely used mixed-mode analog circuit.
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "Simulator Semantics for System Level Formal Verification." In Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015),., 2015. DOI: 10.4204/EPTCS.193.7.
|
|
|
V. Alimguzhin, F. Mari, I. Melatti, E. Tronci, E. Ebeid, S. A. Mikkelsen, R. H. Jacobsen, J. K. Gruber, B. Hayes, F. Huerta et al. "A Glimpse of SmartHG Project Test-bed and Communication Infrastructure." In Digital System Design (DSD), 2015 Euromicro Conference on, 225–232., 2015. DOI: 10.1109/DSD.2015.106.
Keywords: Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis
|
|
|
T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. "Anytime system level verification via parallel random exhaustive hardware in the loop simulation." Microprocessors and Microsystems 41 (2016): 12–28. ISSN: 0141-9331. DOI: 10.1016/j.micpro.2015.10.010.
Abstract: Abstract System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability.
Keywords: Model Checking of Hybrid Systems; Model checking driven simulation; Hardware in the loop simulation
|
|
|
T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. K. Gruber, B. Hayes, M. Prodanovic, and L. Elmegaard. "User Flexibility Aware Price Policy Synthesis for Smart Grids." In Digital System Design (DSD), 2015 Euromicro Conference on, 478–485., 2015. DOI: 10.1109/DSD.2015.35.
Keywords: Contracts; Current measurement; Load management; Power demand; Power measurement; State estimation; Substations; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis
|
|
|
T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, and E. Tronci. "On minimising the maximum expected verification time." Information Processing Letters (2017). DOI: 10.1016/j.ipl.2017.02.001.
|
|
|
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.
|
|
|
T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. "SyLVaaS: System Level Formal Verification as a Service." Fundamenta Informaticae 149, no. 1-2 (2016): 101–132. DOI: 10.3233/FI-2016-1444.
|
|