基于Pushdown系统证明的可视化
文献类型：学位论文
| 作者 | 周青 |
| 学位类别 | 硕士 |
| 答辩日期 | 2016 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 北京 |
| 导师 | 蒋颖研究员 |
| 关键词 | deductive reasoning formal verification alternating pushdown system infinite state systems |
| 学位专业 | 可视化证明 |
| 中文摘要 | 形式验证的方法主要有模型检测和演绎推理两种。 模型检测的优点是验证过程是自 动的， 缺点是具有状态爆炸问题， 不利于处理大型系统。 演绎推理具有可以处理无穷状 态系统的优点， 但验证过程不是完全自 动的且对用户的数学知识要求较高。 有穷自 动机、 下推自 动机、 petri 网等迁移系统常常被用于系统建模， 在这些系统中大部分系统分析 问题可以规约到可达性问题。 因此， 可达性问题在形式验证中是非常重要的。 交替式下 推系统是形式化验证中的一种重要方法。 下推系统的可达性问题传统的解决方法是通过 在原本的下推系统之外构造一个新的有穷状态自 动机， 使得一个状态在下推系统中可达 当且仅当这个状态能被新构造的有穷状态自 动机所接收。 本文采用另一种解决交替式下 推系统可达性问题的方法， 即利用逻辑推演解决这些问题， 在原有的下推系统中做一个 饱和的过程， 使得一个状态是可达的当且仅当它在经过饱和后的下推系统中有一个具有 切消去性质的证明， 而省去了构造有穷状态自 动机的过程。 本文的第一个工作是研究与实现一个关于交替式下推系统中可达性的证明系统， 该 系统可以将无穷证明树转换为有穷树。 首先通过读入文本格式的输入文件， 解析输入文 件并得到交替式下推系统； 然后， 将交替式下推系统转换成小步交替式下推系统， 通过 循环迭代的方式对系统进行饱和操作直至规则收敛， 得到多元自 动机； 接下来利用全排 列算法实现系统的完备化， 得到完备化的多元自 动机， 并利用深度优先算法实现余归纳 方式的搜索证明。 本文的第二个工作是对生成的证明树在三维空间进行可视化。 通过改进力导向布局 算法中的斥力-引 力模型， 实现了树节点的自 动布局； 利用节点颜色的体现节点之间父子 关系； 通过增加旋转、 缩放、 高亮和事件响应功能， 使用户更好的理解证明树。 |
| 英文摘要 | Formal verification method mainly contains model checking and deductive reasoning. The advantage of model checking is that verification process is automatic . The disadvantage is that it has the state explosion problem and is not conducive to handle large scale system. Deductive reasoning has the advantage of dealing with infinite state systems, but the verification process is not completely automatic and requires a higher mathematical knowledge of the user. Systems such as finite automata, push down automata, Petri nets are often used in system modeling, and most analysis problem in these systems can be reduced to the reachability problem . Therefore, the reachability problem is very important in formal verification. Alternative push down system is one of the important methods in formal verification. The problems of the traditional method to solve these problem is to build a new finite state automata base on the original pushdown system, making a state in the pushdown systems is reachable if and only if the state is accepted by the newly built finite state automata. In this paper,we adopt another way to solve alternating pushdown system reachability problem, namely the use of logical deduction to solve these problems, a saturable process is done in the original pushdown system, makes a state is reachable if and only if it in after the saturation of the push system have a cut elimination proof, and eliminates the need for build a new finite state automata. The first work of this paper is to study and implement a system which can prove the reachability of the alternating pushdown system. First, our system read and parse the alternating pushdown system by an input file; Second, we transform the alternating pushdown system to an small step alternating pushdown system, and perform the saturation operation on the small step alternating pushdown system until the system converges; Third, we implement the complementation of the saturated system by full permutation, and implement the the conductive proof search by a depth-first search algorithm; At last, we visualize the proof tree produced by the system in a 3D space. The second work of this paper is to visualize the proof tree in the three-dimensional space . By improving repulsive-attractive model of the force directed placement algorithm, we realizeed the algorithm of the automatic layout of the nodes in a tree,make the relationship between parents nodes and children nodes clear by the color of the nodes, and make the proof tree easy to understand by adding functions such as rotation, scaling, highlighting and event response function. |
| 学科主题 | 软件理论 |
| 公开日期 | 2016-06-21 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/17262]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 周青. 基于Pushdown系统证明的可视化[D]. 北京. 中国科学院研究生院. 2016. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。