In this paper a framework which uses linear time temporal logic and model checking techniques to describe the semantics a variety of test specifications is developed. These include a semantics for action words, which are a practical approach to model based testing, and coverage requirements. Features of tools that support the development of tests using this approach are also presented. While model-checking ideas are used, a model of the system is not actually required. Test sequences are directly generated from the specification of properties.