框架时序逻辑程序设计解释器及模型检测工具

发布时间：2021-10-22 05:13

　　本文主要讨论一个框架时序逻辑程序设计语言FTLL （Framed Temporal Logic Programming Language）的解释器及一个基于命题投影时序逻辑PPTL （Proposition Projection Temporal Logic）进行性质描述的模型检测工具的实现。文中首先介绍了实现解释器的基于范式的基本方法,然后给出了解释器的基本框架并详细说明了各个模块的功用。此外还对FTLL中几个重要的结构的实现做了详细说明,包括框架、等待、投影、指针等操作。作为该解释器应用,它可以作为由OWL-S描述的抽象模型的模拟器,文中给出了一个详细的例子。随后,本文介绍了用FTLL为系统建模,PPTL进行性质描述,然后分别将系统和性质的非转换为各自的范式,接着对范式求交,并找它们的模型,看能否找到反例,从而进行模型检测的方法。并介绍了一个以此实现的模型检测工具,并给出了算法和一个例子。文章最后回顾了现有的模型检测工具。 

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

【文章页数】：56 页

【学位级别】：硕士

【部分图文】：

Present与Remains的输出例子

})这个程序的执行结果如图3.6所示。图3.6 程序执行结果3.4.2 电路仿真时序逻辑可以用来模拟逻辑电路的运行过程，部分基本的门电路用逻辑公式模拟如下：28

第三章 解释器的设计与实现，一旦有溢出，控制器就会终止运算并报路可以由时序逻辑公式来描述，而上面例子的门电路构成，所以我们可以用时序逻辑块，并组成一个完整的程序。逻辑电路就是验证输入任何一个整数，在结果1，此处，为了不至于程序执中行过程行过程，如图3.8所示。图中左边中括号内右边为高位，括号右边的整数为十进制的过程中，值不能超过255，否则就会溢出。16，8，4，2，1这几个数的变化，最终变想的正确性。


本文编号：3450452