|
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier." Int. J. Softw. Tools Technol. Transf. 8, no. 4 (2006): 397–409. Springer-Verlag. ISSN: 1433-2779. DOI: 10.1007/s10009-005-0216-7.
Abstract: In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
|
|
|
|
Verzino Giovanni, Federico Cavaliere, Federico Mari, Igor Melatti, Giovanni Minei, Ivano Salvo, Yuri Yushtein, and Enrico Tronci. "Model checking driven simulation of sat procedures." In Proceedings of 12th International Conference on Space Operations (SpaceOps 2012)., 2012. DOI: 10.2514/6.2012-1275611.
|
|
|
|
E. Tronci, T. Mancini, F. Mari, I. Melatti, I. Salvo, M. Prodanovic, J. K. Gruber, B. Hayes, and L. Elmegaard. "Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids." In Proceedings of Smart Grid Communications (SmartGridComm), 2014 IEEE International Conference On., 2014. DOI: 10.1109/SmartGridComm.2014.7007745.
|
|
|
|
E. Tronci, T. Mancini, I. Salvo, F. Mari, I. Melatti, A. Massini, S. Sinisi, F. Davì, T. Dierkes, R. Ehrig et al. "Patient-Specific Models from Inter-Patient Biological Models and Clinical Records." In Formal Methods in Computer-Aided Design (FMCAD)., 2014. DOI: 10.1109/FMCAD.2014.6987615.
|
|
|
|
E. Tronci, T. Mancini, F. Mari, I. Melatti, R. H. Jacobsen, E. Ebeid, S. A. Mikkelsen, M. Prodanovic, J. K. Gruber, and B. Hayes. "SmartHG: Energy Demand Aware Open Services for Smart Grid Intelligent Automation." In Proceedings of the Work in Progress Session of SEAA/DSD 2014., 2014. ISBN: 978-3-902457-40-0.
|
|
|
|
Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, and Enrico Tronci. "System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation." In Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing. IEEE Computer Society, 2014. DOI: 10.1109/PDP.2014.32.
|
|
|
|
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 April 27, 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, Fabio Merli, and Enrico Tronci. "System Level Formal Verification via Model Checking Driven Simulation." In Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia, 296–312. Lecture Notes in Computer Science 8044. Springer - Verlag, 2013. ISSN: 0302-9743. ISBN: 978-3-642-39798-1. DOI: 10.1007/978-3-642-39799-8_21.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software." In Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013), 43–60. Lecture Notes in Computer Science 7976. Springer - Verlag, 2013. ISSN: 0302-9743. ISBN: 978-3-642-39175-0. DOI: 10.1007/978-3-642-39176-7_4.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "On-the-Fly Control Software Synthesis." In Proceedings of International SPIN Symposium on Model Checking of Software (SPIN 2013), 61–80. Lecture Notes in Computer Science 7976. Springer - Verlag, 2013. ISSN: 0302-9743. ISBN: 978-3-642-39175-0. DOI: 10.1007/978-3-642-39176-7_5.
|
|
