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 Vol-1 (CIMCA-IAWTIC'06), 536–542. Washington, DC, USA: IEEE Computer Society, 2005. ISSN: 0-7695-2504-0-01. 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 cell-to-cell 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, cell-to-cell 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.
|
Francesco Brizzolari, Igor Melatti, Enrico Tronci, and Giuseppe Della Penna. "Disk Based Software Verification via Bounded Model Checking." In APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference, 358–365. Washington, DC, USA: IEEE Computer Society, 2007. ISSN: 0-7695-3057-5. DOI: 10.1109/APSEC.2007.43.
Abstract: One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.
|
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.
|
