Automatic Analysis of Requirements Model with Algebraic Specification Techniques

据说，即使是对客户端的误用也是开发人员应该负责的，因此，指定系统提供哪些特性的任务就成了一个主要问题。根据软件工程，这样的问题是通过检查在开发的早期阶段构建的严格的需求模型来解决的。在这个研究项目中，我们研究了一种用Event-B编写的需求模型自动分析的新方法。该方法利用抽象技术，为现有方法提供了一种新的正确性标准。

Since it is said that even misusage of clients is what developers should be responsible for, the task of specifying what features the system provides becomes a major issue. According to Software Engineering, such a problem is to be resolved by checking of rigorous requirements models constructed at early stages of the development. In this research project, we investigated a new method of automated analysis of requirements models written in Event-B. The proposed method makes use of abstraction techniques, and provides a new correctness criteria complementary to existing methods,