TY  - JOUR
AU  - Mari, Federico
AU  - Melatti, Igor
AU  - Salvo, Ivano
AU  - Tronci, Enrico
ED  - Luigi Lavazza
PY  - 2013
DA  - 2013//
TI  - Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems
T2  - Intern. Journal on Advances in SW
JO  - International Journal on Advances in Software
SP  - 155
EP  - 169
VL  - vol. 6, nr 1&2
PB  - IARIA
KW  - Model-based software design
KW  - Linear predicates
KW  - Hybrid systems
AB  - Model based design is particularly appealing insoftware based control systems (e.g., embeddedsoftware) design,  since in such a case  systemlevel specifications are much easier to definethan the control software behavior itself.  Inturn, model based design of  embedded systemsrequires modeling  both continuous subsystems(typically, the plant) as well as  discretesubsystems (the controller). This is typicallydone using hybrid systems.  Mixed Integer LinearProgramming (MILP) based abstraction techniqueshave been successfully applied to automatically synthesize correct-by-construction controlsoftware for  discrete time linear hybrid systems,where plant dynamics is modeled as a linearpredicate over state,  input,  and next statevariables. Unfortunately, MILP solvers requiresuch linear predicates to be  conjunctions oflinear constraints, which is not a natural way ofmodeling hybrid systems.  In this paper we showthat,  under the hypothesis that each variableranges over a bounded interval,  any linearpredicate built upon conjunction and disjunction of linear constraints  can be automaticallytranslated into an equivalent conjunctivepredicate. Since variable bounds play a key rolein this translation,  our algorithm includes aprocedure to compute all implicit variable boundsof the given linear predicate. Furthermore, weshow that a particular form of linear predicates,namely  guarded predicates, are a natural andpowerful language to succinctly model discretetime linear hybrid systems dynamics. Finally, weexperimentally show the feasibility of ourapproach on an important and challenging casestudy taken from the literature, namely themulti-input Buck DC-DC Converter. As an example,the guarded predicate that models (with 57constraints) a 6-inputs Buck DC-DC Converter istranslated in a conjunctive predicate (with 102linear constraints) in about 40 minutes.
SN  - 1942-2628
L1  - http://mclab.di.uniroma1.it/publications/papers/mari/2013/115_Mari_etal2013.pdf
UR  - http://thinkmind.org/download.php?articleid=soft_v6_n12_2013_13
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=115), last updated on Wed, 13 Jan 2016 17:14:59 +0100
ID  - Mari_etal2013
ER  -