时间敏感下推系统可达性的验证问题

Time-sensitive pushdown systems show both the theoretical and practical importance in program analysis and system verification with time requirements. Reachability problem is one of important properties of the system, and many verification problems can be reduced to the reachability checking of the system. Currently，there are no general results for the decidability of reachability problem on time-sensitive pushdown systems, nor efficient verification tools. Firstly, we will prove the reachability problem is generally undecidable, by reducing a 2-counter machine to a time-sensitive pushdown system. Some subclasses of the system, suitable for program analysis and system verification, are shown to be decidable by reducing them to well-structured pushdown systems. At the same time, concurrent time-sensitive pushdown systems are also investigated, which are suitably used in multi-threaded program analysis. Secondly, the time regions of a time-sensitive pushdown system are encoded as weights, and therefore the reachability checking algorithm is proposed by reducing the system to a weighted pushdown system. An efficient model checker is implemented through this approach. Finally, the utility of the new model checker is illustrated by implementing a schedulability analyzer of timed regular task systems. With this result, an open problem, the decidability result of schedulability analysis on variation-time task systems can be solved.

时间敏感下推系统对具有实时要求的程序分析和系统验证具有重要的理论和应用价值。其中，可达性问题是这个系统的重要性质之一，许多验证问题可以通过可达性检测来解决。目前，尚未有时间敏感下推系统可达问题可判定一般性结论，也没有高效的验证工具。为此，首先，拟采用将2计数器机器规约到该系统的方式，证明一般情况下时间敏感下推系统的可达性不可判定，并通过将各种适于程序分析和系统验证的时间敏感下推系统子模型规约到良结构下推自动机，来证明这些子模型可达性可判定，同时，研究并发时间敏感下推系统可达性的判定问题，并将之应用于多线程程序分析；其次，将时间敏感下推系统的时间区间权重化，并通过规约此类模型至权重下推自动机的方式来高效实现出模型检测工具；最后，通过研究实现时间正则任务系统的可调度分析器,验证时间敏感下推系统模型检测工具的效用，并且解决任务系统中执行时间不固定的条件下，任务系统可调度性是否可判定的开放问题。

时间敏感下推系统对具有实时要求的程序分析和系统验证具有重要的理论和应用价值。其中，可达性问题是这个系统的重要性质之一，许多验证问题可以通过可达性检测来解决。本研究有如下成果：其一，研究时间敏感下推系统在不同类型时钟，如公有时钟、私有时钟、停冻时钟、可调整时钟，以及在不同类型约束下，如对角线时间约束、不变量约束，模型的可达性的可判定与不可判定的界。其二，通过上近似的方法高效实现了时间敏感下推系统的验证工具，并且完成了嵌入式操作系统OSEK/VDX的安全性验证。其三，通过研究实现时间正则任务系统的可调度性和安全性的分析,验证时间敏感下推系统验证工具的效用。