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

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

基于TLA的Kerberos协议符号化与检测

Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVISPA工具对HLPSL编码进行检测,结果表明用基于TLA的检测工具是宜于使用且有效的。     

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

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

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

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

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

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

基于ATL的KM非否认协议形式化分析

研究ATL逻辑及其在电子商务协议形式化分析中的应用,用ATL逻辑语言对KM协议进行描述与分析,并对协议的各参与方和可信第三方TTP的基本行为进行建模.     

TLA改性沥青配合比设计及路用研究

特立尼达湖(TLA)改性沥青是一种混合了TLA沥青的改性沥青制成品,拥有多项出色的路用性能,沥青混合料均匀,改善沥青和沥青混合料的温度敏感性,增强在高温环境下的稳定性和抗变形能力,以及抗水损害能力等。在高速公路施工中采用并取得了良好效果,介绍了TLA改性沥青混合料配合比设计,施工工艺及质量控制。     

高速公路TLA改性沥青路面的施工关键技术控制探讨

特立尼达湖沥青（TLA）作为一种沥青改性剂掺加到石油沥青中，具有良好的高温稳定性和低温抗裂性。目前日益广泛应用于高速公路的建设。本文从摊铺与碾压两个环节，针对高速公路TLA改性沥青路面的施工关键技术进行分析，以期为高速公路建设水平的提高提供参考和借鉴。     

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

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

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

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

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

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

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

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

一种具备数据自校验功能的串行通信协议设计与实现

在以可编程逻辑器件为核心的多节点系统中,为增强系统纠错能力和可用性,设计具备数据自校验功能的串行通信协议SIP。SIP协议采用主端发起从端响应的通信机制,数据收发均由主端发起,并在通信过程中建立数据反馈机制,由主端实时校验数据正确性,保证数据传输的可靠性。SIP总线使用可编程逻辑语言编写实现,已应用于工控领域的现场控制中,具有良好的通用性和使用价值。     

数字逻辑电路在EDA实验开发系统中的仿真设计

数字逻辑电路是重要的硬件基础课程,也是一门与应用密切相关的课程,其应用理论与方法随数字电路器件的发展而不断变革,EDA实验系统是为在系统可编程器件提供一个实验平台。课题研究的内容是基于EDA（电子设计自动化）实验系统,以VHDL为硬件描述语言,以Max＋Plus Ⅱ为软件开发工具,设计了数字逻辑电路的实验程序,为数字电路初学者的逻辑设计抛砖引玉。     

UML 顺序图的一种形式化描述方法

统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。     

基于时序逻辑语言XYZ/E的实时系统应用研究

针对实时系统在计算机系统应用中的重要性,采用形式化方法是保证实时系统软件开发正确性的一种重要途径,而时序逻辑这种形式化方法是研究实时系统的一个重要的理论基础。本文给出了时序逻辑语言XYZ/E的相关介绍,并利用XYZ/E的子语言XYZ/RBE与XYZ图描述了煤气炉实时控制问题。     

基于XYZ/ADL描述的选修课管理系统体系结构

XYZ／ADL是一种基于时序逻辑语言XYZ／E的可视化体系结构描述语言。文章使用XYZ／ADL对高校选修课管理系统的体系结构、客户端组件及服务器端组件进行了抽象描述，并对服务器组件中选课这一事件进行了详细描述。