Towards Deriving Test Sequences by Model Checking