Testing systems of interacting timed finite state machines with the guaranteed fault coverage

In this paper we address the problem of deriving test suites for a system of interacting Finite State Machines (FSMs) with timed guards. We first show that unlike the general composition of timed automata, the composition of timed FSMs can be derived without uniting time variables of components and still can be described by an FSM that has a single time variable. We then discuss how tests with the guaranteed fault coverage can be derived for such composition. A simple composition example illustrates an idea behind the approach.