文献类型：期刊文章

作　　者：张琛[1,2] 段振华[1,2] 田聪[1,2] 鱼滨[2]

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071 [2]西安电子科技大学计算机学院,西安710071

出　　处：《计算机研究与发展》

基　　金：国家自然科学基金项目(61420106004;61322202;61303031;61272117;61133001;61172147);中央高校基本科研业务费专项资金项目(K5051303005)

年　　份：2015

卷　　号：52

期　　号：7

起止页码：1604-1619

语　　种：中文

收录情况：AJ、BDHX、BDHX2014、CSA-PROQEUST、CSCD、CSCD2015_2016、EI、IC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2.0序列图对模块之间交互行为进行描述.采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为Promela模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径.给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试.实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性.

关 键 词：分布式软件系统 建模  模型检测  验证  测试用例

分 类 号：TP311]