Algebraic Specification Approach to Model-Checking with Constraints

模型检查是一种很有前途的软件设计自动验证方法，它通过穷尽搜索有限状态空间来检查给定的LTL公式是否满足。待探索的状态数量变大，当某个数据变量对控制流产生影响时，就会产生状态空间爆炸问题。我们将数据约束的思想与模型检验相结合，提出了一种新的方法来避免这一问题。在该方法中，不扩展单个数据值，而是将数据变量的条件符号表示为数据约束。由于该方法处理的是符号表示，因此可以避免状态空间爆炸问题。我们使用代数规范语言Maude作为底层基础设施，因为代数技术已经被称为提供以统一方式定义复杂数据的系统机制。我们的结果可以总结如下。约束自动机被定义为mealy风格自动机的扩展，以集成数据约束的概念，然后在Maude.2上实现。约束自动机可以很好地表示和分析这三个实例；区间约束、分布式排序和饭店键问题。通过使用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.