EKE协议的描述与TLA验证

行为时序逻辑(TLA)是Leslie Lamport于20世纪90年代提出的一种新的逻辑,运用这种逻辑对软件或协议系统进行建模,在一定程度上减少了由于状态空间爆炸带来的压力,它能在一种语言中同时表达模型程序与系统属性。文中首先介绍了行为时序逻辑的语法和语义,然后以EKE协议为例,用基于行为时序逻辑语言TLA+对EKE协议进行了建模分析,用TLA建模并用行为时序逻辑语言TLA+进行协议的描述,最后用TLC检测工具进行分析,发现存在中间人的重放攻击漏洞。     

基于行为时序逻辑TLA的安全协议形式化分析与检测

随着近年来网络协议的不安全性,对安全协议进行形式化分析与检测则显的非常重要。而基于行为时序逻辑TLA的模型检测是形式化分析检测方法中重要的一种。本文主要采用基于TLA的HLPSL语言形式化分析与检测H.530协议。     

基于行为时序逻辑TLA的Pastry协议的规约与验证

本文研究基于行为时序逻辑TLA的模型检测技术,阐述TLA的语义、语法和公平性问题。用基于TLA的系统描述语言TLA+对Pastry协议及其属性进行规约并用模型检测工具TLC对其进行验证。     

一种基于TLA的解决N皇后问题的方法

行为时序逻辑语言(TLA+)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。N皇后问题是一个久远的问题,回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA+去描述N皇后问题,然后使用Toolbox工具去检测n=5时该问题的全部解。     

GVim的TLA+语言插件设计与实现

GVim是一款著名的编辑器,它允许用户为方便使用而自定义插件.TLA+语言是由Les-lie Lamport设计的基于行为时序逻辑的一门系统描述语言.本文描述了为GVim编写TLA+语言插件的详细步骤.这些插件提供了关键字高亮,插入模板,缩进,以及在图形界面下调用TLA模型检测的相关命令等功能,通过使用这些插件,在用TLA+语言描述系统时可明显提高编辑效率.     

用于C语言程序验证的性质描述语言C-PDL

为了保证程序的正确性,可以先将程序抽象成模型,再采用模型检测技术对模型进行验证.模型检测工具只接受形式化的性质描述语言,而一般程序员很难正确地使用,因此,文章提出了半形式化的描述语言C-PDL,并介绍了采用C-PDL描述性质的验证系统.C-PDL采用时序逻辑语言XYZ/AE的语法结构,结合了C语言程序性质的特点,引入规范模式系统,其语法简单且描述能力强.另外,C-PDL表达式可以方便地转换成模型检测工具识别的各种时序逻辑公式.     

一种理性安全协议形式化分析方法及应用

博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证.不过在理性环境下,由于参与者对知识的自利性,ATL和ATEL都不适合形式化分析与验证理性安全协议.于是在并行认知博弈结构CEGS中引入效用函数和偏好关系,得到新的并行认知博弈结构rCEGS,并在合作模态算子《Γ》中引入行为ACT参数,提出新的交替时序认知逻辑rA-TEL-A,并基于不动点描述rATEL-A时序算子.然后基于rATEL-A,提出适合于形式化分析理性安全协议的推理系统,并对具体的理性安全协议的公平性、安全性等性质进行形式化分析.     

基于PPTL的着色Petri网的模型检测方法

为了提高着色Petri网的描述及验证能力,提出了一种基于投影命题时序逻辑的着色Petri网的模型检测方法。通过构建投影命题时序逻辑公式的否定形式等价的Buchi自动机,将它与着色Petri网的可达图相积,通过检测检测乘积图的可接受语言是否为空,从而判断用时序逻辑公式描述的系统性质是否满足。利用投影命题时序逻辑公式具有更强的表达力,可以有效地提高着色Petri网系统的描述及验证能力。     

用分布式时序逻辑形式化分析IEEE802.11i协议

基于Caleiro提出的分布式时序逻辑,在其模型中增加了挑战问题集合和挑战应答集合,将IEEE802.11i协议转化为分布式时序逻辑的事件结构语义模型.形式化分析并证明了该协议的保密性以及协议中申请者、认证者、认证服务器之间的相互认证性.结果表明,IEEE802.11i协议是安全的.     

基于FPGA的MIL-STD－1553B总线接口设计

本文在深入理解MIL—STD－1553B总线协议的基础上,设计了一种基于FPGA技术的总线控制器BC模块。采用自顶向下的方法使用VHDL语言书写总线控制器程序代码,通过FPGA平台对发送器进行了测试;结果表明,接收器的逻辑功能达到了设计要求,时序指标完全符合协议规范,实现了总线接口的功能。     

分析和设计安全协议的新逻辑的语义

文献[1]中提出了一种分析和设计安全协议的新逻辑.协议分析者可以用该逻辑来对安全协议进行分析,而协议设计者可以使用该逻辑用一种系统的方法来构造安全协议.文献[1]没有给出该逻辑的形式化语义,因为串空间模型具有良好的语义,现将新逻辑和串空间模型结合起来,给出新逻辑的串空间语义,并运用该语义证明了新逻辑的推理规则是正确的.     

基于Petri网的协议测试例自动生成

Petri网支持下的协议一致性测试是协议工程研究中的重要课题.Petri不能很好地支持一致性测试集的自动生成.针对这一问题,分析了对基本Petri网扩展的必要性,提出了一种新的用于支持协议测试的扩展的高级Petri网,揭示了其静态结构和动态行为,并提出了该Petri网到测试描述语言TTCN-3的转换规则.开发了原型系统,并应用于实际的协议一致性测试工作.     

油蚀对TLA改性沥青混合料水稳定性的影响

通过制定室内油蚀试验方案,采用浸水马歇尔和冻融劈裂试验,分析了油蚀对TLA改性沥青混合料AC-13C的水稳定性的影响规律.研究结果表明,油蚀对水稳定性的影响与TLA掺量和油蚀时间密切相关,其中,油蚀浸水残留稳定度和油蚀冻融残留强度比随着TLA掺量增加呈现先增后减的单峰变化关系,且峰值出现在TLA掺量为30%左右; 同时,初期60 min内油蚀浸水残留稳定度的降幅占总降幅的80%以上.因此,适宜的TLA掺量与及时的除油污处理可有效提高TLA改性沥青路面的抗油蚀水损坏能力.     

论文化差异对三语习得的影响——以藏族学生学习英语为例

三语习得和二语习得密切相关,但三语习得的内涵比二语习得更丰富、更复杂。由于三语习得者所面对的是三种不同的文化,文化差异对三语习得的影响较二语习得也更为严重。因此,三语习得作为一种独特的现象,应引起研究者的关注。     

空空导弹分数阶三回路自动驾驶仪的分析与参数优化

针对空空导弹飞航控制系统中存在弹体强非线性、参数不确定等问题,在对传统三回路自动驾驶仪进行分析的基础上,提出了空空导弹分数阶三回路自动驾驶仪.深入分析了分数阶三回路自动驾驶仪的各个回路特点,并比较了与传统三回路自动驾驶仪的区别.引入了基于时间绝对误差积分(ITAE)规则的遗传算法(GA),对三回路自动驾驶仪的参数进行寻优,从而实现对空空导弹的最优三回路控制.通过对两种三回路自动驾驶仪的仿真实验,对比研究了两种自动驾驶仪的时域和频域响应特性.研究结果表明,在相同的参数优化方法下,空空导弹分数阶三回路自动驾驶仪具有与传统三回路自动驾驶仪相当的结构,但时域响应更快,频域稳定裕度更大,因而更适用于空空导弹的飞航控制.     

网络安全中的两种认证协议及安全性分析

研究对称密钥算法产生的安全问题. 根据网络安全的特点设计了两种简单认证协议: 点到点简单认证协议和可信第三方的简单认证协议. 通过使用形式化分析方法（基于知识与信念推理的模态逻辑方法〖CD2〗SVO逻辑）, 对以上两个认证协议进行了安全性分析, 证实其达到了面向密钥的目标、 密钥确认目标和相互信任密钥目标.     

特立尼达湖沥青（TLA）路用性能研究

对特立尼达湖沥青的特点和使用情况进行了概述,通过室内试验,对特立尼达湖沥青的高低温性能、水稳定性和抗疲劳性能进行了分析研究．结果表明,湖沥青相对基质沥青的性能大幅提高,主要表现在软化点和耐老化性的提高上,与沥青相容性好,同时湖沥青混合料的路用性能也优于普通沥青混合料．     

TLA改性沥青混合料AC-13C配合比及性能研究

依托广东省佛山市一环城际快速干线沥青路面工程,对TLA改性沥青混合料AC-13C的配合比和性能进行了试验研究．首先分析了6种不同TLA掺量的TLA改性沥青的技术性能,从而确定了性价比优良的TLA适宜掺量为40％;其次通过正交试验法对TAC-13C的配合比进行了优化设计,提出了满足各项技术指标要求的级配建议范围,并据此进行了配合比设计,对其路用性能进行了室内检验;然后通过试验路铺筑及现场质量监控和性能检测进行了验证．研究结果表明,设计出的TAC-13C具有优良的路用性能,可应用于南方湿热地区的重交通道路．