中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
Subject: 计算机软件::软件理论
Title:
基于Pushdown系统证明的可视化
Author: 周青
Issued Date: 2016
Supervisor: 蒋颖研究员
Major: 可视化证明
Degree Grantor: 中国科学院研究生院
Place of Degree Grantor: 北京
Degree Level: 硕士
Keyword: deductive reasoning ; formal verification ; alternating pushdown system ; infinite state systems
Abstract: 形式验证的方法主要有模型检测和演绎推理两种。 模型检测的优点是验证过程是自
动的, 缺点是具有状态爆炸问题, 不利于处理大型系统。 演绎推理具有可以处理无穷状
态系统的优点, 但验证过程不是完全自 动的且对用户的数学知识要求较高。 有穷自 动机、
下推自 动机、 petri 网等迁移系统常常被用于系统建模, 在这些系统中大部分系统分析
问题可以规约到可达性问题。 因此, 可达性问题在形式验证中是非常重要的。 交替式下
推系统是形式化验证中的一种重要方法。 下推系统的可达性问题传统的解决方法是通过
在原本的下推系统之外构造一个新的有穷状态自 动机, 使得一个状态在下推系统中可达
当且仅当这个状态能被新构造的有穷状态自 动机所接收。 本文采用另一种解决交替式下
推系统可达性问题的方法, 即利用逻辑推演解决这些问题, 在原有的下推系统中做一个
饱和的过程, 使得一个状态是可达的当且仅当它在经过饱和后的下推系统中有一个具有
切消去性质的证明, 而省去了构造有穷状态自 动机的过程。
本文的第一个工作是研究与实现一个关于交替式下推系统中可达性的证明系统, 该
系统可以将无穷证明树转换为有穷树。 首先通过读入文本格式的输入文件, 解析输入文
件并得到交替式下推系统; 然后, 将交替式下推系统转换成小步交替式下推系统, 通过
循环迭代的方式对系统进行饱和操作直至规则收敛, 得到多元自 动机; 接下来利用全排
列算法实现系统的完备化, 得到完备化的多元自 动机, 并利用深度优先算法实现余归纳
方式的搜索证明。
本文的第二个工作是对生成的证明树在三维空间进行可视化。 通过改进力导向布局
算法中的斥力-引 力模型, 实现了树节点的自 动布局; 利用节点颜色的体现节点之间父子
关系; 通过增加旋转、 缩放、 高亮和事件响应功能, 使用户更好的理解证明树。


English Abstract: 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.

Content Type: 学位论文
URI: http://ir.iscas.ac.cn/handle/311060/17262
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
毕业论文final.pdf(968KB)----限制开放 联系获取全文

Recommended Citation:
周青. 基于Pushdown系统证明的可视化[D]. 北京. 中国科学院研究生院. 2016-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[周青]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[周青]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace