Algebraic Specification Approach to Model-Checking with Constraints

点击翻译按钮获取中文摘要

Model-checking is a promising approach to the automatic verification of software design It searches exhaustively a finite-state space to check if a given LTL formula is satisfied. The number of states to be explored becomes large, resulting in a state-space explosion problem, when a certain data variable makes effects on the control flow. We focus on a new method for avoiding the problem by integrating the idea of data constraints with the model-checking. In the proposed method, individual data values are not expanded, but the condition on the data variable is represented symbolically as a data constraint. Since the method deals with the symbolic representation, the state-space explosion problem can be avoided. We employ the algebraic specification language Maude as the underlying infrastructure because the algebraic techniques have been known as providing systematic mechanism to define complex data in a uniform manner. Our results can be summarized as below.1. Constraint automaton is defined as an extension of Mealy-style automaton to integrate the notion of data constraints, which is then implemented on Maude.2. Constraint automaton can successfully represent and analyze the three example cases ; interval constraints, distributed sorting, and Hotel key problem.3. Constraint automaton can be extended to include timing issues, by using RT-Maude as its underlying infrastructure. We have set up next research agenda to apply the constraint automaton to the analysis of behavioral aspects of Event-B descriptions.