Attacking State Space Explosion Problem in Model Checking Embedded TV Software

Comert F., Ovatman T.

IEEE TRANSACTIONS ON CONSUMER ELECTRONICS, cilt.61, sa.4, ss.572-580, 2015 (SCI-Expanded) identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 61 Sayı: 4
  • Basım Tarihi: 2015
  • Dergi Adı: IEEE TRANSACTIONS ON CONSUMER ELECTRONICS
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus
  • Sayfa Sayıları: ss.572-580
  • Anahtar Kelimeler: Model Checking, State Space Explosion, TV Software Verification, TV Software Modeling
  • İstanbul Teknik Üniversitesi Adresli: Evet

Özet

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).