|   | 
Details
   web
Records
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 (down) 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 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 (down) 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 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 (down) 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 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 (down) 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 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 (down) 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 Tronci, Enrico
Title Automatic Synthesis of Controllers from Formal Specifications Type Conference Article
Year 1998 Publication Proc of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM) Abbreviated Journal
Volume Issue Pages 134-143
Keywords
Abstract (down) Many safety critical reactive systems are indeed embedded control systems. Usually a control system can be partitioned into two main subsystems: a controller and a plant. Roughly speaking: the controller observes the state of the plant and sends commands (stimulus) to the plant to achieve predefined goals. We show that when the plant can be modeled as a deterministic finite state system (FSS) it is possible to effectively use formal methods to automatically synthesize the program implementing the controller from the plant model and the given formal specifications for the closed loop system (plant+controller). This guarantees that the controller program is correct by construction. To the best of our knowledge there is no previously published effective algorithm to extract executable code for the controller from closed loop formal specifications. We show practical usefulness of our techniques by giving experimental results on their use to synthesize C programs implementing optimal controllers (OCs) for plants with more than 109 states.
Address
Corporate Author Thesis
Publisher Place of Publication Brisbane, Queensland, Australia 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 @ icfem98 Serial 52
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier Type Conference Article
Year 2003 Publication Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 58-71
Keywords
Abstract (down) Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Blundo, C.; Laneve, C.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2841 Series Issue Edition
ISSN 3-540-20216-1 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ DIMTZ03c Serial 90
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title Regular Systems of Equations in λ-calculus Type Journal Article
Year 1990 Publication Int. J. Found. Comput. Sci. Abbreviated Journal
Volume 1 Issue 3 Pages 325-340
Keywords
Abstract (down) Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
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 @ ijfcs90 Serial 60
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title Regular Systems of Equations in λ-calculus Type Conference Article
Year 1989 Publication Ictcs Abbreviated Journal
Volume Issue Pages
Keywords
Abstract (down) Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
Address
Corporate Author Thesis
Publisher Place of Publication Mantova - 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 @ ictcs89 Serial 61
Permanent link to this record
 

 
Author Mari, Federico; Tronci, Enrico
Title CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems Type Conference Article
Year 2007 Publication Hybrid Systems: Computation and Control (HSCC 2007) Abbreviated Journal
Volume Issue Pages 399-412
Keywords Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS
Abstract (down) Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.
Address
Corporate Author Thesis
Publisher Springer Place of Publication Editor Bemporad, A.; Bicchi, A.; Buttazzo, G.C.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 4416 Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ MarTro07 Serial 92
Permanent link to this record