Complete FSM Testing Using Strong Separability

TL;DR

This paper introduces strong separability as an improved concept over apartness for model learning and testing in hybrid and stochastic systems, adapting the HSI method to ensure completeness in quantitative models.

Contribution

It proposes strong separability to overcome apartness limitations and adapts the HSI testing method to achieve completeness for quantitative models.

Findings

Strong separability addresses shortcomings of apartness in hybrid systems.

The adapted HSI method is proven to be complete.

First demonstration of complete test suite generation for cyber-physical system models.

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.