ESpin: Analyzing Event-Driven Systems in Model Checking

Abstract

Multiple occurrences of the events make the behaviors of an event-driven system usually less logical and explicit. Thus, an event-driven system is hard to be analyzed and found errors. In this paper, we introduce an approach to analyze event-driven systems following the properties related to the occurrence of the events. Our method is based on the exploration of the states of the system using model checking techniques. To that end, we introduced a domain-specific language (DSL) to easily describe the behaviors of the system. The specification of the system in the DSL is then translated into the model of the system to explore the states of the system. The property to be checked is used to realize the model checking algorithm that is used to label the graph realized from the state space. The experiment results show that we can facilitate the specification of the system and analyze the behaviors of the system correctly.