设计模式指导的软件分簇方法

程序理解是一个从计算机程序中获取知识信息的过程,其主要目的是获取软件的各种有关知识以理解开发者的意图,从而支持针对现有或遗产软件系统进行软件评审、错误定位、反向工程、再工程、迁移、维护和复用等软件工程实践.本文提出一种设计模式指导的分簇方法,该方法采用程序中蕴涵的设计模式信息指导开源软件的分簇,运用"分而治之"的策略辅助程序开发者和维护人员快速、方便地理解代码.首先,采用设计模式检测技术从程序代码中抽取设计模式信息;然后,基于设计模式中角色间的相互关系,利用检测出的设计模式信息指导分簇;最后,对分簇结果可视化,以辅助程序理解.基于以上研究工作,开发了原型工具TasteJ并进行了实例研究,设计并实现了以人工为基准的实验来检验本文提出的软件分簇方法,并通过7个软件分簇度量函数,从统计的角度将其与现有主流软件分簇方法进行分析和比较,实验结果显示出本文所提方法的优势.     

基于随机时间自动机和统计模型检验技术的无线传感网络协议建模与分析

近年来，传感器技术得到了长足而有效的提升，无线传感网络（WSN）以其开放、动态的特征获得了极大的关注，并成为了互联网计算的一个重要组成．WSN系统行为复杂，经常面临信息丢失、节点动态变化等不确定因素，且网络中的节点一旦部署将很难更改、维护．因此，为了保证相关应用的正常工作，在系统设计阶段对WSN中的底层协议进行质量保障就成为了一项非常重要的研究问题．系统设计人员不仅需要保证协议功能上的正确性，还应该评估协议在目标工作环境下的性能，以保证其可以胜任相应的工作需求．针对以上问题，本文提出了一种基于随机时间自动机和统计模型检验技术的WSN协议建模、分析和评估途径．在建模阶段，首先将采用时间自动机对协议在理想环境下的基本业务流程进行建模．考虑到WSN系统实际工作中会遇到的各种不确定性因素，将用带权分枝来对模型进行扩展，生成协议的随机时间自动机．在验证阶段，首先采用经典模型检验技术，在理想时间自动机上检验相关功能性质，保证协议工作逻辑的正确性．为评估协议在不同条件下的具体性能，则在随机时间自动机上用统计模型检验技术对其进行数值分析，以进行参数配置、性能预测、协议比较等工作．为展示该途径的可用性及其技术细节，本文对两种著名的WSN时间同步协议，TPSN和FTSP分别进行了完整的建模与评估．     

Model Checking over Paraconsistent Temporal Logic

Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies （inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed）. In this paper, we propose the use of a guasi-classical temporal logic （QCTL） for supporting the verification of temporal properties of such systems even where the consistent model is not available. Our models are paraKripke structures （ extended standard Kripke structures）, in which both a formula and its negation are satisfied in a same state, and properties to be verified are expressed by QCTL with paraKripke structures semantics. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.