| |
Records |
Links |
|
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. |
|
| |
Title |
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 |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.K.; Hayes, B.; Prodanovic, M.; Elmegaard, L. |
|
| |
Title |
User Flexibility Aware Price Policy Synthesis for Smart Grids |
Type |
Conference Article |
| |
Year |
2015 |
Publication |
Digital System Design (DSD), 2015 Euromicro Conference on |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
478-485 |
|
| |
Keywords |
Contracts; Current measurement; Load management; Power demand; Power measurement; State estimation; Substations; 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 @ Mancini_etal2015_3 |
Serial |
136 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
|
| |
Title |
Verifying Flexible Timeline-based Plans |
Type |
Conference Article |
| |
Year |
2009 |
Publication |
E-Proc. of ICAPS Workshop on Validation and Verification of Planning and Scheduling Systems |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verification method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study. |
|
| |
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 @ Vvps09 |
Serial |
23 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Driouich, Y.; Parente, M.; Tronci, E. |
|
| |
Title |
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 |
Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Tini, Simone; Troina, Angelo; Tronci, Enrico |
|
| |
Title |
Automatic Analysis of the NRL Pump |
Type |
Journal Article |
| |
Year |
2004 |
Publication |
Electr. Notes Theor. Comput. Sci. |
Abbreviated Journal |
|
|
| |
Volume |
99 |
Issue |
|
Pages |
245-266 |
|
| |
Keywords |
|
|
| |
Abstract |
We define a probabilistic model for the NRL Pump and using FHP-mur$\varphi$ show experimentally that there exists a probabilistic covert channel whose capacity depends on various NRL Pump parameters (e.g. buffer size, number of samples in the moving average, etc). |
|
| |
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 @ entcs04 |
Serial |
36 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Synchronized Regular Expressions |
Type |
Journal Article |
| |
Year |
2002 |
Publication |
Electr. Notes Theor. Comput. Sci. |
Abbreviated Journal |
|
|
| |
Volume |
62 |
Issue |
|
Pages |
195-210 |
|
| |
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 stresses the need of more powerful tools to interact with texts. Indeed, much work has been done to provide nonprogramming tools that can be useful for the most common text manipulation issues. Regular Expressions (RE), introduced by Kleene, are well–known in the formal language theory. RE received several extensions, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [A] UNIX command, or the Perl [17] language pattern matching constructs) we find backreferences (as defind in [1]), i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all the kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. Therefore, we introduce the Synchronized Regular Expressions (SRE) as a derivation 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 talking about formalisms that should have a practical utility and can be used in the real world, 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 |
TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types |
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ entcs02 |
Serial |
46 |
|
| 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 |
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 |
Focardi, Riccardo; Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico |
|
| |
Title |
Formal Models of Timing Attacks on Web Privacy |
Type |
Journal Article |
| |
Year |
2002 |
Publication |
Electronic Notes in Theoretical Computer Science |
Abbreviated Journal |
|
|
| |
Volume |
62 |
Issue |
|
Pages |
229-243 |
|
| |
Keywords |
|
|
| |
Abstract |
We model a timing attack on web privacy proposed by Felten and Schneider by using three different approaches: HL-Timed Automata, SMV model checker, and tSPA Process Algebra. Some comparative analysis on the three approaches is derived. |
|
| |
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 |
TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types |
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ entcs02a |
Serial |
47 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Bono, V.; Salvo, I. |
|
| |
Title |
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 |
Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; Salvo, Ivano; Sassone, Vladimiro |
|
| |
Title |
A Type Inference Algorithm for Secure Ambients |
Type |
Journal Article |
| |
Year |
2002 |
Publication |
Electronic Notes in Theoretical Computer Science |
Abbreviated Journal |
|
|
| |
Volume |
62 |
Issue |
|
Pages |
83-101 |
|
| |
Keywords |
|
|
| |
Abstract |
We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario. |
|
| |
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 |
TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types |
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01 |
Serial |
73 |
|
| Permanent link to this record |
