Complete property-oriented testing

Abstract

This PhD thesis introduces new methods for property-oriented testing of systems with finite internal states but potentially infinite input/output domains. It focuses on properties defined in Linear Temporal Logic (LTL) and uses Symbolic Finite State Machines (SFSMs) for modeling. The thesis addresses gaps in existing literature by providing exhaustive testing approaches.

Two main methods are presented: The first is a model-based testing approach that modifies traditional conformance testing for FSMs to work with SFSMs, enabling exhaustive property violation checks with potentially smaller test suites. The second is a complete property-oriented testing approach based on black box checking, which is enhanced to work with SFSMs and optimized for better runtime performance through reduced equivalence checks and the incorporation of fuzzing.

Both methods are evaluated for their efficacy through automation and experiments, and further optimizations are discussed.