基2的流水式快速傅里叶变换处理机的形式化模型

快速傅里叶变换(FFT)的应用领域非常广泛,其硬件实现方法多种多样。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是不能穷尽模拟全部输入情况,而形式化方法使用纯数学手段证明电路具有某些属性,从而证明其正确性。所以用形式化方法验证FFT电路的正确性具有极强的实用价值。形式化验证的第一步工作是对要验证的电路进行建模,因此本文首先介绍了国内外FFT形式化建模的主要方法和优缺点,然后用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,显示了重写系统用于复杂硬件电路建模的优越性,为进一步的电路正确性验证奠定基础。     

一种Web服务组合的数学模型

为了更好地分析和验证Web服务组合,提出了一种描述服务间消息交互的Web服务组合数学模型.首先定义了个体服务形式化模型,并分析了相关性质,然后定义了消息交互的各种逻辑以及服务组合模式,并对消息交互逻辑进行了分析和实现,在此基础上,给出了服务组合模型的定义,并通过个体服务控制器、消息逻辑控制和全局控制算法实现了Web服务组合过程.该模型简洁灵活,具有可扩展性.实例分析表明,该模型能够对服务组合中的消息交互进行模拟.     

基于Object-Z的带OCL约束的UML类图形式化描述

UML OCL是基于一阶谓词逻辑和集合论的形式化语言,用它对UML类图进行约束后类图便具备严格语法和精确语义,同时也具备了演绎验证的基本条件;但由于目前的建模工具还无法对缺乏精确语义的UML类图进行有效的演绎验证.因此提出了一种带OCL约束的UML类图通过Object-Z进行形式化描述的方法,这样便可以充分利用Object-Z强大的演绎验证能力来验证UML类图的正确性和是否具有某种性质等.     

从逻辑全知问题认定看当前基于逻辑的agent研究的两个认识盲点

通过对当前逻辑全知问题的认定过程进行仔细的分析和严格的逻辑论证后发现,这一结论的得出主要来源于人们关于模态逻辑用于agent研究的两点模糊认识.在此基础上进一步指出,如果承认逻辑推理的过程意义,并且不用意识系统的特征来约束逻辑系统,那么就不会有真正意义上的逻辑全知问题存在.该结论无疑对当前基于模态逻辑的agent形式化研究具有十分重要的意义.     

一种基于构件的分布式软件构架描述语言

针对分布式软件系统规模和复杂性不断增大的特点，在扩展传统属性文法的基础上提出了一种基于构件的分布式软件构架描述语言（DSADL），详细描述了DSADL的设计目标、组成元素以及形式化描述基础，并实现了分布式软件构架集成开发环境（EDAD）。由于DSADL结合了SADL与构件技术，因此它既有严格的语义基础，同时又具有构件的可复用性、易移植性的特点。实践证明，DSADL能够有效辅助分布式软件设计人员在构架层次上对系统进行分析的设计，从而提高系统的开发效率。     

低成本RFID协议的设计及BAN形式化分析

目的通过分析现有的典型RFID认证协议的效率与成本,针对数字化图书馆RFID认证协议的高成本问题,提出一个低成本的RFID认证协议。方法通过去掉标签中的随机数模块,然后利用阅读器存储能力强、存储随机数模块来确保发出消息的新鲜性。结果该低成本RFID认证协议仅使用一对提前预约好的密钥对,降低了标签的硬件成本和计算能力。结论通过BAN形式化分析,该协议达到了预期的安全协议的认证目标,非常适合于低成本的RFID系统。     

软件过程领域本体的构造

针对目前软件过程领域知识缺乏明确统一的表示、不同组织构造的过程模型缺少互操作性而难以共享和重用的情况,划分并描述了软件过程的顶层本体;在此基础上,对其中包含的任务描述、过程模型和过程实施与改进三个核心本体分别进行了展开和细化,给出了涉及到的关键概念的形式化定义.传统的本体系统并不适宜描述动态过程,因此使用谓词逻辑定义了过程本体中概念间的基本关系,以此来表示和描述软件过程模型的“柔性”和动态知识,使不同的参与者易于交流而达成共识,为构造可共享、易重用的过程模型元模型提供坚实、统一的基础.     

从形式化规范自动生成系统级状态机

形式化方法能精确、无二义地描述软件规范,但其可读性、可理解性差以及缺乏有效的自动测试工具.鉴于此,提出一种新的方法将支持面向对象开发的形式化语言所描述的软件规范自动地转化为系统级状态机,从而改善其可读性与可理解性.实际应用表明,这种方法可以提高形式化规范的可读性与可理解性.     

改进的上下文无关文法及其语法分析

针对一些语言的实际应用情况,对标准的上下文无关文法作了改进,将标准的上下文无关文法定义中的非终结符集合和终结符集合进行细化,使得单词推导和句子推导可以使用同一个过程,即词法分析和语法分析可以在同一个语法分析过程完成.还给出了改进后文法的分析算法及算法的时间复杂度分析,证明用这种改进的方法进行语言文法定义更直观、简洁,其分析算法的时间复杂度优于标准上下文无关文法的分析算法.     

通信协议测试的形式化技术

自然语言协议的自动形式化是通信协议自动测试的前提,从而也是数据链协议自动测试的重要研究方向.此问题出现已久,但尚无可靠解决方案.隐词形理论和格语法是排岐能力很强的自然语言处理方法.运用此套方法.通过分析协议文本,确定隐词形特征,可编写出隐词形词典、隐词形语法规则以及自动机生成规则.根据这些词典、规则,可生成自然语言协议文本对应的自动机.本方案有助于解决自然语言协议文本自动形式化,实现通信协议测试的全面自动化.