English

应用科学学报 >

2011 , Vol. 29 >Issue 5: 529 - 536

DOI: https://doi.org/10.3969/j.issn.0255-8297.2011.05.014

计算机科学与应用

 用模型检验产生安全性质的测试

展开
  • 1. 上海大学计算机工程与科学学院，上海200072
    2. 上海市计算机软件评测重点实验室，上海201112
曾红卫，博士，研究员，研究方向：软件测试和形式化验证，E-mail: zenghongwei@shu.edu.cn；缪淮扣，教授，博导，研究方向：软件工程、形式化方法，E-mail: hkmiao@shu.edu.cn

收稿日期: 2010-12-08

  修回日期: 2011-02-20

  网络出版日期: 2011-09-30

基金资助

国家自然科学基金(No.60970007, No.61073050)；上海市自然科学基金(No.09ZR1412100)；上海市科学技术委员会项目基金(No.10510704900)；上海市重点学科建设项目基金(No.J50103)资助

收起

Generate Safety Property Tests Using Model Checking

Expand
  • 1. School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China
    2. Shanghai Key Laboratory of Computer Software Testing and Evaluating, Shanghai 201112, China

Received date: 2010-12-08

  Revised date: 2011-02-20

  Online published: 2011-09-30

Fold

摘要

摘要： 安全关键系统必须满足规定的安全性质. 测试生成通常独立于给定性质，“先验证再测试”的方法不能保证安全性质被测试. 为此，该文提出了一种基于输入-输出标记迁移系统的安全性质测试方法. 用输出变异建立被测实现的输出-完全模型，通过发现危险迹产生测试用例. 给出了基于图结构覆盖的安全性质测试准则，提出了形式化测试准则的方法. 使用模型检验器NuSMV检验输出-完全模型可产生既满足结构覆盖又与安全性质相关的测试用例.

关键词： 安全性质; 模型检验; 测试生成; 危险迹

本文引用格式

曾红卫1， 缪淮扣1;2 .  用模型检验产生安全性质的测试[J]. 应用科学学报, 2011 , 29(5) : 529 -536 . DOI: 10.3969/j.issn.0255-8297.2011.05.014

Abstract

Abstract: Safety-critical systems must satisfy given safety properties. Generally, the method of "verificationthen-testing" does not guarantee that the given safety properties are tested because test generation is independent of given properties. In this paper, we propose to test safety properties based on the input-output labeled transition system. Output mutations are applied to construct the output-complete model of an implementation under test. Test cases are generated by finding out dangerous traces. We give safety property test criteria based on the structural graph coverage, and propose a method to formalize the test criteria. NuSMV is used to
model check the output-complete model to generate the test cases that are relevant to the given safety property and satisfy the structural coverage.

Key words： safety property; model checking; test generation; dangerous trace

Options
文章导航

/

〈 〉