基于下推网络的实时并发程序可达性分析及增量式验证

Verification of concurrent software is more and more important with the development and widely application of the multi-core technique, but it is still a challenging topic in the field of formal verification. In this project, in order to model real-time concurrent recursive programs, we firstly propose two formalisms named the time multiple stack pushdown network (TMPDN) and the time dynamic pushdown network (TDPN); with these formalisms, the dynamical creation of new threads and the interactions between threads can be modeled respectively. In order to verify real-time concurrent recursive programs which might both create threads dynamically and have interactions between threads, we propose a formalism named the time dynamic multi-stack pushdown network (TDMPN). By making use of some optimization technologies such as the abstract interpretation and the clock domain equivalence, and by using both the static transformation method and the dynamic transformation method, we will convert the multi-stack or dynamic pushdown network with continuous time into domain multi-stack or dynamic pushdown network. Based on the multi-stack or dynamic pushdown network, a context-switching bounded reachability algorithm is proposed; with this algorithm, the date consistency problem is analyzed during the process of linearization, and the reachability analysis and verification of real-time concurrent recursive programs is realized. Finally, in order to reduce the time cost of the verification process and to avoid investigating one property many times, we transform the bounded model checking problem of Boolean programs into the solution finding problem in the answer set programming (ASP), and realize incremental verification of system properties based on the ASP knowledge base.

并发程序验证是当前形式化验证的重点及难点。本项目以实时并发递归程序为研究对象，基于下推系统提出时间多栈下推网络TMPDN和时间动态下推网络TDPN，分别模拟线程之间交互或动态创建。为了进一步验证同时含有线程之间交互和线程动态创建的实时并发递归程序，提出了时间动态多栈下推网络TMDPN。然后通过抽象解释框架和时钟域等价优化技术，采用静态转换和动态转换两种方法，把连续时间的多栈或动态下推网络转换为离散的域多栈或动态下推网络。基于多栈或动态下推网络，给出了其上下文切换限界的可达算法，并在线性化同时，分析数据一致性冲突问题，从而实现实时并发递归程序的可达性分析与验证。为了减少验证过程中的时间花销，不重复计算已验证过得性质，把并发程序限界模型检验转化为ASP（Answer Set Programming）的解集问题，研究动态分析系统模型改变对已验证系统性质的影响，实现系统性质的增量式验证。

并发系统验证是当前形式化验证的重点及难点。本项目以实时并发系统为研究对象，从缓解状态空间爆炸出发，研究实时并发系统模型检验的优化技术。设计出三种描述实时并发递归程序的模型：时间多栈下推网络TMPDN、时间动态下推网络TPDN和时间动态多栈下推网络TMDPN，并给出了语法及其操作语义，能对含有多线程相互交互、线程动态创建以及递归的实时并发系统进行建模。.为了验证TMPDN模型，基于时间关键点的时钟域等价优化技术，并采用抽象解释框架描述其等价，缩减等价域状态空间；然后通过静态转换方法和动态转换方法，获得所有的可达域状态格局，把连续时间的多栈或动态下推网络转换为离散的域多栈或动态下推网络，同时给出了模型转换算法；最后可采用现有模型检验工具验证转换后的MPDN。为了验证TDPN模型，采用on-the-fly技术，仅关心栈顶及下一层的域状态转换，动态的将连续时间模型TDPN转换为时间域表示的离散模型DPN，从而解决带动态线程创建的实时并发系统的可达性分析..基于多栈或动态下推网络，提出了一种无需涉及线性化点的简化多栈数据线性一致性检测方法。在基于完整执行历史的情况下，证明多栈数据是线性一致性的当且仅当栈操作满足五个基本性质，然后扩展到一般执行历史的情况。最后通过自动机理论及可分离程序检测是否违反五个基本性质，进行线性一致性分析。.针对可达性问题，提出一种模糊博弈图作为模糊开放系统的形式化模型，重点解决了模糊博弈图的可达性问题，给出了解决可达性问题的算法和构造最优博弈策略的方法，并将研究成果应用到移动机器人的路径选择和软件开发公司的经营决策中。.同时，也研究了VLSI处理器阵列的重构问题。在行旁路、列重路由的约束下，采用网络流模型，将重构问题转化为对应网络中的最小花费节点不相交路径问题，并使用最小花费流算法对网络中的节点不相交路径问题进行求解，在确保了结果最优性的情况，多项式时间内得到解决。最后证明重构得到的目标阵列的几何性质是满足系统要求的。