面向传值进程的谓词μ-演算与FO(HML)的完备推演系统

作者提出一个谓词μ－演算系统，目的在于描述传值进程的性质，该系统的公式和谓词相互递归定义，谓词中含有抽象式，谓词变元以及最大和最小不动点，其语义模型是带赋值的符号迁移图所诱导的迁移系统，并且该系统包含Hennessy-Milner逻辑的一阶扩弃FO（HML）作为子系统，作者用例说明了本演算系统在表达传值进程性质方面的优越性，该文后半部分主要给出了FO（HML）的一个推演系统，并运用判定树（Tableau)的方法，证明了所给出了推演系统是完备的。     

A Graphical μ—Calculus and Local Model Checking

A graphical notation for the propositional μ-calculus,called modal graphs,is presented.It is shown that both the textual an equational presentations of the μ-calculus can be translated into modal graphs.A model checking algorithm based on such graphs is proposed.The algorithm is truly local in the sense that it only generates the parts of the underlying search space which are necessary for the computation of the final result.The correctness of the algorithm is proven and its complexity analysed.     

传值进程模型检测中诊断信息的生成

诊断信息自动生成是模型检测方法的基本特征之一，对分析和排错具有重要的意义，讨论了传值进程模型检测中诊断信息的生成问题，引入了两种诊断信息的表示结构：证明图和示例；提出了两种诊断信息的构造算法，所采用的方法是从检测过程保存的依赖信息中抽取证明图和示例，这样可以继承已有的信息，从而减少计算量，相应的算法已经实现并用实例作了分析测试，实验结果表明该方法是有效的。     

软件与网络安全研究综述

互联网已经渗入人类社会的各个方面,极大地推动了社会进步。与此同时,各种形式的网络犯罪、网络窃密等问题频频发生,给社会和国家安全带来了极大的危害。网络安全已经成为公众和政府高度关注的重大问题。由于互联网的大量功能和网络上的各种应用都是由软件实现的,软件在网络安全的研究与实践中扮演着至关重要的角色。事实上,几乎所有的网络攻击都是利用系统软件或应用软件中存在的安全缺陷实施的。研究新形势下的软件安全问题日益迫切。本文从恶意软件、软件漏洞和软件安全机制三个方面综述国内外研究现状,进而分析软件生态系统面临的全新安全挑战与发展趋势。     

关于蜕变测试和特殊用例测试的实例研究

提出了基于蜕变测试方法的集成测试环境MTest,进而为检验蜕变测试方法的能力和效率,以稀疏矩阵乘法程序为例设计了一组实验.该实验基于变异分析技术,分别以mutation score和错误发现率为度量指标,定量地分析和对比了特殊用例测试,以特殊测试用例和随机测试用例为源测试用例的蜕变测试这3种方法的测试能力和效率.该实验可在MTest测试环境下自动完成.实验结果表明,蜕变测试与特殊用例测试之间是互补的,而且就蜕变测试的源测试用例而言,随机测试用例在测试能力和效率上优于特殊测试用例.     

π-演算互模拟判定算法的优化和实现

π-演算采用互模拟作为进程等价的准则.对有限状态的π-演算进程互模拟等价是可判定的,由此提出了互模拟检测算法的一种优化技术.该技术基于只将输入名字实例化为在以后的等名测试中用到的自由名字.通过实例说明这一优化技术可大大减少所用的时间和空间,并证明了优化算法的正确性.