Sensitization of symbolic runs in real-time testing using the ORIS tool

We address the problem of test case selection and path sensitization in the process of testing real-time preemptive systems, following a formal methodology based on the theory of preemptive Time Petri Nets (pTPN) implemented in the Oris tool. We discuss practical factors that limit feasible behaviors in the implementation of a nondeterministic specification and we motivate the assumption of test cases defined as paths selected in the symbolic state space of a pTPN specification. Feasibility and effectiveness of the proposed sensitization technique are demonstrated through experimentation on a real-time operating system.