Attacking state space explosion problem in model checking embedded TV software

Abstract

The features of current TV sets is increasing rapidly resulting in more complicated embedded TV software that is also harder to test and verify. Using model checking in verification of embedded software is a widely accepted practice even though it is seriously affected by the exponential increase in the number of states being produced during the verification process. Using fully non-deterministic user agent models is one of the reasons that can result in a drastic increase in the number of states being produced. In order to shrink the state space being observed during the model checking process of TV software, a method is proposed that rely on using previous test logs to generate partly nondeterministic user agent model. Results show that by using partly non-deterministic user agents, the verification time of certain safety and liveness properties can be significantly decreased.