| Presentation | 2010-11-19 A Study of a Symbolic Encoding Method for Bounded Model Checking of UML State Machines with Synchronous and Asynchronous Transitions Hayato NIIMURA, Toshiyuki MIYAMOTO, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Recently, Bounded Model Checking has received attention as a SAT-based symbolic model checking technique. The basic idea behind this method is to reduce the model checking problem to the propositional satisfiability decision problem. In the field of distributed system specified by UML, no bounded model checking techniques take into account both synchronous and asynchronous transition. In this paper, we study a semantics, syntax, and symbolic encoding of UML state machines with synchronous and asynchronous transitions. Using the method, we verify a simple example. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | UML State Machine / Bounded Model Checking / SAT |
| Paper # | CAS2010-80,CST2010-53 |
| Date of Issue |
| Conference Information | |
| Committee | CAS |
|---|---|
| Conference Date | 2010/11/11(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 | Circuits and Systems (CAS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Study of a Symbolic Encoding Method for Bounded Model Checking of UML State Machines with Synchronous and Asynchronous Transitions |
| Sub Title (in English) | |
| Keyword(1) | UML State Machine |
| Keyword(2) | Bounded Model Checking |
| Keyword(3) | SAT |
| 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 | 2010-11-19 |
| Paper # | CAS2010-80,CST2010-53 |
| Volume (vol) | vol.110 |
| Number (no) | 283 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |