Home // ICSEA 2012, The Seventh International Conference on Software Engineering Advances // View article

Linear Constraints as a Modeling Language for Discrete Time Hybrid Systems

Authors:
Federico Mari
Igor Melatti
Ivano Salvo
Enrico Tronci

Keywords: Model-based software design; Linear predicates; Hybrid systems

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.

Pages: 664 to 671

Copyright: Copyright (c) IARIA, 2012

Publication date: November 18, 2012

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-230-1

Location: Lisbon, Portugal

Dates: from November 18, 2012 to November 23, 2012