基于MSVL的动静结合程序验证和自动规划

发布时间：2021-01-20 19:24

　　作为一种规范语言,时序逻辑已经被广泛用于计算机程序、数字电路和通信协议的验证以及人工智能的时序推理中。此外,时序逻辑也被用作程序设计语言来编写程序。一个时序逻辑程序设计语言编写的程序称作是一个时序逻辑程序,其本质上是一个时序逻辑公式。跟传统的非形式化编程语言（如Pascal,C等）不同,时序逻辑程序的执行过程是根据给定的规则对公式进行化简的过程。通常时序逻辑程序的执行过程更加复杂,执行效率已经成为影响时序逻辑程序能否应用于实际大型复杂系统的一个关键因素。为此,本文以建模、仿真和验证语言MSVL（Modeling,Simulation and Verification Language）为研究对象,提出了一种MSVL程序的编译执行方法并实现了一个MSVL编译器。在此基础上,研究了基于MSVL和MSVL编译器的C程序验证方法以及自动规划方法。此外,为了支持对C程序的时序性质验证,研究了时序性质自动挖掘方法从程序中挖掘PPTL（Propositional Projection Temporal Logic）性质。本文主要工作概括如下:第一,为了高效执行MSVL程序,提出了一种MSVL程序的编... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：137 页

【学位级别】：博士

【部分图文】：

例子C程序Exa1.c

例2.1. MSVL程序frame(x) and ((int x<==2 or int x<==3)and (while(x<5){x:=x+2}))对应的NFG如图2.2所示。图2.2 MSVL程序的NFG图示2.3 命命题题投投影影时时序序逻逻辑辑本节介绍命题投影时序逻辑PPTL。PPTL是投影时序逻辑PTL的一个子集。准确地说，PPTL是PTL的命题形式。PPTL中不包含PTL中的一阶成分，例如变量，谓词和量词。文章[10, 11]证明了PPTL是可判定的，并给出了PPTL的判定过程。此外，文章[129]中证明PPTL的表达能力是完全正则的。本节简单介绍PPTL的语法和语义，以及PPTL公式对应的带标记的范式图（Labeled Normal Form Graph，简称LNFG）[11, 28]。2.3.1语法和语义一个PPTL公式 在一个可数的原子命题集合P上的归纳定义如下： ::= | ○ | | ∨ | ( 1

“?”表示任意命题可能在该状态成立。作为对比，图2.3给出了PPTL公式 ( ; )+对应的LNFG。直观地，该公式表示从区间的某个状态开始，命题 和 周期重复成立，且至少重复一次。同样的，图2.6给出了满足了四个满足公式 ( ; )+的状态区间的例子。图2.4中的状态区间1满足公式 ( ; )*但不满足公式 ( ; )+。图2.3公式 ( ; )*对应的LNFG图2.4满足公式 ( ; )*的状态区间图示2.4 本本章章小小结结本章简要介绍了本文的研究基础，包括一阶投影时序逻辑PTL的语法和语义，24

【参考文献】：
期刊论文
[1]基于线性时序逻辑的移动端快递派送路径规划[J]. 禹鑫燚,郭永奎,欧林林,汪涛,卢靓,张爱美.  高技术通讯. 2017(06)
[2]Model checking concurrent systems with MSVL[J]. Nan ZHANG,Zhenhua DUAN,Cong TIAN.  Science China（Information Sciences）. 2016(11)
[3]基于线性时序逻辑理论的仓储机器人路径规划[J]. 禹鑫燚,陈浩,郭永奎,程诚,欧林林,俞立.  高技术通讯. 2016(01)
[4]未知环境下移动机器人安全路径规划的一种神经网络方法[J]. 樊长虹,陈卫东,席裕庚.  自动化学报. 2004(06)
[5]大规模真实地形数据中的全局路径规划方法——基于遗传算法的研究[J]. 梁晓辉,吴威,赵沁平.  计算机研究与发展. 2002(03)
[6]XYZ系统在电信领域中的应用[J]. 沈武威,唐稚松.  软件学报. 1996(06)



本文编号：2989636