Attacking State Space Explosion Problem in Model Checking Embedded TV Software

Comert F., Ovatman T.

IEEE TRANSACTIONS ON CONSUMER ELECTRONICS, vol.61, no.4, pp.572-580, 2015 (SCI-Expanded) identifier

  • Publication Type: Article / Article
  • Volume: 61 Issue: 4
  • Publication Date: 2015
  • Journal Name: IEEE TRANSACTIONS ON CONSUMER ELECTRONICS
  • Journal Indexes: Science Citation Index Expanded (SCI-EXPANDED), Scopus
  • Page Numbers: pp.572-580
  • Keywords: Model Checking, State Space Explosion, TV Software Verification, TV Software Modeling
  • Istanbul Technical University Affiliated: Yes

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 non-deterministic 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(1).