无线射频RFID识别协议自动验证方法研究

Population Protocols是一种受生物启发的计算模型,能够表示无线网络中数量庞大但计算能力弱的多组件间的交互,它为无线传感器网络提供了一种可计算推理的理论框架。将Population Protocol理论引入到RFID识别协议中,提出了RFID识别协议系统模型验证框架;构建了标签与阅读器交互产生的状态变迁模型;最后用spin模型检测工具和LTL线性时序逻辑验证了弱公平条件下该模型的自稳定性,为分析与验证无线传感器网络中协议的正确性提供了一种行之有效的方法。     

Apla中泛型约束机制研究

泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语义的复杂约束需求问题,与完整实现GP尚有距离;以抽象程序设计语言Apla为宿主语言,提出了基于代数结构及公理语义的泛型约束方法,给出了基本数据类型、自定义抽象数据类型和子程序的3类泛型约束机制,拓展了泛型程序设计约束的应用范围.同时,支持静态语法和动态语义层约束,提高了泛型约束的精确度;借助Isabelle定理证明器,设计了泛型约束匹配检测和验证算法;进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型.实验部分给出了该泛型约束机制描述、检测及验证一系列复杂泛型约束问题的全过程,自动生成的C++模板程序的可靠性和安全性得到显著提高.     

Radl算法到Apla程序的生成系统

算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.     

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.     

基于PAR的软件服务外包开发过程应用研究

软件外包中开发效率低、可靠性差的问题一直存在。PAR（Partition and Recur）方法及高可靠软件开发平台PAR平台,在提高软件开发效率和可靠性方面能够发挥很好的作用。本文将PAR方法和PAR平台应用于外包软件开发过程,使用PAR平台成功研发中软国际实训教材中软件外包案例,在软件开发效率和可靠性方面取得显著效果。     

PAR平台数据库查询优化方案

数据库系统的查询优化技术是提高数据库系统效率的重要技术。当今Java和C＋＋等主流程序设计语言依靠SQL语句,造成数据库系统中查询复杂、繁琐、效率低下、可靠性得不到保证等。针对上述问题,在PAR（Partition And Recur）平台数据库关系代数实现机制基础上,提出和实现基于关系代数的查询优化规则设计方法。这种设计不仅提高了数据库查询效率,也为高可靠数据库的形式化开发提供了依据。     

关系代数派生算子语义表达式间等价性证明

关系代数的派生算子在关系数据库查询语言中得到了广泛应用。它们的语义有两种常见的表示方式,一种是基于原始算子的表达式,一种是基于一阶逻辑的表达式。但有关的文献资料都没有给出这两种表达式等价性的严格证明。文章尝试通过一系列等价变换,证明派生算子语义的这两种表达式间的等价性。从派生算子(主要是除算子)语义的原始算子表达式出发,根据关系代数表达式的特点,通过一步步的等价变换,得到派生算子语义的一阶逻辑表达式。所使用的变换方法能为关系代数表达式的正确性证明打下基础。     

用PAR方法构建三种Java集合类

分析了抽象程序设计语言Apla(Abstract Programming Language)定义的集合摄作的实现算法思想,用PAR方法（分划递推法,Partition-and-Recur)推导了实现集合操作的Apla程序,并分别将这些抽象程序用三种数据结构（向量（Vector)、数组（Aarray)、链表（noldep,自定义））实现,构成了自定义Java集合类库。该类库可用于Apla-Java程序自动转换系统和体现数据抽象思想的Java程序开发。     

基于嵌入式平台的并发虚拟机研究

并发程序对提高应用系统的处理能力具有重要作用,基于嵌入式平台的并发程序开发尚无统一的工具支持.本文提出了一种基于嵌入式平台的并发虚拟机(CVM)设计思想,并采用标准C实现了一个CVM模型.研究表明,它可以支持嵌入式平台中的并发程序,实现了嵌入式平台中并发程序的平台无关性和可移植性.     

软件测试在APLA→JAVA系统中的应用研究

在参阅有关软件测试资料及文献,并结合国家自然科学件测试进行了深入的研究和探索.从理论和实际相结合的角度,选用了针对性强、适用性好的测试用例,提出了适合于APLA→JAvA系统的软件测试计划、测试策略、测试方法,软件可靠性评估标准等.