toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico pdf  url
doi  openurl
  Title Automated Generation of Optimal Controllers through Model Checking Techniques Type Conference Article
  Year 2006 Publication Icinco-Icso Abbreviated Journal  
  Volume Issue Pages 26-33  
  Keywords  
  Abstract (up) We present a methodology for the synthesis of controllers, which exploits (explicit) model checking techniques. That is, we can cope with the systematic exploration of a very large state space. This methodology can be applied to systems where other approaches fail. In particular, we can consider systems with an highly non-linear dynamics and lacking a uniform mathematical description (model). We can also consider situations where the required control action cannot be specified as a local action, and rather a kind of planning is required. Our methodology individuates first a raw optimal controller, then extends it to obtain a more robust one. A case study is presented which considers the well known truck-trailer obstacle avoidance parking problem, in a parking lot with obstacles on it. The complex non-linear dynamics of the truck-trailer system, within the presence of obstacles, makes the parking problem extremely hard. We show how, by our methodology, we can obtain optimal controllers with different degrees of robustness.  
  Address  
  Corporate Author Thesis  
  Publisher INSTICC Press Place of Publication Editor Andrade-Cetto, J.; Ferrier, J.-L.; Pereira, J. M. C. D.; Filipe, J.  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 972-8865-59-7 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Dimmtt06 Serial 79  
Permanent link to this record
 

 
Author Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri pdf  openurl
  Title Model Checking Satellite Operational Procedures Type Conference Article
  Year 2011 Publication DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace. Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract (up) We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication 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 @ Dasia11 Serial 13  
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 (up) 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 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 Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa pdf  doi
openurl 
  Title Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier Type Conference Article
  Year 2003 Publication Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings Abbreviated Journal  
  Volume Issue Pages 277-282  
  Keywords  
  Abstract (up) We present a verification algorithm that can automatically switch from RAM based verification to disk based verification without discarding the work done during the RAM based verification phase. This avoids having to choose beforehand the proper verification algorithm. Our experimental results show that typically our integrated algorithm is as fast as (sometime faster than) the fastest of the two base (i.e. RAM based and disk based) verification algorithms.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Geist, D.; Tronci, E.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 2860 Series Issue Edition  
  ISSN 3-540-20363-X ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ DIMTZ03a Serial 85  
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico pdf  doi
openurl 
  Title Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems Type Conference Article
  Year 2010 Publication Computer Aided Verification Abbreviated Journal  
  Volume Issue Pages 180-195  
  Keywords  
  Abstract (up) We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Berlin / Heidelberg Place of Publication Editor Touili, T.; Cook, B.; Jackson, P.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 6174 Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ cav2010 Serial 16  
Permanent link to this record
 

 
Author Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano pdf  doi
openurl 
  Title Mobility Types for Mobile Processes in Mobile Ambients Type Journal Article
  Year 2003 Publication Electr. Notes Theor. Comput. Sci. Abbreviated Journal  
  Volume 78 Issue Pages  
  Keywords  
  Abstract (up) We present an ambient-like calculus in which the open capability is dropped, and a new form of “lightweight†process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the “minimal†requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way.  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication 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 @ Coppo-Dezani-Giovannetti-Salvo:03 Serial 74  
Permanent link to this record
 

 
Author Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico pdf  doi
openurl 
  Title A Symbolic Model Checker for ACTL Type Conference Article
  Year 1998 Publication International Workshop on Current Trends in Applied Formal Method (FM-Trends) Abbreviated Journal  
  Volume Issue Pages 228-242  
  Keywords  
  Abstract (up) We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Boppard, Germany Editor Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 1641 Series Issue Edition  
  ISSN 3-540-66462-9 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ fm-trends98 Serial 51  
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 Coalition Nash Equilibria in MAD Distributed Systems Type Conference Article
  Year 2009 Publication Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings Abbreviated Journal  
  Volume Issue Pages 531-546  
  Keywords  
  Abstract (up) We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Guerraoui, R.; Petit, F.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 5873 Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ sss09 Serial 19  
Permanent link to this record
 

 
Author Campagnano, Edoardo; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico pdf  doi
openurl 
  Title Automatic Analysis of a Safety Critical Tele Control System Type Conference Article
  Year 2005 Publication 24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP) Abbreviated Journal  
  Volume Issue Pages 94-107  
  Keywords  
  Abstract (up) We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Fredrikstad, Norway Editor Winther, R.; Gran, B. A.; Dahll, G.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 3688 Series Issue Edition  
  ISSN 3-540-29200-4 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ safecomp05 Serial 32  
Permanent link to this record
 

 
Author Tronci, Enrico doi  openurl
  Title Defining Data Structures via Böhm-Out Type Journal Article
  Year 1995 Publication J. Funct. Program. Abbreviated Journal  
  Volume 5 Issue 1 Pages 51-64  
  Keywords  
  Abstract (up) We show that any recursively enumerable subset of a data structure can be regarded as the solution set to a B??hm-out problem.  
  Address  
  Corporate Author Thesis  
  Publisher Place of Publication 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 @ jfp95 Serial 57  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: