To search, Click below search items. |
| All Published Papers Search Service |
|
|
|
Title |
Constructing the Reaching Region Graph for Timed Automata with PVS |
|
Author |
Huaikou Miao, Qingguo Xu |
| Citation |
Vol. 6 No. 7 pp. 175-181 |
|
Abstract |
Based on our existing works, this paper firstly gives clock region equivalence PVS specification, and then constructs the reachable region graph for a given Timed Automaton (TA) via characterizing some kinds of clock regions, finally analyses the reachable states using the region graph. These works can conveniently analysis some real-time system in the form of TA model. A case study is investigated and the results are satisfying. As a by-product, an error is detected in the region-equivalence definition which is extensively referred in many papers. |
|
Keywords |
Timed Automata, Clock region, Region equivalence, Reachability analysis, PVS |
|
URL |
