Presentation 2009-01-30
Modeling and Verification of Hybrid Systems using Boolean Differential Constraints
Daisuke ISHII, Kazunori UEDA, Hiroshi HOSOBE,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) We propose a bounded model checking method for reachability analysis of hybrid systems. In our method, a nonlinear hybrid automaton is encoded into a logic formula which contains ordinary differential equations and guard constraints. The formula is also joined with logic formulas describing unsafe regions in a model. By showing satisfiability of the logic formula with a SAT solver and a computer algebra system (Mathematica), a bug in the model will be detected.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) hybrid systems / bounded model checking / reachability analysis
Paper # CST2008-53
Date of Issue

Conference Information
Committee CST
Conference Date 2009/1/22(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Concurrent System Technology (CST)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Modeling and Verification of Hybrid Systems using Boolean Differential Constraints
Sub Title (in English)
Keyword(1) hybrid systems
Keyword(2) bounded model checking
Keyword(3) reachability analysis
1st Author's Name Daisuke ISHII
1st Author's Affiliation Faculty of Science and Engineering, Waseda University()
2nd Author's Name Kazunori UEDA
2nd Author's Affiliation Faculty of Science and Engineering, Waseda University
3rd Author's Name Hiroshi HOSOBE
3rd Author's Affiliation National Institute of Informatics
Date 2009-01-30
Paper # CST2008-53
Volume (vol) vol.108
Number (no) 415
Page pp.pp.-
#Pages 4
Date of Issue