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.
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.
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "From Boolean Relations to Control Software." In Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances, 528–533. ThinkMind, 2011. ISSN: 978-1-61208-165-6. Notes: Best Paper Award.
Abstract: Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F.
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems." In Computer Aided Verification, edited by T. Touili, B. Cook and P. Jackson, 180–195. Lecture Notes in Computer Science 6174. Springer Berlin / Heidelberg, 2010. DOI: 10.1007/978-3-642-14295-6_20.
Abstract: We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.
|
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, and Harry Li. "Model Checking Coalition Nash Equilibria in MAD Distributed Systems." In Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings, edited by R. Guerraoui and F. Petit, 531–546. Lecture Notes in Computer Science 5873. Springer, 2009. DOI: 10.1007/978-3-642-05118-0_37.
Abstract: We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.
|
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, and Harry Li. "Model Checking Nash Equilibria in MAD Distributed Systems." In FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, edited by A. Cimatti and R. Jones, 1–8. Piscataway, NJ, USA: IEEE Press, 2008. ISSN: 978-1-4244-2735-2. DOI: 10.1109/FMCAD.2008.ECP.16.
Abstract: We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published.
Keywords: Model Checking, MAD Distributed System, Nash Equilibrium
|
Federico Mari, Igor Melatti, Enrico Tronci, and Alberto Finzi. "A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET." Mobile Information Systems 3, no. 9 (2013): 261–280. IOS Press. ISSN: 1574-017x (Print) 1875-905X (Online). DOI: 10.3233/MIS-130162.
|
Federico Mari, and Enrico Tronci. "CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems." In Hybrid Systems: Computation and Control (HSCC 2007), edited by A. Bemporad, A. Bicchi and G. C. Buttazzo, 399–412. Lecture Notes in Computer Science 4416. Springer, 2007. DOI: 10.1007/978-3-540-71493-4_32.
Abstract: Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
Keywords: Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS
|
Marco Martinelli, Enrico Tronci, Giovanni Dipoppa, and Claudio Balducelli. "Electric Power System Anomaly Detection Using Neural Networks." In 8th International Conference on: Knowledge-Based Intelligent Information and Engineering Systems (KES), edited by M. G. Negoita, R. J. Howlett and L. C. Jain, 1242–1248. Lecture Notes in Computer Science 3213. Wellington, New Zealand: Springer, 2004. ISSN: 3-540-23318-0. DOI: 10.1007/978-3-540-30132-5_168.
Abstract: The aim of this work is to propose an approach to monitor and protect Electric Power System by learning normal system behaviour at substations level, and raising an alarm signal when an abnormal status is detected; the problem is addressed by the use of autoassociative neural networks, reading substation measures. Experimental results show that, through the proposed approach, neural networks can be used to learn parameters underlaying system behaviour, and their output processed to detecting anomalies due to hijacking of measures, changes in the power network topology (i.e. transmission lines breaking) and unexpected power demand trend.
|
Silvia Mazzini, Stefano Puri, Federico Mari, Igor Melatti, and Enrico Tronci. "Formal Verification at System Level." In In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace., 2009.
Abstract: System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques.
|
I. Melatti, F. Mari, T. Mancini, M. Prodanovic, and E. Tronci. "A Two-Layer Near-Optimal 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 user-oblivious 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 two-layer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields near-optimal 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.
|