| Presentation | 2009-01-29 On Model Checking Method for Soundness Verification of Workflow Nets Munenori YAMAGUCHI, Shingo YAMAGUCHI, Minoru TANAKA, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | A WF-net should have a property, called soundeness, which guarantees a logical correctness of the modeled workflow. In this paper, we propose a method to verify soundness using SPIN and NuSMV, which are typical model checking tools. Cyclic WF-nets may have livelock. We give a necessary and sufficient condition of livelock. Without livelock, SPIN can verify soundness than effectively NuSMV. Therefore we choose SPIN or NuSMV according to existence of livelock. In addition, we provide a necessary condition of soundness. The necessary condition enables us to use SPIN even if there is livelock. We also show effectiveness of our method by comparing it with an existing WF-net analysis tool, Woflan, on verification time for cyclic WF-nets. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | model checking / temporal logic / workflow nets / asymmetric choice / Woflan |
| Paper # | CST2008-46 |
| 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) | On Model Checking Method for Soundness Verification of Workflow Nets |
| Sub Title (in English) | |
| Keyword(1) | model checking |
| Keyword(2) | temporal logic |
| Keyword(3) | workflow nets |
| Keyword(4) | asymmetric choice |
| Keyword(5) | Woflan |
| 1st Author's Name | Munenori YAMAGUCHI |
| 1st Author's Affiliation | Graduate School of Science and Engineering, Yamaguchi University() |
| 2nd Author's Name | Shingo YAMAGUCHI |
| 2nd Author's Affiliation | Graduate School of Science and Engineering, Yamaguchi University |
| 3rd Author's Name | Minoru TANAKA |
| 3rd Author's Affiliation | Graduate School of Science and Engineering, Yamaguchi University |
| Date | 2009-01-29 |
| Paper # | CST2008-46 |
| Volume (vol) | vol.108 |
| Number (no) | 415 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |