| Presentation | 1994/9/3 Method of Specification and Verification of Concurrent System using infinite timed statechart Satoshi Yamane, Nobutoshi Umehara, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Asynchronus concurrent system specification which includes timing constraints,is usually expressed by timed graph.The approach of computer support for the concurrent system is classified into automatic generation(model generation from constraint temporal logic specification)and automatic vetification(deciding whether or not timed graph satisfies property).It is difficult to generate dense timed graph from temporal logic including punctuality.But automatic verification approach is decidable.We propose infinite timed statechart in order to effectively specify concurrent system and verify it.The main feature is following:(1)Formal specification by statechart extending timed automata.(2)Verification problem reduces to inclusion problem in formal language theory.(3)Timing simulation of timed graph largely reduces verification complexity.(4) Interface rule reduces space complexity of timed graph according to each verification property specification. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | concurrent system / specification / verification / statechart / timing constraint / timed automaton |
| Paper # | CAS94-55 |
| Date of Issue |
| Conference Information | |
| Committee | CAS |
|---|---|
| Conference Date | 1994/9/3(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 | Circuits and Systems (CAS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Method of Specification and Verification of Concurrent System using infinite timed statechart |
| Sub Title (in English) | |
| Keyword(1) | concurrent system |
| Keyword(2) | specification |
| Keyword(3) | verification |
| Keyword(4) | statechart |
| Keyword(5) | timing constraint |
| Keyword(6) | timed automaton |
| 1st Author's Name | Satoshi Yamane |
| 1st Author's Affiliation | Department of Computer and Information Science,Faculty of Science, Shimane University() |
| 2nd Author's Name | Nobutoshi Umehara |
| 2nd Author's Affiliation | Department of Computer and Information Science,Faculty of Science, Shimane University |
| Date | 1994/9/3 |
| Paper # | CAS94-55 |
| Volume (vol) | vol.94 |
| Number (no) | 214 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |