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