Complete FSM Testing Using Strong Separability
Robert M. Hierons, Mohammad Reza Mousavi
TL;DR
The paper tackles conformance testing for quantitative FSMs where outputs are noisy, arguing that classical apartness is too strong. It introduces strong separability, a weaker yet effective notion defined via a metric $m$ and threshold $t$, and adapts the Harmonized State Identifiers (HSI) method to achieve $m$-complete test suites under this notion. The approach extends to the W-method and Wp-method, proving completeness when specification states are pairwise strongly separable and state identification uses strong separation. A discretized thermostat example demonstrates that using separability alone can yield incomplete test suites, while strong separability restores completeness. This work enables robust, complete MBT for cyber-physical and stochastic systems under metric-based conformance.
Abstract
Apartness is a concept developed in constructive mathematics, which has resurfaced as a powerful notion for separating states in the area of model learning and model-based testing. We identify some fundamental shortcomings of apartness in quantitative models, such as in hybrid and stochastic systems. We propose a closely-related alternative, called strong separability and show that using it to replace apartness addresses the identified shortcomings. We adapt a well-known complete model-based testing method, called the Harmonized State Identifiers (HSI) method, to adopt the proposed notion of strong separability. We prove that the adapted HSI method is complete. As far as we are aware, this is the first work to show how complete test suites can be generated for quantitative models such as those found in the development of cyber-physical systems.