Algebraic Specification Approach to Model-Checking with Constraints

模型检测是一种很有前途的软件设计自动验证方法，它在有限状态空间中进行穷举搜索，以检测给定的LTL公式是否满足。当某个数据变量对控制流产生影响时，要探索的状态的数量变得很大，从而导致状态空间爆炸问题。我们专注于一个新的方法，以避免这个问题的数据约束的想法与模型检测相结合。在所提出的方法中，单个数据值不被扩展，但数据变量的条件被象征性地表示为数据约束。由于该方法采用符号表示，避免了状态空间爆炸问题。我们采用代数规范语言Maude作为底层基础设施，因为代数技术已被称为提供系统的机制，以统一的方式定义复杂的数据。我们的研究结果可以总结如下.将约束自动机定义为Mealy-style自动机的扩展，集成了数据约束的概念，并在Maude上实现.约束自动机可以成功地表示和分析三个例子的情况下，区间约束，分布式排序，酒店的关键问题.通过使用RT-Maude作为其底层基础设施，约束自动机可以扩展到包括时序问题。我们已经建立了下一个研究议程，将约束自动机应用于事件B描述的行为方面的分析。

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.