This technical report is an extended version of a paper with the same title, submitted by the authors to the SEFM 2021 conference https://sefm-conference.github.io. In this paper, new contributions to property oriented testing (POT) against SFSM models are presented. While several POT approaches are known, none of these is exhaustive in the sense that every implementation violating the property is uncovered by a given test suite under certain hypotheses. On the other hand, numerous exhaustive theories for testing against models specified in various formalisms exist, but only for conformance testing. Since a hybrid approach using both models and properties seems to be preferred in industry, this paper presents an approach to close this gap. For given properties that are at the same time represented in a reference model, a test suite derivation procedure is presented, and its exhaustiveness is proven. The technical report extends the paper by full proofs for the lemmas and theorems stated there, and it discusses examples regarding the test case reduction achievable when testing for specific properties instead of checking full model conformance.

Funded by the Deutsche Forschungsgemeinschaft (DFG) -- project number 407708394.