Test Case Generation for Temporal Properties

Robert Nahm, Jens Grabowski, Dieter Hogrefe

Abstract

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.
Document Type: 
Technical Reports
Institution: 
Institute for Informatics, University of Berne
Address: 
Berne, Switzerland
Month: 
6
Year: 
1993
Note: 
Technical Report IAM-93-013
2020 © Software Engineering For Distributed Systems Group

Main menu 2