toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Martinelli, Marco; Tronci, Enrico; Dipoppa, Giovanni; Balducelli, Claudio pdf  doi
openurl 
  Title Electric Power System Anomaly Detection Using Neural Networks Type Conference Article
  Year 2004 Publication 8th International Conference on: Knowledge-Based Intelligent Information and Engineering Systems (KES) Abbreviated Journal  
  Volume Issue Pages 1242-1248  
  Keywords  
  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.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication (down) Wellington, New Zealand Editor Negoita, M.G.; Howlett, R.J.; Jain, L.C.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 3213 Series Issue Edition  
  ISSN 3-540-23318-0 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ kes04 Serial 35  
Permanent link to this record
 

 
Author Tronci, Enrico file  url
openurl 
  Title On Computing Optimal Controllers for Finite State Systems Type Conference Article
  Year 1997 Publication CDC '97: Proceedings of the 36th IEEE International Conference on Decision and Control Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication (down) Washington, DC, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ cdc97 Serial 66  
Permanent link to this record
 

 
Author Tronci, Enrico pdf  url
doi  openurl
  Title Optimal Finite State Supervisory Control Type Conference Article
  Year 1996 Publication CDC '96: Proceedings of the 35th IEEE International Conference on Decision and Control Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract Supervisory Controllers are Discrete Event Dynamic Systems (DEDSs) forming the discrete core of a Hybrid Control System. We address the problem of automatic synthesis of Optimal Finite State Supervisory Controllers (OSCs). We show that Boolean First Order Logic (BFOL) and Binary Decision Diagrams (BDDs) are an effective methodological and practical framework for Optimal Finite State Supervisory Control. Using BFOL programs (i.e. systems of boolean functional equations) and BDDs we give a symbolic (i.e. BDD based) algorithm for automatic synthesis of OSCs. Our OSC synthesis algorithm can handle arbitrary sets of final states as well as plant transition relations containing loops and uncontrollable events (e.g. failures). We report on experimental results on the use of our OSC synthesis algorithm to synthesize a C program implementing a minimum fuel OSC for two autonomous vehicles moving on a 4 x 4 grid.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication (down) Washington, DC, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ cdc96 Serial 67  
Permanent link to this record
 

 
Author Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico pdf  doi
openurl 
  Title A Model Checking Technique for the Verification of Fuzzy Control Systems Type Conference Article
  Year 2005 Publication 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) Abbreviated Journal  
  Volume Issue Pages 536-542  
  Keywords  
  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.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication (down) Washington, DC, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0-7695-2504-0-01 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Immt05 Serial 75  
Permanent link to this record
 

 
Author Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe pdf  doi
openurl 
  Title Disk Based Software Verification via Bounded Model Checking Type Conference Article
  Year 2007 Publication APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference Abbreviated Journal  
  Volume Issue Pages 358-365  
  Keywords  
  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.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication (down) Washington, DC, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0-7695-3057-5 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Bmtd07 Serial 76  
Permanent link to this record
 

 
Author Tronci, Enrico pdf  doi
openurl 
  Title Formally Modeling a Metal Processing Plant and its Closed Loop Specifications Type Conference Article
  Year 1999 Publication 4th IEEE International Symposium on High-Assurance Systems Engineering (HASE) Abbreviated Journal  
  Volume Issue Pages 151  
  Keywords  
  Abstract We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design followed by automatic verification. The system to be controlled (plant) models a metal processing facility near Karlsruhe. We succeeded in automatically generating C code implementing a (correct by construction) embedded controller for such a plant from closed loop formal specifications. Our experimental results show that for industrial automation control systems automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design followed by automatic verification.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication (down) Washington, D.C, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0-7695-0418-3 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ hase99 Serial 50  
Permanent link to this record
 

 
Author Tronci, Enrico pdf  doi
openurl 
  Title Hardware Verification, Boolean Logic Programming, Boolean Functional Programming Type Conference Article
  Year 1995 Publication Tenth Annual IEEE Symposium on Logic in Computer Science (LICS) Abbreviated Journal  
  Volume Issue Pages 408-418  
  Keywords  
  Abstract One of the main obstacles to automatic verification of finite state systems (FSSs) is state explosion. In this respect automatic verification of an FSS M using model checking and binary decision diagrams (BDDs) has an intrinsic limitation: no automatic global optimization of the verification task is possible until a BDD representation for M is generated. This is because systems and specifications are defined using different languages. To perform global optimization before generating a BDD representation for M we propose to use the same language to define systems and specifications. We show that first order logic on a Boolean domain yields an efficient functional programming language that can be used to represent, specify and automatically verify FSSs, e.g. on a SUN Sparc Station 2 we were able to automatically verify a 64 bit commercial multiplier.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication (down) San Diego, California Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ lics95 Serial 56  
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa pdf  doi
openurl 
  Title Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier Type Conference Article
  Year 2002 Publication 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD) Abbreviated Journal  
  Volume Issue Pages 202-219  
  Keywords  
  Abstract The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication (down) Portland, OR, USA Editor Aagaard, M.; O'Leary, J.W.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 2517 Series Issue Edition  
  ISSN 3-540-00116-6 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ fmcad02 Serial 41  
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry pdf  doi
openurl 
  Title Model Checking Nash Equilibria in MAD Distributed Systems Type Conference Article
  Year 2008 Publication FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design Abbreviated Journal  
  Volume Issue Pages 1-8  
  Keywords Model Checking, MAD Distributed System, Nash Equilibrium  
  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.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Press Place of Publication (down) Piscataway, NJ, USA Editor Cimatti, A.; Jones, R.  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 978-1-4244-2735-2 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ MarMelSalTroAlvCle08 Serial 93  
Permanent link to this record
 

 
Author Böhm, Corrado; Piperno, Adolfo; Tronci, Enrico openurl 
  Title Solving Equations in λ-calculus Type Conference Article
  Year 1989 Publication Proc. of: Logic Colloquium 88 Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication (down) Padova - Italy Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ logic-colloquium-88 Serial 62  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: