| Presentation | 2016-01-25 On-the-fly Model Checker for a Petri Net Verification Tool(HiPS) by using Replacement LTL Formula to Event-Based Automaton Yojiro Harie, Katsumi Wasaki, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | This paper proposes an On-the-fly Linear Temporal Logic (LTL) model checker using state space generation based on the Petri net models. The `HiPS' tool developed by our research group at Shinshu University, is a design and verification environment for Place-Transition net. This tool features the functions to generate the state space and process trace graph which has a root and the edges as the initial marking and the firing sequences of Petri net respectively. HiPS tool can perform the exhaustive model checking for the state space by combining with external tools. However, since the order at present to apply the model checking is required for generating all of the state space, there are difficult issues to apply the large model from the physical and time constraint. Simultaneously, there is the on-the-fly model checking technique as the efficiency to against for the state explosion problem. The on-the-fly method then performs to test the events in parallel with the state space construction. In this study, we propose the parallel execution by performing the inter-process communication using the state space generation process and IPC channels on HiPS tool. This implement realizes a high-efficiency on-the-fly verification that executes independently of the verification process and the state space generation process. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Petri net / Model check / on-the-fly / Linear Temporal Logic / Event based checking |
| Paper # | MSS2015-46,SS2015-55 |
| Date of Issue | 2016-01-18 (MSS, SS) |
| Conference Information | |
| Committee | SS / MSS |
|---|---|
| Conference Date | 2016/1/25(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Shiinoki-Geihin-Kan |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Shoji Yuen(Nagoya Univ.) / Satoshi Yamane(Kanazawa Univ.) |
| Vice Chair | Kazuhiro Ogata(JAIST) / Morikazu Nakamura(Univ. of Ryukyus) |
| Secretary | Kazuhiro Ogata(Tokyo Inst. of Tech.) / Morikazu Nakamura(Waseda Univ.) |
| Assistant | Yoshiki Higo(Osaka Univ.) / Hideki Kinjo(Okinawa Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science / Technical Committee on Mathematical Systems Science and its applications |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | On-the-fly Model Checker for a Petri Net Verification Tool(HiPS) by using Replacement LTL Formula to Event-Based Automaton |
| Sub Title (in English) | |
| Keyword(1) | Petri net |
| Keyword(2) | Model check |
| Keyword(3) | on-the-fly |
| Keyword(4) | Linear Temporal Logic |
| Keyword(5) | Event based checking |
| 1st Author's Name | Yojiro Harie |
| 1st Author's Affiliation | Shinshu University(Shinshu Univ.) |
| 2nd Author's Name | Katsumi Wasaki |
| 2nd Author's Affiliation | Shinshu University(Shinshu Univ.) |
| Date | 2016-01-25 |
| Paper # | MSS2015-46,SS2015-55 |
| Volume (vol) | vol.115 |
| Number (no) | MSS-419,SS-420 |
| Page | pp.pp.63-68(MSS), pp.63-68(SS), |
| #Pages | 6 |
| Date of Issue | 2016-01-18 (MSS, SS) |