|
Records |
Links |
|
Author |
Bobbio, Andrea; Ciancamerla, Ester; Di Blasi, Saverio; Iacomini, Alessandro; Mari, Federico; Melatti, Igor; Minichino, Michele; Scarlatti, Alessandro; Tronci, Enrico; Terruggia, Roberta; Zendri, Emilio |
|
|
Title |
Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks |
Type |
Conference Article |
|
Year |
2009 |
Publication |
Proceedings of Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
90-97 |
|
|
Keywords |
|
|
|
Abstract |
The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation. |
|
|
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 |
Fourth International Conference on Risks and Security of Internet and Systems (CRiSIS) |
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ crisis09 |
Serial |
17 |
|
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 |
Chierichetti, Flavio; Lattanzi, Silvio; Mari, Federico; Panconesi, Alessandro |
|
|
Title |
On Placing Skips Optimally in Expectation |
Type |
Conference Article |
|
Year |
2008 |
Publication |
Web Search and Web Data Mining (WSDM 2008) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
15-24 |
|
|
Keywords |
Information Retrieval |
|
|
Abstract |
We study the problem of optimal skip placement in an inverted list. Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O(n log n), n being the length of the list. The placement is optimal in the sense that it minimizes the expected time to process a query. Our theoretical results are matched by experiments with a real corpus, showing that substantial savings can be obtained with respect to the tra- ditional skip placement strategy, that of placing consecutive skips, each spanning sqrt(n) many locations. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Acm |
Place of Publication |
|
Editor |
Najork, M.; Broder, A.Z.; Chakrabarti, S. |
|
|
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 @ ChiLatMar08 |
Serial |
94 |
|
Permanent link to this record |
|
|
|
|
Author |
Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa |
|
|
Title |
Exploiting Transition Locality in Automatic Verification |
Type |
Conference Article |
|
Year |
2001 |
Publication |
11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
259-274 |
|
|
Keywords |
|
|
|
Abstract |
In this paper we present an algorithm to contrast state explosion when using Explicit State Space Exploration to verify protocols. We show experimentally that protocols exhibit transition locality. We present a verification algorithm that exploits transition locality as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm is compatible with all Breadth First (BF) optimization techniques present in the Mur$\varphi$ verifier and it is by no means a substitute for any of them. In fact, since our algorithm trades space with time, it is typically most useful when one runs out of memory and has already used all other state reduction techniques present in the Mur$\varphi$ verifier. Our experimental results show that using our approach we can typically save more than 40% of RAM with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer |
Place of Publication |
Livingston, Scotland, UK |
Editor |
Margaria, T.; Melham, T.F. |
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
|
Series Volume |
2144 |
Series Issue |
|
Edition |
|
|
|
ISSN |
3-540-42541-1 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ charme01 |
Serial |
44 |
|
Permanent link to this record |
|
|
|
|
Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
|
|
Title |
Validation and verification issues in a timeline-based planning system |
Type |
Journal Article |
|
Year |
2010 |
Publication |
The Knowledge Engineering Review |
Abbreviated Journal |
|
|
|
Volume |
25 |
Issue |
03 |
Pages |
299-318 |
|
|
Keywords |
|
|
|
Abstract |
One of the key points to take into account to foster effective introduction of AI planning and scheduling systems in real world is to develop end user trust in the related technologies. Automated planning and scheduling systems often brings solutions to the users which are neither “obvious†nor immediately acceptable for them. This is due to the ability of these tools to take into account quite an amount of temporal and causal constraints and to employ resolution processes often designed to optimize the solution with respect to non trivial evaluation functions. To increase technology trust, the study of tools for verifying and validating plans and schedules produced by AI systems might be instrumental. In general, validation and verification techniques represent a needed complementary technology in developing domain independent architectures for automated problem solving. This paper presents a preliminary report of the issues concerned with the use of two software tools for formal verification of finite state systems to the validation of the solutions produced by MrSPOCK, a recent effort for building a timeline based planning tool in an ESA project. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Cambridge University Press |
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 @ Cffot10 |
Serial |
18 |
|
Permanent link to this record |
|
|
|
|
Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
|
|
Title |
Flexible Timeline-Based Plan Verification |
Type |
Conference Article |
|
Year |
2009 |
Publication |
KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
49-56 |
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer |
Place of Publication |
|
Editor |
Mertsching, Bärbel; Hund, M.; Aziz, M.Z. |
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
|
Series Volume |
5803 |
Series Issue |
|
Edition |
|
|
|
ISSN |
978-3-642-04616-2 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ Cffot09 |
Serial |
21 |
|
Permanent link to this record |
|
|
|
|
Author |
Cecconi, Michele; Tronci, Enrico |
|
|
Title |
Requirements Formalization and Validation for a Telecommunication Equipment Protection Switcher |
Type |
Conference Article |
|
Year |
2000 |
Publication |
Hase |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
IEEE Computer Society |
Place of Publication |
|
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
0-7695-0927-4 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ CeTro00 |
Serial |
29 |
|
Permanent link to this record |
|
|
|
|
Author |
Böhm, Corrado; Tronci, Enrico |
|
|
Title |
X-separability and left-invertibility in the λ-calculus (extended abstract, invited paper) |
Type |
Conference Article |
|
Year |
1987 |
Publication |
Proceedings of: Temi e prospettive della Logica e della Filosofia della Scienza contemporanea |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
|
|
|
Keywords |
|
|
|
Abstract |
|
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
|
Place of Publication |
Cesena - 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 @ cesena87 |
Serial |
64 |
|
Permanent link to this record |
|
|
|
|
Author |
Tronci, Enrico |
|
|
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 |
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 |
|
|
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 |
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 |