Towards Test Purpose Generation from CTL Properties for Reactive Systems

This paper presents an approach for the generation of test purposes in the form of labelled transition systems from specifications of properties in CTL. The approach is aimed at adapting the model checking process, by extending search algorithms to perform further analysis so that examples and counter-examples can be extracted. An algorithm for the generation of test purposes through analysis over the examples and counter-examples is presented, along with a case study to show the correspondence between the CTL properties and the generated test purposes.