一种基于自动机理论的LTL检验符号优化方法

模型检验是一种重要的形式化自动验证技术。检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验。由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机。     

基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

基于ASP的CSP进程描述与组合研究

前期工作中,为解决CSP模型检测不支持一次运行验证多条性质的问题,构建了基于ASP的CSP模型检测框架,但其存在着可描述并发进程形态不完善与可验证并发系统规模受限的问题。构建了全新的并发系统ASP描述体系,其解决了前期工作中前缀描述不允许出现类环状结构的问题,可完整描述各种形态的CSP进程。研究了并发组合进程生成技术,它可使多个进程自动化并发组合,并生成一个满足所有行为特性、具有一致结构特性的新进程,保持了验证框架内进程描述的一致性,有利于并发进程的抽象与验证。实验表明了基于ASP的CSP进程描述与组合进程生成技术的有效性,以及基于该ASP描述体系的系统性质验证的可行性。     

一种基于熵的OBDD变量排序算法

有序二叉决策图（OBDD）是一种有效表示布尔函数的数据结构，其大小依赖于所采用的变量序。熵是定量描述布尔函数中变量重要性的一种方法。基于变量的熵值分析了高质量变量序的特征，给出了一种基于熵的OBDD变量排序算法。实验结果表明：该算法与模拟退火算法和遗传算法结果相当。时间仅为相应算法的80．84％和29．79％。     

基于改进的Tent混沌万有引力搜索算法

万有引力搜索算法(gravitational search algorithm,GSA)相比于传统的优化算法具有收敛速度快、开拓性能强等特点,但GSA易陷入早熟收敛和局部最优,搜索能力较弱.为此,提出一种基于改进的Tent混沌万有引力搜索算法(gravitational search algorithm based on improved tent chaos,ITC-GSA).首先,改进Tent混沌映射来初始化种群,利用Tent混沌序列随机性、遍历性和规律性的特性使得初始种群随机性和遍历性在可行域内,具有加强算法的全局搜索能力;其次,引入引力常数G的动态调整策略提高算法的收敛速度和收敛精度;再次,设计成熟度指标判断种群成熟度,并使用Tent混沌搜索有效抑制算法早熟收敛,帮助种群跳出局部最优;最后,对10个基准函数进行仿真实验,结果表明所提算法能够有效克服GSA易陷入早熟收敛和局部最优的缺点,提高算法的收敛速度和寻优精度.     

基于动态调整简化粒子群优化的组合测试用例生成方法

优化的组合测试中的一个关键是生成的测试用例能够覆盖更多的组合,而粒子群算法在生成强组合覆盖用例方面有其独特的优势和能力。文中提出了一种基于动态调整简化粒子群优化的组合测试用例生成方法。该方法基于粒子群算法生成测试用例,结合混合的优先级one-test-at-a-time策略和基于动态调整的简化粒子群算法生成组合测试用例集,排除了速度因素对粒子优化过程的影响。定义了一个粒子收敛指标,以粒子群早熟收敛程度为依据来动态调整惯性权值,以防止粒子陷入局部最优和后期出现收敛速度慢的情况,从而提高粒子群算法所生成的覆盖表的覆盖组合能力。通过对比实验表明,基于动态调整的简化粒子群优化算法在用例规模和时间成本上具有一定的优势。     

Statchart规格语言的语法分析研究

Ｓｔａｔｅｃｈａｒｔ是一种用以规约复杂反应式系统行为的可视化语言。它在一些方面上扩展了典型的状态转移图,保留甚至发挥了可视化要求。实际上,Ｓｔａｔｅｃｈａｒｔ满足层次的描述,包括高层和低层事件,更显著地是采用广播通信机制产生连锁反应而引起多层并发。     

面向类集成测试序列生成的强化学习研究

集成测试是软件测试过程中不可缺少的步骤, 针对在集成测试中如何对系统中的类合理排序的问题, 国内外研究者提出了多种生成类集成测试序列的方法, 然而他们大多没有将测试桩复杂度作为评估测试代价的指标.针对该问题, 提出面向类集成测试序列生成的强化学习研究方法, 以总体测试桩复杂度为评价测试代价的指标, 生成测试代价尽可能低...