Abstract
This paper presents a bounded model checking tool called for hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Our implementation successfully handled several examples including those with nonlinear constraints.
| Original language | English |
|---|---|
| Pages (from-to) | 449-461 |
| Number of pages | 13 |
| Journal | International Journal on Software Tools for Technology Transfer |
| Volume | 13 |
| Issue number | 5 |
| DOIs | |
| Publication status | Published - 2011 Oct |
Fingerprint
Keywords
- Bounded model checking
- Interval analysis
- Nonlinear hybrid systems
- Satisfiability modulo theories
ASJC Scopus subject areas
- Software
- Information Systems
Cite this
An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. / Ishii, Daisuke; Ueda, Kazunori; Hosobe, Hiroshi.
In: International Journal on Software Tools for Technology Transfer, Vol. 13, No. 5, 10.2011, p. 449-461.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems
AU - Ishii, Daisuke
AU - Ueda, Kazunori
AU - Hosobe, Hiroshi
PY - 2011/10
Y1 - 2011/10
N2 - This paper presents a bounded model checking tool called for hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Our implementation successfully handled several examples including those with nonlinear constraints.
AB - This paper presents a bounded model checking tool called for hybrid systems. It translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints and checks the satisfiability of the formula based on a satisfiability modulo theories method. We tightly integrate (i) an incremental SAT solver to enumerate the possible sets of constraints and (ii) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas. The HCS solver verifies the occurrence of a discrete change by using a set of boxes to enclose continuous states that may cause the discrete change. We utilize the existence property of a unique solution in the boxes computed by the HCS solver as (i) a proof of the reachability of a model and (ii) a guide in the over-approximation refinement procedure. Our implementation successfully handled several examples including those with nonlinear constraints.
KW - Bounded model checking
KW - Interval analysis
KW - Nonlinear hybrid systems
KW - Satisfiability modulo theories
UR - http://www.scopus.com/inward/record.url?scp=80052532801&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80052532801&partnerID=8YFLogxK
U2 - 10.1007/s10009-011-0193-y
DO - 10.1007/s10009-011-0193-y
M3 - Article
AN - SCOPUS:80052532801
VL - 13
SP - 449
EP - 461
JO - International Journal on Software Tools for Technology Transfer
JF - International Journal on Software Tools for Technology Transfer
SN - 1433-2779
IS - 5
ER -