Model Based Design is particularly appealing in embedded software design where system level specifications are much easier to define than the control software behavior itself. Formal analysis of Embedded Systems requires modelling both continuous systems (typically, the plant) as well as discrete systems (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 System, where plant dynamics is modeled as a linear predicate over state, input, and next state variables. MILP solvers requires constraints represented as conjunctive predicates. 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 transformed into an equisatisfiable conjunctive predicate. Moreover, since variable bounds play a key role in this transformation, we present an algorithm that taking as input a linear predicate, computes implicit variable bounds.

Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems / Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico. - STAMPA. - (2012). (Intervento presentato al convegno ICSEA 2012).

Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems

MARI, FEDERICO;MELATTI, IGOR;SALVO, Ivano;TRONCI, Enrico
2012

Abstract

Model Based Design is particularly appealing in embedded software design where system level specifications are much easier to define than the control software behavior itself. Formal analysis of Embedded Systems requires modelling both continuous systems (typically, the plant) as well as discrete systems (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 System, where plant dynamics is modeled as a linear predicate over state, input, and next state variables. MILP solvers requires constraints represented as conjunctive predicates. 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 transformed into an equisatisfiable conjunctive predicate. Moreover, since variable bounds play a key role in this transformation, we present an algorithm that taking as input a linear predicate, computes implicit variable bounds.
2012
ICSEA 2012
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems / Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico. - STAMPA. - (2012). (Intervento presentato al convegno ICSEA 2012).
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/488410
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact