A Quantitative Approach to Input Generation in Real-Time Testing of Stochastic Systems

The testing process, an implementation is exercised under controlled conditions with the intent of observing deviations with respect to the expected behavior. The development of reactive and real-time systems, this often relies on the execution of test-suites derived from abstractions that focus on finite-state and timed behavior, with the aim of revealing defects related to concurrency, communication, and timeliness. A rich survey on timed and untimed model-based approaches to testing can be found in, focusing on the problems of test-suites generation and execution. a model-based theory for conformance testing of Labeled Transition Systems (LTS) and Input/Output Transition Systems (IOTS) is presented; The theory defines the input-output conformance (ioco) implementation relation, which in turn allows the definition of test suite generation algorithms. In a more applicative perspective, Muccini et al. derive test-suites as coverage of a bisimulation reduction of the LTS modeling system dynamics. Coverage of an untimed and deterministic Finite State Machine (FSM) is also addressed in the partial- WpMethod, where state-verification and full fault-coverage are achieved under the assumption of an upper bound on the number of states in the implementation. Timed Input Output Automaton (TIOA). A comprehensive framework based on FSMs is presented for the generation of tests on systems whose temporal parameters may also include time intervals or random variables. Test cases are selected as deterministically timed event sequences of a deterministic and output-urgent Timed Automaton, either as witnesses of real-time logic expressions capturing specific testing purposes or as elements of a test-suite covering locations of the specification automaton. this problem is faced on the basis of a specification model represented as a Stochastic Input Output Automaton (STIOA), where input actions are events that can be forced to occur at any desired time, and output actions are noncontrollable events with uniform distribution over finite intervals; under these assumptions, for each selected timing of input actions the probability of conclusive execution of a symbolic run is proven to be proportional to the volume of a multivariate Difference Bounds Matrix (DBM) domain collecting the timings that make the run feasible.