题名 行为时序逻辑中公平性的研究与完善
被引量：4
1
作者
唐郑熠 李均涛 李祥
机构
贵州大学计算机软件与理论研究所
出处
《计算机应用研究》
CSCD
北大核心
2010年第5期1788-1790,共3页
文摘
基于行为时序逻辑(TLA)的并发系统描述,就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性,无法准确地描述某些系统的行为,从而限制了TLA的描述能力。通过研究TLA中公平性的推导过程,分析公平性的概念与定义方法,并以实际例子说明它的局限性。在此基础上,提出以加入两级新的公平性方式对其进行完善。最后,证明了新公平性等级之间的蕴涵关系。完善后的公平性具有更强的描述能力,能够对系统进行更完整的描述与规约。
关键词
行为时序逻辑 公平性 并发系统 系统描述 蕴涵关系
Keywords
TLA（temporal logic of action） fairness concurrent system system description implication relation
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
题名 基于行为时序逻辑的入侵取证研究
被引量：3
2
作者
李均涛 唐郑熠 李祥
机构
贵州大学计算机科学与信息学院
出处
《计算机应用研究》
CSCD
北大核心
2011年第7期2742-2745,共4页
文摘
提出一种基于行为时序逻辑的入侵取证的形式化方法,其描述语言能够准确描述入侵证据、系统知识以及攻击行为,并具有在部分数据缺失的情况下进行非确定性推理的能力;其自动验证工具能够寻求额外的证据并可检查是否有可能的攻击与这些证据相符。实例研究表明,这种方法不依赖于具体的攻击技术和操作系统,不惧证据的缺失,能够有效搜寻更多的证据并重建可能的攻击场景。
关键词
入侵取证 行为时序逻辑 逻辑 描述语言系统验证
Keywords
computer intrusion forensic temporal logic of actions TLA＋ system verification
分类号
TP309.2
[自动化与计算机技术—计算机系统结构]
题名 行为时序逻辑中四级公平性下的活性推理规则
3
作者
唐郑熠 薛醒思 王金水 王晓峰
机构
福建工程学院信息科学与工程学院 贵州大学计算机科学与技术学院 北方民族大学计算机科学与工程学院
出处
《计算机应用研究》
CSCD
北大核心
2016年第10期3045-3048,共4页
基金
福建省自然科学基金计划资助项目(2016J05146) 国家自然科学基金资助项目(61503082) +1 种基金 福州市科技基金资助项目(2012-G-126) 福建工程学院科研启动基金资助项目(GY-Z13112)
文摘
公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则对一个程序实例进行了推理验证,在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。
关键词
行为时序逻辑 公平性 活性 推理规则 系统验证
Keywords
temporal logic of action fairness liveness reasoning rules system verification
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
题名 基于行为时序逻辑的多方协作取证研究
被引量：1
4
作者
李均涛 唐郑熠 张金磊
机构
贵州财经大学信息学院 福建工程学院信息科学与工程学院
出处
《网络空间安全》
2016年第11期82-86,共5页
文摘
论文提出了一种基于行为时序逻辑和片面性理论的多方协作取证的形式化方法,有望在多方参与的调查取证中验证不可观察的行为证据,并将其应用到一个取证实例中。
关键词
入侵取证 行为时序逻辑 片面性 多方协作取证
Keywords
computer intrusion forensic temporal logic of actions opacity multilateral cooperation intrusion forensics
分类号
TP309.2
[自动化与计算机技术—计算机系统结构]
题名 并发系统中谓词行为图的行为时序逻辑表达
5
作者
黄贻望 袁科
机构
铜仁学院数学与计算机科学系 武汉大学计算机学院软件工程国家重点实验室 南开大学信息技术科学学院
出处
《计算机应用研究》
CSCD
北大核心
2013年第9期2752-2754,共3页
基金
中央高校基本科研业务费专项资金资助项目(2012211020201) 贵州省科学技术厅 +3 种基金 铜仁市科学技术局 铜仁学院联合基金资助项目(黔科合J字LKT[2012]04号 黔科合J字LKT[2012]24号) 铜仁学院科研启动基金资助项目(TS10013)
文摘
行为时序逻辑(TLA)组合时序逻辑与行为逻辑,可以对并发系统进行描述与验证,它引入动作和行为的概念,使得系统和属性可用它的规约公式表示,但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图,对于并发转移可以用谓词行为图进行图形化表示,谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则,用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性,并用系统规约的TLA公式对谓词行为图表达能力进行证明,表明两者具有等价性,为描述和分析并发转换系统提供了一种可行的方法。
关键词
并发性 规约 谓词行为 图 行为时序逻辑
Keywords
concurrent reduction predicate behavior graph temporal logic of actions （TLA）
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 行为时序逻辑与自反线性时序逻辑的关系
6
作者
白金山 冯天亮 吴应江 丘文峰 王梦
机构
广东医学院信息工程学院
出处
《现代计算机（中旬刊）》
2014年第1期3-7,共5页
基金
广东医学院博士启动基金(No.B2011006)
文摘
为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中,对行为时序逻辑公式的语义进行形式化定义,从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系,提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念,定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统,以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。
关键词
模型检测 行为时序逻辑 语义 语法 自反性
Keywords
Model Checker Temporal Logic of Actions（TLA） Semantics Syntax Reflective
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
题名 基于行为时序逻辑系统性质研究
7
作者
李均涛
机构
贵州财经大学信息学院
出处
《信息安全与技术》
2014年第12期17-19,共3页
基金
贵州省自然科学技术基金(黔科合J字[2012]2096号) 贵州财经大学人才引进科研基金
文摘
文章研究行为时序逻辑(TLA)中行为(Action)的性质及行为之间的关系,提出"行为活性"和"行为安全性"概念,从行为的视角重新给出系统活性和安全性的定义,使得安全性和活性定义更加直观和容易理解,并证明了新老定义的等价性。
关键词
行为时序逻辑 活性 安全性 安全行为
Keywords
tla liveness safety safe action
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
题名 基于行为时序逻辑的磁盘入侵取证研究
8
作者
李均涛
机构
贵州财经大学信息学院
出处
《电脑知识与技术（过刊）》
2013年第9X期5820-5821,5832,共3页
基金
贵州省自然科学技术基金(黔科合J字[2012]2096号) 贵州财经大学人才引进科研基金
文摘
运用假设行为时序逻辑理论体系对磁盘的文件系统进行描述,建立入侵系统模型,使用模型检测工具予以取证。该方法的目标是在反侦察攻击环境下,即在证据缺失的情况下,也能顺利地进行取证调查。
关键词
入侵取证 行为时序逻辑 模型检测 磁盘技术
Keywords
Forensics TLA Model checking Disk technology
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
题名 基于行为时序逻辑TLA的时钟系统分析与检测
被引量：1
9
作者
吴勇 李祥
机构
山西大学工程学院 贵州大学计算机软件与理论研究所
出处
《电力学报》
2011年第4期310-312,321,共4页
文摘
对基于行为时序逻辑TLA的模型检测技术进行了研究,指明了TLA的语义和语法并对行为时序逻辑中的公平性问题进行了定义。用基于TLA的系统描述语言TLA+对时钟系统进行描述并用其模型检测工具TLC对其进行了验证。
关键词
计算机应用 模型检测 时钟系统 行为时序逻辑 TLC
Keywords
model checking clock system TLA TLC
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
题名 基于行为时序逻辑的安全协议研究
被引量：1
10
作者
黄佳
机构
贵州交通职业技术学院
出处
《信息通信》
2012年第4期22-23,共2页
文摘
随着计算机网络的不断发展,全球信息化已经成为社会发展的必然趋势。在网络的应用和服务中,信息安全是至关重要的环节。而安全协议是保障信息安全最基本内容之一,已广泛应用在计算机通信网和分布系统中。这样,高效准确的安全协议的研究是必不可少的。本文主要采用基于行为时序逻辑TLA的HLPSL语言形式化分析与检测Geopriv协议。
关键词
行为时序逻辑 Geopriv协议 AVISPA
分类号
TP309
[自动化与计算机技术—计算机系统结构]
题名 基于行为时序逻辑TLA的安全协议形式化分析与检测
11
作者
白圣广 龙士工
机构
贵州大学计算机科学与信息学院
出处
《贵州大学学报（自然科学版）》
2012年第2期99-101,共3页
基金
国家自然科学基金资助项目(No.61163001)
文摘
随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。
关键词
行为时序逻辑 安全协议 HLPSL
Keywords
temporal logic of actions security protocol HLPSL
分类号
TP301.6
[自动化与计算机技术—计算机系统结构]
F123.1
[经济管理—世界经济]
题名 基于行为时序逻辑TLA的算法分析与验证
12
作者
赵梦龙
机构
贵州广播电视大学
出处
《计算机光盘软件与应用》
2013年第18期74-75,共2页
文摘
行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑,它结合了行为逻辑和时序逻辑的特点,增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了Dekker算法,并利用ToolBox模型检测工具对DEKKER并发算法进行了验证。证明该算法满足互斥属性和非饥饿属性。
关键词
行为时序逻辑 PlusCal TOOLBOX DEKKER算法
分类号
TP311.52
[自动化与计算机技术—计算机软件与理论]
题名 基于TLA的UML模型形式化验证
被引量：3
13
作者
梁盟磊 王小平 薛小平 李刚
机构
同济大学电子与信息工程学院计算机科学与技术系 同济大学电子与信息工程学院信息与通信工程系
出处
《计算机工程》
CAS
CSCD
北大核心
2011年第2期72-74,共3页
基金
国家自然科学基金资助项目(60972036)
文摘
统一建模语言(UML)不能直接对所建立模型的正确性进行形式化验证。为解决上述问题,从UML模型的静态结构和动态行为2个方面分别提出结合行为时序逻辑(TLA)的模型形式化方法,在此基础上提出将UML模型转化为TLA+的形式化描述方法,并用TLC工具形式化检测TLA+描述的正确性。通过实例分析证明了该方法的有效性。
关键词
形式化方法 形式化验证 统一建模语言 行为时序逻辑
Keywords
formal method formal verification UML Temporal Logic of Actions（TLA）
分类号
TP391
[自动化与计算机技术—计算机应用技术]
题名 ARP协议的描述与TLA验证
被引量：1
14
作者
李元 吴勇 李祥
机构
贵州大学计算机软件与理论研究所
出处
《计算机技术与发展》
2010年第6期163-166,共4页
基金
美国GeneChiu基金资助项目(GFC2006-001)
文摘
随着计算机网络的发展,网络的安全性日益受到人们的关注。ARP攻击是一种非常专业化的网络攻击方式,它会给网络管理员增加很大的负担,破坏主机数据,窃取主机信息。Lesilie Lamport提出了一种新的逻辑,即行为时序逻辑(TLA)理论体系,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达程序与属性。文中介绍了ARP协议,用基于行为时序逻辑TLA的建模语言TLA+对ARP协议进行建模分析。构造了一个ARP欺骗的攻击者模型,用基于TLA的模型检测工具TLC对其进行验证并找出一条攻击者路径。
关键词
ARP协议 ARP欺骗 行为时序逻辑
Keywords
ARP protocol ARP spoofing TLA
分类号
TP393.08
[自动化与计算机技术—计算机应用技术]
题名 基于TLA的Kerberos协议符号化与检测
被引量：4
15
作者
万良 李样
机构
贵州大学计算机理论研究所
出处
《贵州大学学报（自然科学版）》
2007年第6期605-609,共5页
文摘
Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVISPA工具对HLPSL编码进行检测,结果表明用基于TLA的检测工具是宜于使用且有效的。
关键词
行为时序逻辑 角色 模型检测
Keywords
TLA role model-checking
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
题名 高校计算机专业形式化方法课程教学研究
被引量：5
16
作者
李均涛
机构
贵州财经大学信息学院
出处
《大学教育》
2012年第2期73-74,共2页
文摘
高校计算机专业开设形式化方法课程十分必要。必须设计课程目标和教学方法,并提出考核和评价学生学习效果的标准,通过严格的数学方法让学生获取对其他课程也很有益的知识、技术和能力。
关键词
形式化方法 课程教学 行为时序逻辑 系统描述
分类号
G423
[文化科学—课程与教学论]
题名 一种安全转移系统模型的构造及其运用
17
作者
万良 肖源
机构
中国人民大学信息学院数据工程与知识工程重点实验室 贵州大学计算机科学与信息学院
出处
《计算机应用研究》
CSCD
北大核心
2014年第2期558-562,共5页
基金
国家自然科学基金资助项目(61163001) 中国人民大学科学研究基金(中央高校基本科研业务费专项资金资助)项目成果(+12 XNLF06) 贵州自然科学基金项目(J[2011]2328)
文摘
为提高安全性,一般利用密码技术,但系统运行过程的安全尚显不足,为此基于行为时序逻辑TLA提出一种安全转移系统模型。通过设置安全属性,构造安全行为,使得系统在运行过程中的每次转移都满足安全属性,从而提高过程的安全性。为此,定义初始安全态、安全转移条件、安全状态、安全行为、安全运迹和安全转移系统,并证明在安全转移系统中状态处处安全。安全转移系统中强调的是系统转移过程的安全性,从而增强了系统运行的安全。通过实例的运用表明面向过程安全的建模为提高系统的安全性是有意义的。
关键词
形式化方法 行为时序逻辑 安全性 安全行为 安全转移系统
Keywords
formal methods TLA（ temporal logic of actions） safety safety action safety transition systems
分类号
TP393
[自动化与计算机技术—计算机应用技术]
题名 基于TLA+的AFDX冗余管理算法的改进
被引量：1
18
作者
库恒 龙士工 罗昊
机构
贵州大学理学院 贵州大学计算机科学与信息学院
出处
《计算机工程与设计》
CSCD
北大核心
2013年第3期837-840,853,共5页
基金
国家自然科学基金项目(61163001) 贵州省科学技术基金项目(黔科合J字[2012]2135号) 贵州大学自然科学青年科研基金项目(贵大自青基合字(2009)027号)
文摘
为了在航空应用中得到更加安全可靠的通讯系统,就目前普遍应用的标准以太网可能会出现的问题,提出了用行为时序逻辑TLA对AFDX冗余管理算法进行形式化分析。在适当的环境中,根据安全性、活性、可用性3个性质,得到两个冗余管理的推论,根据这些性质和推论,提出了3个冗余管理算法,并用TLA+语言进行详细的描述。通过模型检测,表明出RMA13为最优算法。
关键词
AFDX冗余管理算法 帧 行为时序逻辑 TLA+语言 模型检测
Keywords
AFDX redundancy management algorithms frames action temporal logic TLA＋ language model checking
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
题名 互斥协议的安全性分析
19
作者
赵梦龙 唐郑熠 万良 韦立
机构
贵州职业技术学院信息技术系 福建工程学院信息科学与工程学院 贵州大学计算机科学与技术学院 贵州师范大学数学与计算机科学学院
出处
《计算机应用研究》
CSCD
北大核心
2015年第5期1486-1488,共3页
基金
国家自然科学基金资助项目(6130900) 贵州省自然科学基金资助项目(J[2011]2328) 福建工程学院科研启动基金资助项目(GY-Z13112)
文摘
安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转移条件的约束。以此为基础,对互斥这一并发系统的典型属性进行了形式化的分析,由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。
关键词
互斥协议 属性分类 安全性 活性 行为时序逻辑
Keywords
mutual exclusion protocol classification of properties safety liveness temporal logic of action
分类号
TP309.1
[自动化与计算机技术—计算机系统结构]
题名 基于TLA的ARQ协议描述与验证
被引量：1
20
作者
吴勇 李祥
机构
山西大学工程学院 贵州大学计算机软件与理论研究所
出处
《计算机安全》
2012年第8期40-43,共4页
文摘
根据停止等待ARQ协议的算法,用基于TLA的系统描述语言TLA+对ARQ协议进行建模,用TLC验证了ARQ协议应该满足的两条基本属性。根据ARQ协议的弱点在协议中加入一个攻击者行为Intuder,用TLC验证后,出现死锁造成ARQ拒绝服务攻击。
关键词
行为时序逻辑 模型检测 停止等待协议 TLC TLA+
Keywords
TLA medelchecking ARQ protocol TLC TLA＋
分类号
TP393
[自动化与计算机技术—计算机应用技术]
