In this technical report, a comprehensive testing theory for model-based testing against symbolic nite state machines (SFSM) is presented. It covers both conformance testing for language equivalence (the input/output language observable at the interface of the system under test (SUT) should be the same as the language of the reference model) and property-oriented testing (the SUT should ful l a set of properties that are also ful lled by the reference model). Part I describes the general theory for arbitrary nondeterministic SFSMs. It presents an exhaustive testing strategy (every erroneous SUT from a given fault domain fails at least one test case) for property-oriented testing. It is shown that the property-oriented testing theory provides a complete (the SUT fails at least one test case if and only if it violates language equivalence) test strategy for language equivalence testing as a corollary. In Part II, the class of admissible reference SFSMs is specialised to machines with separable alphabets. While this restriction still contains practically relevant models, it allows for a re ned testing strategy proving language equivalence with signi cantly smaller test suites than those induced by the general theory. Part I of this document has been submitted in similar form to the Software and Systems Modeling (https://www.springer.com/journal/10270) journal and is currently under review. Part II has been submitted in abridged form to the Fundamentals of Software Engineering conference FSEN 2023 (http://fsen.ir/2023/).

The zip archive associated with the technical report contains the open source tool version used for demonstration purposes.