University of Minnesota
Software Engineering Center

You are here

Test-Sequence Generation from Formal Requirement Models

Date of Publication: 
October 2001
Associated Research Groups: 
Publication Files: 
This paper discusses a method for generating test sequences from state-based specifications. We show how a model checker can be used to automatically generate complete test sequences that will provide arbitrary structural coverage of requirements specified in a high-level language like SCR or rsml. We have defined a language independent formal foundation for test sequence generation using model checkers that is suitable for representing software artifacts like requirements models, software specifications, and code. This paper shows a concrete application of our formal framework for test generation in the requirements modeling domain. The framework allows one to define structural coverage criteria in terms of the formal model of a software artifact and describes how test sequences can be generated to satisfy those coverage criteria using a model-checker. The approach is illustrated using examples. We define various criteria in terms of the specification language, translate those into criteria in the formal framework, and demonstrate how we generate the test sequences.
Proceedings of the Sixth IEEE High Assurance in Systems Engineering Workshop, Florida, October 2001.
@INPROCEEDINGS{TestsFromReqs:HASE01, author = {Sanjai Rayadurgam and Mats P.E. Heimdahl}, title = {{Test-Sequence Generation from Formal Requirement Models}}, booktitle = {Proceedings of the 6th IEEE International Symposium on the High Assurance Systems Engineering (HASE 2001)}, year = {2001}, month = {October}, address = {Boca Raton, Florida}, note = {To appear} }