Thank you all for your answers. I'd like to try to give some short explanation.

The W-method (Chow, 1978) is one of the most general ways for generating tests from a finite state machine. It creates an m-complete test suite, with m being the maximum number of assumed additional states in the Implementation Under Test (which might be a black box). With this test suite all faulty behaviors (erroneous outputs) in an Implementation Under Test can be detected - or the absence of faults can be proven. So the W-Method is a way to guarantee complete fault coverage for all errors with regard to a reference model given as an FSM, as long as the IUT has not more than m states.

It generates shorter test suites (less test cases) than a naive approach would. WP-Method or HSI method and all the newer methods aim to shorten the test suite while still guarantee to detect all errors. There has been a lot research in the last few years.

My problem is: I want even shorter test suites. But with less requirements. I don't need/want to have a test suite that guarantees to detect all erroneous outputs. It's enough to detect only some errors: those erroneous outputs that effect certain properties.

So the idea was: Is there a property-oriented approach for model based generation of test sequences with FSMs?

Applying the WP-Method to a simplification or abstraction of the original FSM sometimes results in even more test cases than applying the Wp-Method to the original FSM. I don't know how good the results are when other methods are applied to an abstraction FSM.

I'm looking for a way (whether with based on some of the methods mentioned above or not) to guarantee shorter test suites when focussing on certain properties only.

I thought maybe someone suggests an approach for property oriented testing with FSM that he thinks could be more promising.