导读:本文包含了行为时序逻辑论文开题报告文献综述及选题提纲参考文献，主要关键词:区间时序逻辑,控制流程图,程序静态结构,模型检验
行为时序逻辑论文文献综述
陈冬火,刘全,金海东,朱斐,王辉[1]（2016）在《具有程序的静态结构和动态行为语义的时序逻辑》一文中研究指出提出一种区间分支时序逻辑——控制流区间时序逻辑(control flow interval temporal logic,CFITL),用于规约程序的时序属性.不同于计算树逻辑(computation tree logic,CTL)和线性时序逻辑(linear temporal logic,LTL)等传统的时序逻辑,CFITL公式的语义模型不是基于状态的类Kripke结构,而是以程序的抽象模型控制流图(control flow graph,CFG)为基础所构建的含序CFG结构.含序CFG是CFG的一种受限子集,它们的拓扑结构可映射为偏序集,这样诱导产生的自然数区间可自然地用于描述定义良好的程序结构.这种结构含有程序的静态结构信息和动态行为信息,换而言之,CFITL具有规约程序实现结构属性和程序执行动态行为属性的能力.在定义CFITL的语法和语义的基础上,详细讨论了CFITL的模型检验问题,包括基于值状态空间可达性计算的模型检验方法和基于SMT(satisfiability modulo theories)的CFITL有界模型检验方法.现代程序都含有复杂且具有无限值域的抽象数据类型及各种复杂的操作,CFITL语义定义相比CTL等时序逻辑更复杂,因此,基于显示状态搜索的方法难以有效进行,而基于SMT的CFITL有界模型检验方法更易实现、更具有可行性.最近开发相关的原型工具,并进行相关的实例研究.(本文来源于《计算机研究与发展》期刊2016年09期）
唐郑熠,薛醒思,王金水,王晓峰[2]（2016）在《行为时序逻辑中四级公平性下的活性推理规则》一文中研究指出公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则对一个程序实例进行了推理验证,在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。(本文来源于《计算机应用研究》期刊2016年10期）
刘照洋,龙士工[3]（2015）在《基于行为时序逻辑TLA的Pastry协议的规约与验证》一文中研究指出本文研究基于行为时序逻辑TLA的模型检测技术,阐述TLA的语义、语法和公平性问题。用基于TLA的系统描述语言TLA+对Pastry协议及其属性进行规约并用模型检测工具TLC对其进行验证。(本文来源于《贵州大学学报(自然科学版)》期刊2015年06期）
刘照洋[4]（2015）在《基于行为时序逻辑TLA的网络协议的描述与验证》一文中研究指出形式化验证方法(Formal Verification Method)是对软硬件系统进行分析和验证一种有效的方式。而模型检测(Model Checking)技术是其中一种很重要的有限状态系统自动验证技术,因其简洁和自动化程度高的特征而备受关注。它主要用于分析验证安全认证协议、通信协议、硬件检测、控制系统等方面。模型检测(Model Checking)是一种近年来比较流行的形式化验证方法。目前有基于一阶逻辑、高阶逻辑、时态逻辑、自动机、状态机等模型检测技术。行为时序逻辑TLA(Temporal Logic of Actions)是由Leslie Lamport提出的一种新的逻辑,行为时序逻辑可以在一个程序中同时表达系统模型及系统属性,使得系统形式化更为有效。目前,基于行为时序逻辑的模型检测技术也是模型检测的主流技术之一。它通过公式的形式在一种逻辑下同时表达系统模型与属性。同时它具有自己的时序规约描述语言TLA+和对应的模型检测工具TLC方便对用TLA+描述的并发系统模型进行检测。因此,这种模型检测技术具有重要的研究和利用价值。本文深入研究了模型检测技术、自动机理论和行为时序逻辑TLA,行为时序逻辑的语言TLA+以及它的验证工具TLC的结构及使用方法.在详细介绍网络协议Pastry及其工作原理的基础上,用TLA+对Pastry协议进行了分析建模同时用TLC进行了验证分析,所作的主要工作与创新之处如下:(1)深入研究行为时序逻辑TLA,及其形式化语言TLA+,自动验证工具TLC;(2)选取网络协议pastry,并对其原理及其行为进行了详细研究,分析了Join工作机制。(3)用TLA+语言对pastry协议进行建模及规约描述,通过TLC模型检测工具对规约的系统进行验证。(本文来源于《贵州大学》期刊2015-06-01）
李均涛[5]（2014）在《基于行为时序逻辑系统性质研究》一文中研究指出文章研究行为时序逻辑(TLA)中行为(Action)的性质及行为之间的关系,提出"行为活性"和"行为安全性"概念,从行为的视角重新给出系统活性和安全性的定义,使得安全性和活性定义更加直观和容易理解,并证明了新老定义的等价性。(本文来源于《信息安全与技术》期刊2014年12期）
白金山,冯天亮,吴应江,丘文峰,王梦[6]（2014）在《行为时序逻辑与自反线性时序逻辑的关系》一文中研究指出为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中,对行为时序逻辑公式的语义进行形式化定义,从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系,提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念,定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统,以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。(本文来源于《现代计算机(专业版)》期刊2014年02期）
金然,范荣荣,顾小琪[7]（2013）在《基于谓词时序逻辑的恶意代码行为描述及检测》一文中研究指出基于行为的判别已成为恶意代码检测技术研究的主流方向,现有方法容易受到拟态攻击或影子攻击的影响。针对这些问题,提出了一种全新的使用谓词时序逻辑描述恶意代码行为的方法,该方法能够同时刻画一组函数调用之间的逻辑组合、时序、参数依赖和主客体关联等关系,因此能更准确细致地描述恶意代码行为。在此基础上,提出了相应的恶意行为检测算法,通过实例测试验证了该方法的有效性。(本文来源于《计算机科学》期刊2013年09期）
赵梦龙[8]（2013）在《基于行为时序逻辑TLA的算法分析与验证》一文中研究指出行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑,它结合了行为逻辑和时序逻辑的特点,增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了Dekker算法,并利用ToolBox模型检测工具对DEKKER并发算法进行了验证。证明该算法满足互斥属性和非饥饿属性。(本文来源于《计算机光盘软件与应用》期刊2013年18期）
李均涛[9]（2013）在《基于行为时序逻辑的磁盘入侵取证研究》一文中研究指出运用假设行为时序逻辑理论体系对磁盘的文件系统进行描述,建立入侵系统模型,使用模型检测工具予以取证。该方法的目标是在反侦察攻击环境下,即在证据缺失的情况下,也能顺利地进行取证调查。(本文来源于《电脑知识与技术》期刊2013年26期）
黄贻望,袁科[10]（2013）在《并发系统中谓词行为图的行为时序逻辑表达》一文中研究指出行为时序逻辑(TLA)组合时序逻辑与行为逻辑,可以对并发系统进行描述与验证,它引入动作和行为的概念,使得系统和属性可用它的规约公式表示,但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图,对于并发转移可以用谓词行为图进行图形化表示,谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则,用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性,并用系统规约的TLA公式对谓词行为图表达能力进行证明,表明两者具有等价性,为描述和分析并发转换系统提供了一种可行的方法。(本文来源于《计算机应用研究》期刊2013年09期）
行为时序逻辑论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则对一个程序实例进行了推理验证,在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
行为时序逻辑论文参考文献
[1].陈冬火,刘全,金海东,朱斐,王辉.具有程序的静态结构和动态行为语义的时序逻辑[J].计算机研究与发展.2016
[2].唐郑熠,薛醒思,王金水,王晓峰.行为时序逻辑中四级公平性下的活性推理规则[J].计算机应用研究.2016
[3].刘照洋,龙士工.基于行为时序逻辑TLA的Pastry协议的规约与验证[J].贵州大学学报(自然科学版).2015
[4].刘照洋.基于行为时序逻辑TLA的网络协议的描述与验证[D].贵州大学.2015
[5].李均涛.基于行为时序逻辑系统性质研究[J].信息安全与技术.2014
[6].白金山,冯天亮,吴应江,丘文峰,王梦.行为时序逻辑与自反线性时序逻辑的关系[J].现代计算机(专业版).2014
[7].金然,范荣荣,顾小琪.基于谓词时序逻辑的恶意代码行为描述及检测[J].计算机科学.2013
[8].赵梦龙.基于行为时序逻辑TLA的算法分析与验证[J].计算机光盘软件与应用.2013
[9].李均涛.基于行为时序逻辑的磁盘入侵取证研究[J].电脑知识与技术.2013
[10].黄贻望,袁科.并发系统中谓词行为图的行为时序逻辑表达[J].计算机应用研究.2013