Test Case Generation for Temporal Properties

The goal of testing is to make statements about the relation between the traces of an implementation and a temporal property. This is not possible for all temporal properties. Within this paper safety and guarantee properties are identified to be testable temporal properties and for these testable properties a test case definition is given. This is done by representing a safety property as a labeled transition system and by representing the guarantee property as a finite automaton. The test case definition is applied to practical testing by using SDL descriptions to specify safety properties and by using Message Sequence Charts (MSCs) to specify guarantee properties.