Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems
Mari
Federico
author
Melatti
Igor
author
Salvo
Ivano
author
Tronci
Enrico
author
2013
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.
Model-based software design
Linear predicates
Hybrid systems
exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=115), last updated on Wed, 13 Jan 2016 17:14:59 +0100
text
http://thinkmind.org/download.php?articleid=soft_v6_n12_2013_13
http://mclab.di.uniroma1.it/publications/papers/mari/2013/115_Mari_etal2013.pdf
http://thinkmind.org/download.php?articleid=soft_v6_n12_2013_13
Mari_etal2013
International Journal on Advances in Software
Intern. Journal on Advances in SW
Luigi Lavazza
editor
2013
IARIA
continuing
periodical
academic journal
vol. 6, nr 1&2
155
169
1942-2628