|
|
Giuseppe Della Penna, Daniele Magazzeni, Alberto Tofani, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "Automated Generation Of Optimal Controllers Through Model Checking Techniques." In Informatics in Control Automation and Robotics. Selected Papers from ICINCO 2006, 107–119. Springer, 2008. DOI: 10.1007/978-3-540-79142-3_10.
|
|
|
|
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems." Sttt 6, no. 4 (2004): 320–341. DOI: 10.1007/s10009-004-0149-6.
Abstract: In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms. We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Mur$\varphi$ verifier distribution. We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Mur$\varphi$ verifier. Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Mur$\varphi$ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Mur$\varphi$ was able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 GB of memory using standard Mur$\varphi$.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. From Boolean Functional Equations to Control Software. Vol. abs/1106.0468. CoRR, Technical Report, 2011. http://arxiv.org/abs/1106.0468 (accessed May 18, 2024).
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) at most O(nr), being n = |x| the number of arguments of functions in F and r the number of functions in F.
|
|
|
|
Toni Mancini, Enrico Tronci, Ivano Salvo, Federico Mari, Annalisa Massini, and Igor Melatti. "Computing Biological Model Parameters by Parallel Statistical Model Checking." International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) 9044 (2015): 542–554. DOI: 10.1007/978-3-319-16480-9_52.
|
|
|
|
T. Mancini, F. Mari, I. Melatti, I. Salvo, and E. Tronci. "An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks." In Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings, 302–312., 2018. Notes: Best Paper. DOI: 10.1007/978-3-030-01851-1_29.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems." In Proceedings of the 51th IEEE Conference on Decision and Control, CDC 2012, December 10-13, 2012, Maui, HI, USA, 6120–6125. IEEE, 2012. ISBN: 978-1-4673-2065-8. Notes: Techreport version can be found at http://arxiv.org/abs/1207.4098. DOI: 10.1109/CDC.2012.6426260.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "On Model Based Synthesis of Embedded Control Software." In Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012, edited by Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr, 227–236. ACM, 2012. ISBN: 978-1-4503-1425-1. Notes: Techreport version can be found at arxiv.org. DOI: 10.1145/2380356.2380398.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems." In Proceedings of ICSEA 2012, The Seventh International Conference on Software Engineering Advances, 664–671. ThinkMind, 2012.
|
|
|
|
Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems." In Theoretical Aspects of Computing – ICTAC 2012, edited by A. Roychoudhury and M. D'Souza, 243–258. Lecture Notes in Computer Science 7521. Springer Berlin Heidelberg, 2012. ISBN: 978-3-642-32942-5. DOI: 10.1007/978-3-642-32943-2_19.
|
|
|
|
Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software. Vol. abs/1210.2276. CoRR, Technical Report, 2012. http://arxiv.org/abs/1210.2276 (accessed May 18, 2024).
Abstract: Many Control Systems are indeed Software Based Control Systems, i.e. 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 control software.
Available algorithms and tools (e.g., QKS) may require weeks or even months of computation to synthesize control software for large-size systems. This motivates search for parallel algorithms for control software synthesis.
In this paper, we present a map-reduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPI-based implementation PQKS of our algorithm. To the best of our knowledge, this is the first parallel approach for control software synthesis.
We experimentally show effectiveness of PQKS on two classical control synthesis problems: the inverted pendulum and the multi-input buck DC/DC converter. Experiments show that PQKS efficiency is above 65%. As an example, PQKS requires about 16 hours to complete the synthesis of control software for the pendulum on a cluster with 60 processors, instead of the 25 days needed by the sequential algorithm in QKS.
|
|
