Presentation | 2012-01-26 A Study for Bounded Model Checking of UML State Machines Using SMT Solvers Hayato NIIMURA, Toshiyuki MIYAMOTO, |
---|---|
PDF Download Page | PDF download Page Link |
Abstract(in Japanese) | (See Japanese page) |
Abstract(in English) | Recently, SAT-based bounded model checking has received attention as an efficient symbolic model checking technique. It is known that for model checking of distributed systems with data SMT solvers is more effective than SAT solvers. We have proposed cbUML as a subset of UML to design and verify systems based on SOA. In this paper, we study a bounded model checking technique using SMT solvers to verify state machines of cbUML. |
Keyword(in Japanese) | (See Japanese page) |
Keyword(in English) | SOA / UML / state machine diagram / synchronous and asynchronous / bounded model checking |
Paper # | MSS2011-58,SS2011-43 |
Date of Issue |
Conference Information | |
Committee | MSS |
---|---|
Conference Date | 2012/1/19(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 | Mathematical Systems Science and its applications(MSS) |
---|---|
Language | JPN |
Title (in Japanese) | (See Japanese page) |
Sub Title (in Japanese) | (See Japanese page) |
Title (in English) | A Study for Bounded Model Checking of UML State Machines Using SMT Solvers |
Sub Title (in English) | |
Keyword(1) | SOA |
Keyword(2) | UML |
Keyword(3) | state machine diagram |
Keyword(4) | synchronous and asynchronous |
Keyword(5) | bounded model checking |
1st Author's Name | Hayato NIIMURA |
1st Author's Affiliation | Graduate School of Engineering, Osaka University() |
2nd Author's Name | Toshiyuki MIYAMOTO |
2nd Author's Affiliation | Graduate School of Engineering, Osaka University |
Date | 2012-01-26 |
Paper # | MSS2011-58,SS2011-43 |
Volume (vol) | vol.111 |
Number (no) | 405 |
Page | pp.pp.- |
#Pages | 6 |
Date of Issue |