Timed Testing under Partial Observability

To steer model-based conformance testing of real-time systems towards certain test purposes or test coverage, many testing methods need (to be enhanced with) the assumption of full observability of the System Under Test (SUT), which means that the tester can observe precisely what state or configuration the SUT is in, or can uniquely infer one such state or configuration by observing an externally observable timed input/output action sequence on the tester/SUT interface. However, in practice this is often not the case due to e.g. the internal component interactions inside the SUT, or the limited precision sensors that we use to measure the SUT. This paper studies the problem of testing timed systems that are only partially observable. We model the SUT using Timed Game Automata (TGA) which has internal actions, uncontrollable outputs and timing uncertainty of outputs. We define the partial observability of SUT using a set of predicates over the TGA state space, and specify the test purposes in Computation Tree Logic (CTL) formulas. A recently developed partially observable timed game solver is used to generate winning strategies, which are used as test cases. We propose a conformance testing framework, define a partial observation-based conformance relation, present the test execution algorithms, and prove the soundness and completeness of this test method (i.e., a detected error is really an error, and if the SUT violates the test purpose, then a test case can be generated to detect this violation). Experiments on some non-trivial examples show that this method yields encouraging results