| Records |
| Author |
Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
On Model Based Synthesis of Embedded Control Software |
Type |
Conference Article |
| Year |
2012 |
Publication |
Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 7-12, 2012 |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
227-236 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
Publisher  |
ACM |
Place of Publication |
|
Editor |
Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
|
ISBN |
978-1-4503-1425-1 |
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
Techreport version can be found at arxiv.org |
Approved |
yes |
| Call Number |
Sapienza @ mari @ emsoft12 |
Serial |
97 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
Model Based Synthesis of Control Software from System Level Formal Specifications |
Type |
Journal Article |
| Year |
2014 |
Publication |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
Abbreviated Journal |
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY |
| Volume |
23 |
Issue |
1 |
Pages |
Article 6 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
ACM |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
1049-331X |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
no |
| Call Number |
Sapienza @ melatti @ |
Serial |
110 |
| Permanent link to this record |
| |
|
| |
| Author |
Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri |
| 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 |
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 |
Cesta, Amedeo; Fratini, Simone; Orlandini, Andrea; Finzi, Alberto; Tronci, Enrico |
| Title |
Flexible Plan Verification: Feasibility Results |
Type |
Journal Article |
| Year |
2011 |
Publication |
Fundamenta Informaticae |
Abbreviated Journal |
|
| Volume |
107 |
Issue |
2 |
Pages |
111-137 |
| 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 |
yes |
| Call Number |
Sapienza @ mari @ fi11 |
Serial |
15 |
| Permanent link to this record |
| |
|
| |
| 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 |
Mazzini, Silvia; Puri, Stefano; Mari, Federico; Melatti, Igor; Tronci, Enrico |
| Title |
Formal Verification at System Level |
Type |
Conference Article |
| Year |
2009 |
Publication |
In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
|
| Keywords |
|
| Abstract |
System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques. |
| 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 @ Dasia09 |
Serial |
20 |
| Permanent link to this record |
| |
|
| |
| Author |
Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico |
| Title |
Flexible Plan Verification: Feasibility Results |
Type |
Conference Article |
| Year |
2009 |
Publication |
16th RCRA International Workshop on “Experimental evaluation of algorithms for solving problems with combinatorial explosion” (RCRA). Proceedings |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
|
| 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 |
yes |
| Call Number |
Sapienza @ mari @ Rcra09 |
Serial |
22 |
| Permanent link to this record |
| |
|
| |
| Author |
Bobbio, Andrea; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico |
| Title |
Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections |
Type |
Journal Article |
| Year |
2005 |
Publication |
Archives of Transport – International Journal of Transport Problems |
Abbreviated Journal |
|
| Volume |
17 |
Issue |
3-4 |
Pages |
|
| 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 |
yes |
| Call Number |
Sapienza @ mari @ jtp05 |
Serial |
31 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
| Title |
Linearising Discrete Time Hybrid Systems |
Type |
Journal Article |
| Year |
2017 |
Publication |
IEEE Transactions on Automatic Control |
Abbreviated Journal |
|
| Volume |
62 |
Issue |
10 |
Pages |
5357-5364 |
| Keywords |
|
| Abstract |
Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool. |
| 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 |
0018-9286 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
no |
| Call Number |
Sapienza @ mari @ ref7902199 |
Serial |
164 |
| Permanent link to this record |
| |
|
| |
| Author |
Tronci, Enrico |
| 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 |
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 |
