Property Oriented Test Case Generation

Abstract. In this paper we propose an approach to automatically produce test cases allowing to check the satis ability of a linear property on a given implementation. Linear properties can be expressed by formulas of temporal logic. An observer is built from each formula. An observer is a nite automaton on in nite sequences. Of course, testing the satis ability of an in nite sequence is not possible. Thus, we introduce the notion of bounded properties. Test cases are generated from a (possibly partial) speci cation of the IUT and the property to validate is expressed by a parameterised automaton on in nite words. This approach is formally de ned, and a practical test generation algorithm is sketched.

• Type: Conference
• Year: 2003
• Where: FATES
• Authors: Jean-Claude Fernandez, Laurent Mounier, Cyril Pachon
• Keywords: FATES 2003, Nite Sequence, Satis Ability, Test Cases