| |
Records |
Links |
|
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 |
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 |
| |
|
| |
|
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 |
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 |
Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano |
|
| |
Title |
Intersection types and λ-definability |
Type |
Journal Article |
| |
Year |
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 |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems |
Type |
Journal Article |
| |
Year |
2013 |
Publication |
International Journal on Advances in Software |
Abbreviated Journal |
Intern. Journal on Advances in SW |
|
| |
Volume |
vol. 6, nr 1&2 |
Issue |
|
Pages |
155-169 |
|
| |
Keywords |
Model-based software design; Linear predicates; Hybrid systems |
|
| |
Abstract |
Model based design is particularly appealing in
software based control systems (e.g., embedded
software) design, since in such a case system
level specifications are much easier to define
than the control software behavior itself. In
turn, model based design of embedded systems
requires modeling both continuous subsystems
(typically, the plant) as well as discrete
subsystems (the controller). This is typically
done using hybrid systems. Mixed Integer Linear
Programming (MILP) based abstraction techniques
have been successfully applied to automatically
synthesize correct-by-construction control
software for discrete time linear hybrid systems,
where plant dynamics is modeled as a linear
predicate over state, input, and next state
variables. Unfortunately, MILP solvers require
such linear predicates to be conjunctions of
linear constraints, which is not a natural way of
modeling hybrid systems. In this paper we show
that, under the hypothesis that each variable
ranges over a bounded interval, any linear
predicate built upon conjunction and disjunction
of linear constraints can be automatically
translated into an equivalent conjunctive
predicate. Since variable bounds play a key role
in this translation, our algorithm includes a
procedure to compute all implicit variable bounds
of the given linear predicate. Furthermore, we
show that a particular form of linear predicates,
namely guarded predicates, are a natural and
powerful language to succinctly model discrete
time linear hybrid systems dynamics. Finally, we
experimentally show the feasibility of our
approach on an important and challenging case
study taken from the literature, namely the
multi-input Buck DC-DC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6-inputs Buck DC-DC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IARIA |
Place of Publication |
|
Editor |
Luigi Lavazza |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
1942-2628 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ melatti @ |
Serial |
115 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
|
| |
Title |
Synthesizing Control Software from Boolean Relations |
Type |
Journal Article |
| |
Year |
2012 |
Publication |
International Journal on Advances in Software |
Abbreviated Journal |
Intern. Journal on Advances in SW |
|
| |
Volume |
vol. 5, nr 3&4 |
Issue |
|
Pages |
212-223 |
|
| |
Keywords |
Control Software Synthesis; Embedded Systems; Model Checking |
|
| |
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 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. Moreover, a formal
proof of the proposed algorithm correctness is
also shown. Finally, we present experimental
results showing effectiveness of the proposed
algorithm. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IARIA |
Place of Publication |
|
Editor |
Luigi Lavazza |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
1942-2628 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ melatti @ |
Serial |
108 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
|
| |
Title |
An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks |
Type |
Conference Article |
| |
Year |
2018 |
Publication |
Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
302-312 |
|
| |
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 |
Best Paper |
Approved |
no |
|
| |
Call Number |
MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 |
Serial |
176 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico |
|
| |
Title |
Model checking driven simulation of sat procedures |
Type |
Conference Article |
| |
Year |
2012 |
Publication |
Proceedings of 12th International Conference on Space Operations (SpaceOps 2012) |
Abbreviated Journal |
International Conference on Space Operations |
|
| |
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 |
no |
|
| |
Call Number |
Sapienza @ melatti @ |
Serial |
117 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Tronci, E.; Mancini, T.; Salvo, I.; Mari, F.; Melatti, I.; Massini, A.; Sinisi, S.; Davì, F.; Dierkes, T.; Ehrig, R.; Röblitz, S.; Leeners, B.; Krüger, T.; Egli, M.; Ille, F. |
|
| |
Title |
Patient-Specific Models from Inter-Patient Biological Models and Clinical Records |
Type |
Conference Article |
| |
Year |
2014 |
Publication |
Formal Methods in Computer-Aided Design (FMCAD) |
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 |
no |
|
| |
Call Number |
Sapienza @ mari @ |
Serial |
120 |
|
| Permanent link to this record |
