期刊名称：International Journal of Computer Science and Network Security
印刷版ISSN：1738-7906
出版年度：2006
卷号：6
期号：7A
页码：175-181
出版社：International Journal of Computer Science and Network Security
摘要：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.
关键词：Timed Automata, Clock region, Region equivalence, Reachability analysis, PVS
