基于Event-B的EBRE需求模型的正确性验证

作     者：冯世玲 

作者单位：华东师范大学 

学位级别：硕士

导师姓名：李钦

授予年度：2022年

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：Event-B 需求工程 需求模型 需求验证 Rodin 

摘      要：需求分析在软件工程中处于非常重要的地位,为设计起指导作用,是软件工程中的一个关键过程,需求分析的正确性直接关系到所开发系统的效率和质量。目前需求工程也已经研究出一系列需求分析的方法,金芝等提出的基于环境建模的需求工程方法（EBRE）被广泛应用,该方法显式地对交互环境进行建模,并基于环境模型为需求获取和分析提供系统的过程和需求模型。如何验证EBRE需求模型的正确性是备受关注的问题之一,目前存在相应工具以环境本体为标准验证EBRE模型的完整性等,但对于需求模型自身的正确性仍缺少形式化证明手段,导致需求模型的正确性在数学逻辑证明层面无法得到保障。Event-B作为一种典型的形式化方法,其基于集合论和一阶逻辑,以精化的方式进行形式化建模与验证,并根据系统需求验证其正确性,可以作为EBRE需求模型正确性验证的一种途径。我们将EBRE方法和Event-B的方法结合起来,提出基于Event-B的EBRE需求模型的正确性验证方法。将EBRE模型转换为Event-B的初始模型,转换过来的Event-B模型可以为需求模型的正确性提供形式化证明。在此基础上,我们实现了EBRE模型到Event-B模型的自动化转换工具,并以Rodin插件的形式发布,从而实现EBRE需求模型的正确性的自动化验证。本文的主要工作如下:***需求模型到Event-B模型的转换:通过分析EBRE模型元素与Event-B模型元素之间的对应关系,定义了一套转换规则,将EBRE需求模型转换为Event-B模型,确保EBRE需求模型与转换后的Event-B模型具有语义上的一致性。***需求模型的正确性验证:转换后的Event-B模型会生成相应的证明义务,基于Rodin平台的定理证明机制,进行证明义务的自动证明或手动交互式证明,从而验证需求模型的正确性。通过分析证明义务与EBRE需求模型中所要满足的性质的一一对应关系,将Event-B的验证机制应用于EBRE模型的正确性验证,验证需求的正确性。3.基于Rodin平台的模型自动化转换插件:基于EBRE需求模型到Event-B模型的转换以及EBRE需求模型的正确性验证的方法,实现EBRE需求模型元素到Event-B模型元素的自动化转换工具,为EBRE需求模型的正确性验证提供技术支撑。