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

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

基于Spring框架的轻量级J2EE架构与应用

合理的J2EE架构设计方案对J2EE应用系统的开发至关重要。Spring框架包含依赖注入方式的构件组装机制、统一的事务和日志管理服务等,为搭建轻量级的J2EE架构提供了有力的支持。介绍Spring框架的体系结构,将基于Spring框架的J2EE架构与其他几种J2EE架构进行对比分析,最后给出一个运用该架构方案解决的实例。     

基于版本信息的面向对象框架实例化模式挖掘*

基于框架的面向对象开发技术是实现大规模软件复用的一种有效的途径.由于框架本身层次的复杂性,往往导致框架实例化过程的复杂和烦琐,通常采用记录框架变化点的实例化过程和约束条件的方法来解决这个问题.但是,对于那些缺乏详细记录的"遗留"面向对象框架,框架变化点实例化记录往往隐含在具体的实现细节中,从而使得"遗留"面向对象框架的复用变得十分困难.提出了一种基于版本信息获取面向对象框架的实例化模式的方法,从而辅助框架的实例化工作.     

形式化方法Designware、B的比较

用形式化方法开发软件是提高软件可靠性和开发效率的革命性途径。Designware、B是两种支持软件开发全过程的形式化方法。对它们的规约描述方法、规约求精方式、开发步骤进行比较,最后分析这两种方法各自的优缺点。     

基于软件体系结构的可复用构件模型*

在分析了构件间各种操作的基础上,将软件体系结构的概念引入现有的构件模型,用于对复合构件进行描述,从而改进了现有的构件模型,给出了一种基于软件体系结构的可复用构件模型,并给出了该模型的应用.     

论水泥混凝土路面路基技术

本文作者结合多年工作经验，主要分析填挖交界处路基不均匀沉降产生机理，并对横向填挖交界路基不均匀沉降曲线方程，以及对不均匀沉降指标对水泥混凝土路面结构的影响，以供参考。     

PAR平台中若干软件构件形式化验证技术研究

PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。     

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.