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

项目名称： 时间敏感下推系统可达性的验证问题

项目编号： No.61472240

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 李国强

作者单位： 上海交通大学

项目金额： 76万元

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

中文关键词： 形式化验证；下推系统；时间敏感；可达性问题；可调度分析

英文摘要： 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.

英文关键词： formal verification;pushdown systems;time-sensitive;reachability problems;schedulability analysis