| Presentation | 1994/11/17 An Automatic Generation of Formal Specifications and Its Verification Using Logical Petri net Kukhwan SONG, Atsushi TOGASHI, Norio SHIRATORI, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, we propose a model, Logical Petri net (LPN), that is a kind of extended Petri net, in order to model functional requirements which come from system requirements. And we also propose a synthesis method that converts functional requirements of a system into formal specifications automatically, while searching functional requirements that contain some kinds of logical errors. We use the state transition systems as the formal specification descriptions, because it is the basic concept of the Formal Description Techniques (FDTs) for communication systems. When we create the state transition systems, the synthesis method produces states that are only necessary ones in the system. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Petri net / reachability tree / formal specification / verification |
| Paper # | CAS94-69,CST94-29 |
| Date of Issue |
| Conference Information | |
| Committee | CST |
|---|---|
| Conference Date | 1994/11/17(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) | An Automatic Generation of Formal Specifications and Its Verification Using Logical Petri net |
| Sub Title (in English) | |
| Keyword(1) | Petri net |
| Keyword(2) | reachability tree |
| Keyword(3) | formal specification |
| Keyword(4) | verification |
| 1st Author's Name | Kukhwan SONG |
| 1st Author's Affiliation | Research Institute of Electrical Communication, Tohoku University() |
| 2nd Author's Name | Atsushi TOGASHI |
| 2nd Author's Affiliation | Research Institute of Electrical Communication, Tohoku University |
| 3rd Author's Name | Norio SHIRATORI |
| 3rd Author's Affiliation | Research Institute of Electrical Communication, Tohoku University |
| Date | 1994/11/17 |
| Paper # | CAS94-69,CST94-29 |
| Volume (vol) | vol.94 |
| Number (no) | 333 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |