行为时序逻辑中公平性的研究与完善

基于行为时序逻辑(TLA)的并发系统描述,就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性,无法准确地描述某些系统的行为,从而限制了TLA的描述能力。通过研究TLA中公平性的推导过程,分析公平性的概念与定义方法,并以实际例子说明它的局限性。在此基础上,提出以加入两级新的公平性方式对其进行完善。最后,证明了新公平性等级之间的蕴涵关系。完善后的公平性具有更强的描述能力,能够对系统进行更完整的描述与规约。     

BAN逻辑的可靠性分析与改进

BAN逻辑的推理过程中可能引入错误的推理条件,导致不安全的协议被验证为安全的。为解决该问题,对消息的形式化描述方式进行改进,在消息含义推理规则中加上一个隐含但不能被忽略的条件,以增强验证的可靠性,通过对发送和推理的消息单元进行限定,使消息新鲜性判定规则适用于更多类型的协议安全性验证。     

RSA密码算法及其Java实现

RSA密码算法是目前公认的,在理论和实际应用中最为成熟和完善的一种非对称密钥体制。该文对其原理进行了介绍,并证明了该算法的正确性。最后,使用Java语言编程实现了RSA密码算法,并进行了测试。     

OWL-S过程模型的形式化描述与相容性分析

构建组合服务的形式化模型是对其进行验证的前提与基础,然而缺乏统一的构建框架使得建模过程变得难以把握且无法实现自动化。通过对确定型有限自动机的扩展,建立了用于描述OWL-S过程模型的有限迁移系统——服务过程自动机,为组合服务的形式化建模提供了统一框架和自动化基础。同时,通过分析服务过程自动机的可接受位置及其在组合过程中可能产生的约束,将相容性划分为三个等级,从而能够在不同强度的可靠性要求下进行组合服务的验证工作。     

互斥协议的安全性分析

安全性和活性是两大基本的系统属性,对于指导系统的设计与验证具有重要意义。通过对它们原始定义的形式化梳理,发现其缺乏对状态序列的具体约束。针对这一问题,使用对系统动作刻画更完善的行为时序逻辑进行了重定义,加入了初始状态和转移条件的约束。以此为基础,对互斥这一并发系统的典型属性进行了形式化的分析,由此说明如何判断一个属性是否满足安全性或活性的定义。该技术为实现系统性质的自动推理与验证提供了形式化基础。     

语义Web中本体概念的语义匹配分离方法

本体概念能够有效表达Web服务的语义信息,可通过推理机实现自动语义匹配,但推理机的推理过程比较耗时,会对服务计算技术多个环节的效率产生很大影响。以本体概念间的匹配度为基础,建立公共本体概念库,可在不影响本体概念表达能力的前提下,实现语义匹配过程的分离。为适应公共本体概念库的动态特性,给出对其进行更新(添加、删除和修改)的算法。实验结果表明,该方法大幅提高了语义匹配的效率,且不会对语义匹配的性能产生影响。     

基于位运算的N皇后问题的解法

N皇后问题一般是用回溯法进行求解,常规的做法是用数组来模拟棋盘,但是运行效率却不高。基于位运算的N皇后问题的解法,将列冲突转化为行冲突,以整型数的二进制形式来模拟集合,用位运算来实现集合运算。通过编程测试,证明此种解法能够大大提高运行效率。     

基于创新课程教学的创新人才培养

分析数据库系统原理课程内容的特点,提出采用创新的教学方法,有目的地在预设教学场景中对学生的思维活动进行有效引导。     

基于连续ARQ协议的隐蔽洪水攻击

通信协议设计时的疏漏很容易造成严重的后果,因此有必要采用形式化的方法来保证协议的安全性和可靠性.模型检测是一种具有工业应用前景的形式化分析方法,并具有很高的自动化程度,适合于协议的分析与验证.文中采用模型检测工具SPIN对连续ARQ协议建模,通过验证该协议的基本属性证明所建模型的正确性.然后依据Dolev和Yao的思想加入攻击者模型再进行分析,发现了连续ARQ协议的一个新漏洞,攻击者能够利用这个漏洞造成大量冗余数据的传输和存储.这种攻击建立在互信的数据传输基础上,且攻击者并不直接发送冗余数据,因此具有很高的隐蔽性.