|   | 
Details
   web
Records
Author
Title Charme Type Conference Article
Year (down) 2003 Publication Lecture Notes in Computer Science Abbreviated Journal
Volume 2860 Issue Pages
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Geist, D.; Tronci, E.
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 3-540-20363-X ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ editor-charme03 Serial 37
Permanent link to this record
 

 
Author Ciancamerla, Ester; Minichino, Michele; Serro, Stefano; Tronci, Enrico
Title Automatic Timeliness Verification of a Public Mobile Network Type Conference Article
Year (down) 2003 Publication 22nd International Conference on Computer Safety, Reliability, and Security (SAFECOMP) Abbreviated Journal
Volume Issue Pages 35-48
Keywords
Abstract This paper deals with the automatic verification of the timeliness of Public Mobile Network (PMN), consisting of Mobile Nodes (MNs) and Base Stations (BSs). We use the Mur$\varphi$ Model Checker to verify that the waiting access time of each MN, under different PMN configurations and loads, and different inter arrival times of MNs in a BS cell, is always below a preassigned threshold. Our experimental results show that Model Checking can be successfully used to generate worst case scenarios and nicely complements probabilistic methods and simulation which are typically used for performance evaluation.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Edinburgh, UK Editor Anderson, S.; Felici, M.; Littlewood, B.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2788 Series Issue Edition
ISSN 978-3-540-20126-7 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ safecomp03 Serial 38
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa
Title Synchronized regular expressions Type Journal Article
Year (down) 2003 Publication Acta Inf. Abbreviated Journal
Volume 39 Issue 1 Pages 31-70
Keywords
Abstract Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday also increases the need of more powerful tools to interact with texts. Indeed, much work has been done to provide simple and versatile tools that can be useful for the most common text manipulation tasks. Regular Expressions (RE), introduced by Kleene, are well known in the formal language theory. RE have been extended in various ways, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [15] UNIX command, or the Perl [20] language pattern matching constructs) we find backreferences, i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. In this paper we introduce the Synchronized Regular Expressions (SRE) as an extension of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are dealing with formalisms that should have a practical utility and be used in real applications, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user-friendly syntax for SRE to be used in implementations of SRE-powered search algorithms.
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 @ actainf03 Serial 39
Permanent link to this record
 

 
Author Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele
Title Fluid Petri Nets and hybrid model checking: a comparative case study Type Journal Article
Year (down) 2003 Publication Int. Journal on: Reliability Engineering & System Safety Abbreviated Journal
Volume 81 Issue 3 Pages 239-257
Keywords
Abstract The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a ’real world’ hybrid system: the temperature control system of a co-generative plant.
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 Approved yes
Call Number Sapienza @ mari @ ress03 Serial 40
Permanent link to this record
 

 
Author Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano
Title Intersection types and λ-definability Type Journal Article
Year (down) 2003 Publication Mathematical Structures in Computer Science Abbreviated Journal
Volume 13 Issue 1 Pages 15-53
Keywords
Abstract This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
Address
Corporate Author Thesis
Publisher Cambridge University Press Place of Publication New York, NY, USA Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0960-1295 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03 Serial 69
Permanent link to this record
 

 
Author Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano
Title Mobility Types for Mobile Processes in Mobile Ambients Type Journal Article
Year (down) 2003 Publication Electr. Notes Theor. Comput. Sci. Abbreviated Journal
Volume 78 Issue Pages
Keywords
Abstract 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 Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier Type Conference Article
Year (down) 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 394-409
Keywords
Abstract In this paper we present an explicit disk based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
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 @ Dimtz03 Serial 84
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Integrating RAM and Disk Based Verification within the Mur$\varphi$ Verifier Type Conference Article
Year (down) 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 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 Della Penna, Giuseppe; Di Marco, Antinisca; Intrigila, Benedetto; Melatti, Igor; Pierantonio, Alfonso
Title Xere: Towards a Natural Interoperability between XML and ER Diagrams Type Conference Article
Year (down) 2003 Publication Fundamental Approaches to Software Engineering, 6th International Conference, FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 356-371
Keywords
Abstract XML (eXtensible Markup Language) is becoming the standard format for documents on Internet and is widely used to exchange data. Often, the relevant information contained in XML documents needs to be also stored in legacy databases (DB) in order to integrate the new data with the pre-existing ones. In this paper, we introduce a technique for the automatic XML-DB integration, which we call Xere. In particular we present, as the first step of Xere, the mapping algorithm which allows the translation of XML Schemas into Entity-Relationship diagrams.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Pezzè, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2621 Series Issue Edition
ISSN 3-540-00899-3 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Ddimp03 Serial 86
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Minichino, Michele; Ciancamerla, Ester; Parisse, Andrea; Tronci, Enrico; Venturini Zilli, Marisa
Title Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier Type Conference Article
Year (down) 2003 Publication Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 141-155
Keywords
Abstract Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Maler, O.; Pnueli, A.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2623 Series Issue Edition
ISSN 3-540-00913-2 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimmcptz03 Serial 88
Permanent link to this record