时间符号迁移图上的可达性分析

提出了以时间符号迁科为建模语言、基于可达性分析的模型检测算法，并给出了算法的正确性证明。该算法可被用于硬件设计和通信协议验证等领域。

Reachability Analysis on Real-Time Value-Passing Systems

Model checking is widely used in verification of hardware design and communication protocols. But because of state explosion, model checking cannot solve problems with larger scale. Actually, many issues in model checking can be reduced to reachability checking, which means less time and less space involved since the task is simply to check whether the state we care is reachable or not. Thus this kind of algorithms is easy to maintain or optimize in practice, and is accepted widely in industry. In this paper and algorithm based on reachability analysis is presented and many useful properties can be checked efficiently by it. The model used for systems is Timed Symbolic Transition Graph which can represent both real time and value passing under the same framework. Correspondingly a logic is presented for the algorithm to check the assertions concerning time, data and location. The correctness proof for the algorithm is also given.