
Giuseppe Della Penna, Alberto Tofani, Marcello Pecorari, Orazio Raparelli, Benedetto Intrigila, Igor Melatti, and Enrico Tronci. "A Case Study on Automated Generation of Integration Tests." In Fdl, 278–284. Ecsi, 2006. ISSN: 9783000197109.



Benedetto Intrigila, Ivano Salvo, and Stefano Sorgi. "A characterization of weakly ChurchRosser abstract reduction systems that are not ChurchRosser." Information and Computation 171, no. 2 (2001): 137–155. Academic Press, Inc.. ISSN: 08905401. DOI: 10.1006/inco.2001.2945.
Abstract: Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or ChurchRosser, CR) and weak confluence (or weak ChurchRosser, WCR) and their relationships can be studied in this setting: as a matter of fact, wellknown counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graphtheoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the NewmanÃ¢â‚¬â„¢s lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graphrewriting rules, with specific combinatorial properties.



V. Bono, and I. Salvo. "A CuCh Interpretation of an ObjectOriented Language." Electronic Notes in Theoretical Computer Science 50, no. 2 (2001): 159–177. Elsevier. Notes: BOTH 2001, BohmÃ¢â‚¬â„¢s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001). DOI: 10.1016/S15710661(04)001719.
Abstract: CuCh machine extends pure lambdaÃ‚â€“calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of overloading to define a functional interpretation of a simple, but significant fragment of a typical objectoriented language.



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 Testbed 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



Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. A MapReduce Parallel Approach to Automatic Synthesis of Control Software. Vol. abs/1210.2276. CoRR, Technical Report, 2012. http://arxiv.org/abs/1210.2276 (accessed June 15, 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 largesize systems. This motivates search for parallel algorithms for control software synthesis.
In this paper, we present a mapreduce style parallel algorithm for control software synthesis when the controlled system (plant) is modeled as discrete time linear hybrid system. Furthermore we present an MPIbased 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 multiinput 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.



Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "A MapReduce 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: 03029743. ISBN: 9783642391750. DOI: 10.1007/9783642391767_4.



Y. Driouich, M. Parente, and E. Tronci. "A methodology for a complete simulation of CyberPhysical Energy Systems." In EESMS 2018 – Environmental, Energy, and Structural Monitoring Systems, Proceedings, 1–5., 2018. DOI: 10.1109/EESMS.2018.8405826.



Benedetto Intrigila, Daniele Magazzeni, Igor Melatti, and Enrico Tronci. "A Model Checking Technique for the Verification of Fuzzy Control Systems." In CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol1 (CIMCAIAWTIC'06), 536–542. Washington, DC, USA: IEEE Computer Society, 2005. ISSN: 076952504001. DOI: 10.1109/CIMCA.2005.1631319.
Abstract: Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the celltocell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, celltocell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system.



Federico Mari, Igor Melatti, Enrico Tronci, and Alberto Finzi. "A multihop advertising discovery and delivering protocol for multi administrative domain MANET." Mobile Information Systems 3, no. 9 (2013): 261–280. IOS Press. ISSN: 1574017x (Print) 1875905X (Online). DOI: 10.3233/MIS130162.



Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila, and Marisa Venturini Zilli. "A Probabilistic Approach to Automatic Verification of Concurrent Systems." In 8th AsiaPacific Software Engineering Conference (APSEC), 317–324. Macau, China: IEEE Computer Society, 2001. ISSN: 0769514081. DOI: 10.1109/APSEC.2001.991495.
Abstract: The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead it just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that by using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory.

