题名 软件动态执行网络建模及其级联故障分析
被引量:2
1
作者
王小龙
侯刚
任龙涛
周宽久
常军旺
王竹
机构
大连理工大学 软件 学院
大连理工大学 软件 评测 中心
出处
《计算机科学》
CSCD
北大核心
2014年第8期109-114,共6页
基金
国家自然科学基金(61272174)资助
文摘
随着人们对软件功能需求的不断增加,软件系统的结构和规模越来越复杂。如何对复杂软件系统的拓扑结构及其质量进行有效分析和评估是软件工程中亟待解决的难题。采用复杂网络理论对软件系统进行建模和求解,将软件源代码中的函数作为节点,函数之间的调用关系看作有向边,函数调用次数作为边的权重,提出了一种软件动态执行加权网络模型的构建方法。通过对TAR、GEDIT、EMACS这3个开源软件系统的建模及网络特征分析,发现软件系统动态执行的加权拓扑网络满足小世界效应和无标度特性,即符合复杂网络特性。基于此结论,进一步利用CML(耦合映像格子)网络故障传播模型对软件系统的级联效应进行了模拟,通过实验发现了影响软件级联故障的主要因子,这些因子为软件质量保证等研究提供了重要支持。
关键词
复杂网络
软件执行路径
加权拓扑网络
CML模型
级联故障
Keywords
Complex networks, Software execution route, Weighted topological network, CML model, Cascading failure
分类号
TP301
[自动化与计算机技术—计算机系统结构]
题名 基于层次化时间STM软件设计的形式化验证
被引量:1
2
作者
周宽久
任龙涛
王小龙
勇嘉伟
侯刚
机构
大连理工大学 软件 学院
大连理工大学 软件 评测 中心
出处
《计算机科学》
CSCD
北大核心
2014年第8期42-46,共5页
基金
国家自然科学基金(61272174)资助
文摘
状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法。基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性。
关键词
层次化时间状态迁移矩阵
形式化验证
有界模型检测
Keywords
Hierarchical time state transition matrix, Formal verification, Bounded model checking
分类号
TP301
[自动化与计算机技术—计算机系统结构]
题名 基于PEFSM行为模型的黑盒测试用例生成方法
被引量:1
3
作者
梁浩然
周宽久
崔凯
潘杰
侯刚
机构
大连理工大学 软件 学院
大连理工大学 软件 评测 中心
出处
《计算机科学》
CSCD
北大核心
2017年第4期234-240,共7页
基金
国家自然科学基金(61402073)资助
文摘
随着计算机软件在医疗、航天、金融等领域的广泛应用,人们对软件系统可靠性的要求越来越严格。软件测试是保证软件安全可靠的有效手段,测试用例的优劣会直接影响测试效果及测试成本。针对嵌入式系统黑盒测试问题,提出了基于概率扩展有限状态机(PEFSM)行为模型的测试用例生成方法,通过两个假设给出了该方法的适用场景,设计了正则表达式转化和展开算法,并将该方法应用于Android智能电视的黑盒测试。该方法的特点是:1)根据用户对待测系统各类操作的使用频率信息,优先测试用户常用操作,从而缩减测试用例的数量和长度;2)可人为指定测试用例的初始状态和结束状态,设置闭包循环次数和迁移之间的等待时长,从而保证测试方法的灵活性和适用性。对比实验结果表明,该方法能够降低软件测试成本,提高测试用例的错误探测效率。
关键词
可信验证
PEFSM
正则表达式
自动化测试
Keywords
Credible verification
PEFSM
Regular expression
Automated testing
分类号
TP306
[自动化与计算机技术—计算机系统结构]
题名 基于时间Petri网的嵌入式系统中断建模与验证
4
作者
周宽久
常军旺
侯刚
任龙涛
王小龙
机构
大连理工大学 软件 学院
大连理工大学 软件 评测 中心
出处
《计算机科学》
CSCD
北大核心
2014年第9期205-209,219,共6页
基金
国家自然科学基金:航天多核嵌入式软件可信性验证与系统原型(61272174)资助
文摘
嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间Petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间Petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过SMT对时间自动机的不变属性进行BMC验证。最后,通过SMT求解器Z3进行实验,实验结果证明了所提方法的有效性。
关键词
中断建模
有界模型检测
时间自动机
可满足性模理论
时间PETRI网
Keywords
Interrupt modeling
Bounded model checking
Timed automata
Satisfiability modulo theories
Time petri nets
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]