Testing timed systems modeled by Stream X-machines

摘要

Stream X-machines have been used to specify real systems where complex data structures. They are a vari ety of extended finite state machine where a shared memory is used to represent communications between the compo nents of systems. In this paper we introduce an extension of the Stream X-machines formalism in order to specify sys tems that present temporal requirements. We add time in two different ways. First, we consider that (output) actions take time to be performed. Second, our formalism allows to spec ify timeouts. Timeouts represent the time a system can wait for the environment to react without changing its internal tate. Since timeous affect the set of available actions of the system, a relation focusing on the functional behavior of sys tems, that is, the actions that they can perform, must explicitly take into account the possible timeouts. In this paper we also propose a formal testing methodology allowing to systemati cally test a system with respect to a specification. Finally, we introduce a test derivation algorithm. Given a specification, the derived test suite is sound and complete, that is, a system under test successfully passes the test suite if and only if this system conforms to the specification.