论文部分内容阅读
摘 要：现有的安全关键系统开发的方法一般是在系统开发后期使用测试的方法对系统需求进行验证，这种方法一方面需要耗费大量时间与人力，另一方面测试并不能保证系统中不存在错误。使用形式化的开发方法可以将软件需求添加到模型中，使用数学证明的方法来验证所要建立的系统是正确的，即在开发早期就能发现需求与系统设计间可能存在的问题，能够有效地减少后期发现错误所带来的损失。在现有需求工程方法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]。精化是Event-B区别于其它形式化方法的主要特征，即根据需求逐步向模型中添加细节使其完善。同时，早期模型中已经被证明的安全性属性在后续精化过程中可以得到保持。
然而，由于使用Event-B方法时需要从普通文本需求中获取形式化的需求规范，对开发人员的专业背景要求较高。针对这一问题，目前常用方法是使用需求工程方法对文本需求进行预处理，将复杂需求分解成若干子需求，并且以半形式化方式进行表达，然后将半形式化的需求规范转化到Event-B模型中，通过这种方式可以有效降低需求规范的获取难度。KAOS方法是一种经典的面向目标的需求工程方法，现有的研究是将KAOS方法中的目标模型（goalmodel）转换到Event-B组件中，如[3，4，6，10]。然而，这些方法都只是将目标模型中的功能性需求及安全属性转到Event-B中，由于目标模型中的目标（goal）同样表达了活性属性，使得现有的方法在转化过程中会出现活性属性丢失的问题[5，7，9]。本文在现有方法的基础上，给出了目标模型转化到Event-B模型的过程中保持其活性属性的方法。
结构如下：第2节介绍KAOS方法中的目标模型和Event-B的相关理论知识；第3节给出目标模型中目标的活性属性到Event-B模型的相关转化规则；第4节通过电梯实例介绍本文方法的有效性；第5节总结及未来工作的展望。
2 相关理论
2.1 KAOS方法
KAOS方法是一种面向目标建模和分析的需求工程方法[8]。KAOS方法包含5种模型用于描述需求文本，本文主要研究其中的核心模型，即目标模型（goalmodel）。在目标模型中，目标（goal）定义了系统为了实现对应需求应该完成的功能，可以分为实现目标（achievegoal）和维持目标（maintaingoal），分别表示功能性需求和安全性需求。实现目标是指预期系统最终将要实现的属性，形如：{If （Cur_Condition） then eventually （Tar_Condtion）}。维持目标则是指在某些条件下系统中定义的需要一直保持的属性，形如{If （CurrentCondition） then always not （BadCondition）}。
在目标模型中，上层的抽象目标可以分解精化为若干个子目标，子目标和上层抽象目标之间通过三种关系联系，分别为AND分解，OR分解，MileStone分解。 其中，AND分解表示当且仅当所有子目标实现时，上层抽象目标可以被满足；OR分解表示子目标中的一个实现时，上层抽象目标可以被满足；MileStone分解则表示子目标按照一定次序实现时，上层抽象目标可以被满足。
2.2 Event-B方法
为了验证模型中的属性是否满足需求规约，以及精化后的模型与上一层模型是否一致，Event-B在建模过程中需要对一些证明义务（proofobligations）进行证明。这些证明义务主要包括不变式保持（INV）、无死锁性（DLF）、胶合不变式。INV表示当前模型中的事件所引起的状态变迁应该满足不变式的要求，DLF要求模型中不存在死锁，胶合不变式则表示精化后模型中的事件与抽象模型应该保持一致。
3 目标中的活性属性到Event-B中的表达
在2.1节中，目标goal分为两种类型，分别为实现目标和维持目标，目前常用的转化方法中如[3，4，6，10]一般是直接将实现目标显式地转化到Event-B中的事件event中，即每一个目标对应于Event-B模型中的一个事件。然而，实现目标同时也通过eventually修饰符来表达在将来某个时间点目标状态最终会到达这样一种活性属性。现有的转化方法一般忽略了实现目标中的活性属性的表达，考虑到目标模型中的目标ag可以被分解为多个子目标如g1、g2，对应转化到Event-B模型中的事件evt1、evt2，存在这样的一组事件执行序列{evt1，evt1，…}，使得事件evt2无法得到执行，ag中的目标状态Tar_Condition无法达到。可以看到，在转化过程中，目标ag中的活性属性丢失。
在Event-B模型中，事件event表达状态变迁行为的同时，自身具有三种不同的属性{ordinary，convergent，anticipated}。Ordinary属性表示事件的执行次数不受约束，convergent属性表示事件的执行次数是收敛的，anticipated属性表示事件的执行次数不受约束，需要通过后续精化进行约束。
事件的收敛通过变式variant进行约束，变式是一组包含常数（x∈N）或有限集合（x∈P（α））的表達式。变式会随着convergent事件的执行递减，当变式的值为零或集合为空时，convergent事件在后续事件链中停止执行。
4 结束语
使用KAOS方法将文本需求进行分解建立目标模型，并且将需求改写转化到Event-B模型中对应元素，可以有效减少开发人员的工作量。目前现有的方法在转换过程中只考虑到需求中的安全性属性和功能性属性，对活性属性的转化有所缺失。本文在现有方法的基础上给出了将目标模型中目标的活性属性添加到Event-B模型的方法，并且结合电梯实例说明了该方法的有效性。
由于在Event-B的精化过程中，已经标记为convergent属性的事件可能会在精化过程中分解为若干子事件，导致之前保持的活性属性可能丢失，因此在之后的研究中将会关注Event-B精化过程中的活性属性保持研究。
参考文献
[1] ABRIAL J R.Modeling in event-b：system and software engineering[M].Cambridge University press，New York，2010.
[2] 黄志球，徐丙凤，阚双龙.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报，2014，25（2）：200—218.
[3] LALEAU R，SEMMAK F，MATOUSSI A，et al.A first attempt to combine SysML requirements diagrams and B[J].Innevations in Systems
关键字：安全关键系统；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]。精化是Event-B区别于其它形式化方法的主要特征，即根据需求逐步向模型中添加细节使其完善。同时，早期模型中已经被证明的安全性属性在后续精化过程中可以得到保持。
然而，由于使用Event-B方法时需要从普通文本需求中获取形式化的需求规范，对开发人员的专业背景要求较高。针对这一问题，目前常用方法是使用需求工程方法对文本需求进行预处理，将复杂需求分解成若干子需求，并且以半形式化方式进行表达，然后将半形式化的需求规范转化到Event-B模型中，通过这种方式可以有效降低需求规范的获取难度。KAOS方法是一种经典的面向目标的需求工程方法，现有的研究是将KAOS方法中的目标模型（goalmodel）转换到Event-B组件中，如[3，4，6，10]。然而，这些方法都只是将目标模型中的功能性需求及安全属性转到Event-B中，由于目标模型中的目标（goal）同样表达了活性属性，使得现有的方法在转化过程中会出现活性属性丢失的问题[5，7，9]。本文在现有方法的基础上，给出了目标模型转化到Event-B模型的过程中保持其活性属性的方法。
结构如下：第2节介绍KAOS方法中的目标模型和Event-B的相关理论知识；第3节给出目标模型中目标的活性属性到Event-B模型的相关转化规则；第4节通过电梯实例介绍本文方法的有效性；第5节总结及未来工作的展望。
2 相关理论
2.1 KAOS方法
KAOS方法是一种面向目标建模和分析的需求工程方法[8]。KAOS方法包含5种模型用于描述需求文本，本文主要研究其中的核心模型，即目标模型（goalmodel）。在目标模型中，目标（goal）定义了系统为了实现对应需求应该完成的功能，可以分为实现目标（achievegoal）和维持目标（maintaingoal），分别表示功能性需求和安全性需求。实现目标是指预期系统最终将要实现的属性，形如：{If （Cur_Condition） then eventually （Tar_Condtion）}。维持目标则是指在某些条件下系统中定义的需要一直保持的属性，形如{If （CurrentCondition） then always not （BadCondition）}。
在目标模型中，上层的抽象目标可以分解精化为若干个子目标，子目标和上层抽象目标之间通过三种关系联系，分别为AND分解，OR分解，MileStone分解。 其中，AND分解表示当且仅当所有子目标实现时，上层抽象目标可以被满足；OR分解表示子目标中的一个实现时，上层抽象目标可以被满足；MileStone分解则表示子目标按照一定次序实现时，上层抽象目标可以被满足。
2.2 Event-B方法
为了验证模型中的属性是否满足需求规约，以及精化后的模型与上一层模型是否一致，Event-B在建模过程中需要对一些证明义务（proofobligations）进行证明。这些证明义务主要包括不变式保持（INV）、无死锁性（DLF）、胶合不变式。INV表示当前模型中的事件所引起的状态变迁应该满足不变式的要求，DLF要求模型中不存在死锁，胶合不变式则表示精化后模型中的事件与抽象模型应该保持一致。
3 目标中的活性属性到Event-B中的表达
在2.1节中，目标goal分为两种类型，分别为实现目标和维持目标，目前常用的转化方法中如[3，4，6，10]一般是直接将实现目标显式地转化到Event-B中的事件event中，即每一个目标对应于Event-B模型中的一个事件。然而，实现目标同时也通过eventually修饰符来表达在将来某个时间点目标状态最终会到达这样一种活性属性。现有的转化方法一般忽略了实现目标中的活性属性的表达，考虑到目标模型中的目标ag可以被分解为多个子目标如g1、g2，对应转化到Event-B模型中的事件evt1、evt2，存在这样的一组事件执行序列{evt1，evt1，…}，使得事件evt2无法得到执行，ag中的目标状态Tar_Condition无法达到。可以看到，在转化过程中，目标ag中的活性属性丢失。
在Event-B模型中，事件event表达状态变迁行为的同时，自身具有三种不同的属性{ordinary，convergent，anticipated}。Ordinary属性表示事件的执行次数不受约束，convergent属性表示事件的执行次数是收敛的，anticipated属性表示事件的执行次数不受约束，需要通过后续精化进行约束。
事件的收敛通过变式variant进行约束，变式是一组包含常数（x∈N）或有限集合（x∈P（α））的表達式。变式会随着convergent事件的执行递减，当变式的值为零或集合为空时，convergent事件在后续事件链中停止执行。
4 结束语
使用KAOS方法将文本需求进行分解建立目标模型，并且将需求改写转化到Event-B模型中对应元素，可以有效减少开发人员的工作量。目前现有的方法在转换过程中只考虑到需求中的安全性属性和功能性属性，对活性属性的转化有所缺失。本文在现有方法的基础上给出了将目标模型中目标的活性属性添加到Event-B模型的方法，并且结合电梯实例说明了该方法的有效性。
由于在Event-B的精化过程中，已经标记为convergent属性的事件可能会在精化过程中分解为若干子事件，导致之前保持的活性属性可能丢失，因此在之后的研究中将会关注Event-B精化过程中的活性属性保持研究。
参考文献
[1] ABRIAL J R.Modeling in event-b：system and software engineering[M].Cambridge University press，New York，2010.
[2] 黄志球，徐丙凤，阚双龙.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报，2014，25（2）：200—218.
[3] LALEAU R，SEMMAK F，MATOUSSI A，et al.A first attempt to combine SysML requirements diagrams and B[J].Innevations in Systems