toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Della Penna, Giuseppe; Tofani, Alberto; Pecorari, Marcello; Raparelli, Orazio; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico pdf  url
openurl 
  Title (up) A Case Study on Automated Generation of Integration Tests Type Conference Article
  Year 2006 Publication Fdl Abbreviated Journal  
  Volume Issue Pages 278-284  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Ecsi Place of Publication Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 978-3-00-019710-9 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Dtprimt06 Serial 27  
Permanent link to this record
 

 
Author Intrigila, Benedetto; Salvo, Ivano; Sorgi, Stefano pdf  doi
openurl 
  Title (up) A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser Type Journal Article
  Year 2001 Publication Information and Computation Abbreviated Journal  
  Volume 171 Issue 2 Pages 137-155  
  Keywords  
  Abstract Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church-Rosser, CR) and weak confluence (or weak Church-Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known 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 graph-theoretic 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 graph-rewriting rules, with specific combinatorial properties.  
  Address  
  Corporate Author Thesis  
  Publisher Academic Press, Inc. Place of Publication Duluth, MN, USA Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0890-5401 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ Intrigila-Salvo-Sorgi:01 Serial 68  
Permanent link to this record
 

 
Author Bono, V.; Salvo, I. pdf  url
doi  openurl
  Title (up) A CuCh Interpretation of an Object-Oriented Language Type Journal Article
  Year 2001 Publication Electronic Notes in Theoretical Computer Science Abbreviated Journal  
  Volume 50 Issue 2 Pages 159-177  
  Keywords  
  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 object-oriented language.  
  Address  
  Corporate Author Thesis  
  Publisher Elsevier 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 BOTH 2001, Bohm’s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001) Approved yes  
  Call Number Sapienza @ mari @ Bono-Salvo:BOTH01 Serial 72  
Permanent link to this record
 

 
Author Alimguzhin, V.; Mari, F.; Melatti, I.; Tronci, E.; Ebeid, E.; Mikkelsen, S.A.; Jacobsen, R.H.; Gruber, J.K.; Hayes, B.; Huerta, F.; Prodanovic, M. pdf  doi
openurl 
  Title (up) A Glimpse of SmartHG Project Test-bed and Communication Infrastructure Type Conference Article
  Year 2015 Publication Digital System Design (DSD), 2015 Euromicro Conference on Abbreviated Journal  
  Volume Issue Pages 225-232  
  Keywords Batteries; Control systems; Databases; Production; Sensors; Servers; Smart grids; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis  
  Abstract  
  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 no  
  Call Number Sapienza @ preissler @ Alimguzhin_etal2015 Serial 127  
Permanent link to this record
 

 
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico file  url
openurl 
  Title (up) A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software Type Report
  Year 2012 Publication Abbreviated Journal  
  Volume abs/1210.2276 Issue Pages  
  Keywords  
  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.
 
  Address  
  Corporate Author Thesis  
  Publisher CoRR, Technical Report 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 @ Serial 101  
Permanent link to this record
 

 
Author Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico pdf  doi
isbn  openurl
  Title (up) A Map-Reduce Parallel Approach to Automatic Synthesis of Control Software Type Conference Article
  Year 2013 Publication Proc. of International SPIN Symposium on Model Checking of Software (SPIN 2013) Abbreviated Journal International SPIN Symposium on Model Checking of Software  
  Volume Issue Pages 43-60  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher Springer - Verlag Place of Publication Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 7976 Series Issue Edition  
  ISSN 0302-9743 ISBN 978-3-642-39175-0 Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ melatti @ Serial 112  
Permanent link to this record
 

 
Author Driouich, Y.; Parente, M.; Tronci, E. pdf  doi
openurl 
  Title (up) A methodology for a complete simulation of Cyber-Physical Energy Systems Type Conference Article
  Year 2018 Publication EESMS 2018 – Environmental, Energy, and Structural Monitoring Systems, Proceedings Abbreviated Journal  
  Volume Issue Pages 1-5  
  Keywords  
  Abstract  
  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 no  
  Call Number MCLab @ davi @ Driouich20181 Serial 169  
Permanent link to this record
 

 
Author Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico pdf  doi
openurl 
  Title (up) 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 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 Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto pdf  url
doi  openurl
  Title (up) A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET Type Journal Article
  Year 2013 Publication Mobile Information Systems Abbreviated Journal Mobile Information Systems  
  Volume 3 Issue 9 Pages 261-280  
  Keywords  
  Abstract  
  Address  
  Corporate Author Thesis  
  Publisher IOS Press Place of Publication Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 1574-017x (Print) 1875-905X (Online) ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ melatti @ Serial 109  
Permanent link to this record
 

 
Author Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa pdf  doi
openurl 
  Title (up) A Probabilistic Approach to Automatic Verification of Concurrent Systems Type Conference Article
  Year 2001 Publication 8th Asia-Pacific Software Engineering Conference (APSEC) Abbreviated Journal  
  Volume Issue Pages 317-324  
  Keywords  
  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.  
  Address  
  Corporate Author Thesis  
  Publisher IEEE Computer Society Place of Publication Macau, China Editor  
  Language Summary Language Original Title  
  Series Editor Series Title Abbreviated Series Title  
  Series Volume Series Issue Edition  
  ISSN 0-7695-1408-1 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ apsec01 Serial 43  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: