张棋 谢健 尹小花

摘 要：现有的安全关键系统开发的方法一般是在系统开发后期使用测试的方法对系统需求进行验证，这种方法一方面需要耗费大量时间与人力，另一方面测试并不能保证系统中不存在错误。使用形式化的开发方法可以将软件需求添加到模型中，使用数学证明的方法来验证所要建立的系统是正确的，即在开发早期就能发现需求与系统设计间可能存在的问题，能够有效地减少后期发现错误所带来的损失。在现有需求工程方法KAOS方法转化到Event-B模型的方法基础上，对其中活性属性丢失问题进行研究，并给出了解决方法。

关键字：安全关键系统；KAOS；Event-B；活性；模型检测

中图法分类号：TP311 文献标识码：A

Abstract： The traditional verification method of safety-critical system usually happened in the late stage of system development.On one hand，test stage requires a lot of time and effort，moreover，traditional test technique does not guarantee that there is no error in the system.On the other hand，formal development methods use mathematic language to describe requirements，and then use various model checking methods to prove that the model which contains properties of requirements is correct.So we can find design error in early development stage，and this can reduce the losses caused by late errors.In this paper，we discuss the deletion of liveness property in several translation method from goal-oriented method to Event-B method，then we give a solution.

Keywords：safety-critical system；KAOS；Event-B；liveness；model checking

1 引 言

安全关键系统是指系统运行错误会导致一系列危及生命财产安全等后果的计算机系统。常见的安全关键系统如车载自动驾驶系统、医疗系统、航空控制系统等，這些系统在运行过程中一旦发生错误，造成的潜在危害往往是难以预估的[2]。因此，如何确保安全关键系统在运行过程中正确行使其功能是目前软件工程领域中研究的一个热点。

在软件工程领域中，形式化方法通过使用严格数学语言对需求进行描述和建模，并且使用证明的方法验证需求和软件模型之间的一致性和正确性。对于安全关键系统开发，使用形式化的语言来描述文本需求有助于消除自然语言的二义性，提高需求规范的准确性。Event-B是一种基于一阶逻辑和集合论的用于对需求进行规约验证的形式化建模方法[1]。……