| Presentation | 2001/1/15 Automatic Verification of Fault Tolerance Using Symbolic Model Checking Tomoyuki Yokogawa, Tatsuhiro Tsuchiya, Tohru Kikuno, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | We propose a model checking method for automatic verification of fault tolerance of systems. We assume that a system to be verified is given in the form of a guarded-command program. This method uses a symbolic model checking tool called SMV (Symbolic Model Verifier). Although it has been widely applied to hardware systems, it is rarely reported to apply to software systems. In this paper we define a modeling language suited for describing guarded command programs, and then we propose a translation method from the modeling language to the input language of SMV. Finally we apply the proposed method to an example in the literature to verify fault tolerance of the system. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | symbolic model checking / fault tolerance / SMV / concurrent system / BDD / boolean function |
| Paper # | SS2000-35 |
| Date of Issue |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2001/1/15(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) | Automatic Verification of Fault Tolerance Using Symbolic Model Checking |
| Sub Title (in English) | |
| Keyword(1) | symbolic model checking |
| Keyword(2) | fault tolerance |
| Keyword(3) | SMV |
| Keyword(4) | concurrent system |
| Keyword(5) | BDD |
| Keyword(6) | boolean function |
| 1st Author's Name | Tomoyuki Yokogawa |
| 1st Author's Affiliation | Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University() |
| 2nd Author's Name | Tatsuhiro Tsuchiya |
| 2nd Author's Affiliation | Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| 3rd Author's Name | Tohru Kikuno |
| 3rd Author's Affiliation | Department of Informatics and Mathematical Science, Graduate School of Engineering Science, Osaka University |
| Date | 2001/1/15 |
| Paper # | SS2000-35 |
| Volume (vol) | vol.100 |
| Number (no) | 569 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |