| Records |
| 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 |
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 |
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 |
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 |
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 |
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 |
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 |
Tronci, Enrico |
| Title |
Formally Modeling a Metal Processing Plant and its Closed Loop Specifications |
Type |
Conference Article |
| Year |
1999 |
Publication |
4th IEEE International Symposium on High-Assurance Systems Engineering (HASE) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
151 |
| Keywords |
|
| Abstract |
We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design followed by automatic verification. The system to be controlled (plant) models a metal processing facility near Karlsruhe. We succeeded in automatically generating C code implementing a (correct by construction) embedded controller for such a plant from closed loop formal specifications. Our experimental results show that for industrial automation control systems automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design followed by automatic verification. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
IEEE Computer Society |
Place of Publication |
Washington, D.C, USA |
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
0-7695-0418-3 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ hase99 |
Serial |
50 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
From Boolean Functional Equations to Control Software |
Type |
Report |
| Year |
2011 |
Publication |
|
Abbreviated Journal |
|
| Volume |
abs/1106.0468 |
Issue |
|
Pages |
|
| Keywords |
|
| Abstract |
Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) at most O(nr), being n = |x| the number of arguments of functions in F and r the number of functions in F. |
| 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 |
105 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
From Boolean Relations to Control Software |
Type |
Conference Article |
| Year |
2011 |
Publication |
Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
528-533 |
| Keywords |
|
| Abstract |
Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) linear in nr, being n = |x| the number of input arguments for functions in F and r the number of functions in F. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
ThinkMind |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
978-1-61208-165-6 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
Best Paper Award |
Approved |
yes |
| Call Number |
Sapienza @ mari @ icsea11 |
Serial |
14 |
| 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 |
