Verification system for real-time specification based on extended real-time logic

摘要

Real-time system consists of many concurrent processes and behaves on strict timing conditions. It is important to verify the timing conditions of real-time system. In this paper, we propose extended TCTL(Timed CTL) and effective real-time model checking as follows. (1)The timing description of extended TCTL consists of both freeze quantification and bounded temporal operator. For this extension, extended TCTL admits timing constraints between distant contexts.rn(2)Real time model checking consists of both labelling algorithm and geometric region method. For this method, we can avoid the state explosion problem. We have developed the verification system, and showed our method effective.