Reachability Analysis on Real-Time Value-Passing Systems
Jing Chen · Chinese Journal of Computers · 2003
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.