| Presentation | 1999/1/22 Verification of Statechart Specifications Using Symbolic Model Checking Hirofumi Terada, Tatsuhiro Tsuchiya, Tohru Kikuno, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Statechart is a well-known visual formalism for the specification and design of large and complex reactive systems. We discuss automatic verification of statechart specifications. Specifically, we use a symbolic model checking tool called SMV(Symbolic Model Verifier).Symbolic model checking overcomes the state explosion problem using the Binary Decision Diagram(BDD)to represent the transition relation and state space of the model.Although it has been highly successful when applied to hardware systems, it is rarely reported applying to software specifications. In this paper, we first propose a translation method from a statechart specification to the SMV language. Then, we apply the proposed method to examples of statecharts in the literature. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | statechart / verification / symbolic model checking / SMV / SMV language |
| Paper # | SS98-41 |
| Date of Issue |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 1999/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 | Software Science (SS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Verification of Statechart Specifications Using Symbolic Model Checking |
| Sub Title (in English) | |
| Keyword(1) | statechart |
| Keyword(2) | verification |
| Keyword(3) | symbolic model checking |
| Keyword(4) | SMV |
| Keyword(5) | SMV language |
| 1st Author's Name | Hirofumi Terada |
| 1st Author's Affiliation | Department of Informatics and Mathematical Sciences Graduate School of Engineering Science, Osaka University() |
| 2nd Author's Name | Tatsuhiro Tsuchiya |
| 2nd Author's Affiliation | Department of Informatics and Mathematical Sciences Graduate School of Engineering Science, Osaka University |
| 3rd Author's Name | Tohru Kikuno |
| 3rd Author's Affiliation | Department of Informatics and Mathematical Sciences Graduate School of Engineering Science, Osaka University |
| Date | 1999/1/22 |
| Paper # | SS98-41 |
| Volume (vol) | vol.98 |
| Number (no) | 558 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |