Gömülü TV yazılımı modelinin kontrolünde ortaya çıkan durum patlaması problemine çözüm yaklaşımı

Digital technology is developing rapidly. Thus the demand of new features for the TVs is increasing speedily. Besides, this increasing demand causes stronger competition. As a result of strong competition and increasing demand for the new features, embedded TV software of current TV sets is getting more complicated. Therefore, the test and verification process of the embedded TV software is getting harder. Logic of model checking is to algorithmically check if a model satisfies a specification. A model generally expressed as a directed graph including vertices and edges. The vertices specify the states of the model and the edges specify the state transitions due to a given condition. It is a widely accepted practice to use model checking in verification of embedded systems. On the other hand, it is seriously affected by the exponential increase in the number of states during the verification process. Modelling a fully non-deterministic TV-user is the one of the main reason for the exponential increase in the number of states. For the purpose of shrinking the state space being observed during the model checking process of TV, three methods are proposed in this thesis. TV logs are used to generate partly non-deterministic TV-user (user agent) models for all three methods that are proposed. The TV logs includes the Remote Controller (RC) keystroke histories recorded during the manual testing of the TV. The first method is "Direct Log Based Specification". In this method, the user agent is designed directly from the TV log. The number of states are decreased in this method whereas the user agent model became fully deterministic. The second method is "Injecting non-determinism to Log Based Specifications". In this methodthe first method is improved and a more non-determinictic user agent is produced according to the given TV log. The Third method is "Combining Log Based Specifications". In this method we used two different TV logs to construct a more non-deterministic user-agent. Our results show that by using partly non-deterministic user agents we can significantly decrease the verification time of certain safety and liveness properties.