SPARDL模型Event—B解释.docVIP

SPARDL模型Event—B解释 　　摘 要：针对由周期行为和模式转换机制组成的实时系统提出的SPARDL需求建模语言，详细阐明了其对应的SPARDL模型的Event-B解释。通过Event-B来解释SPARDL的语义，同时提出一种基于SPARDL模型特征的精化框架用于Event-B模型的开发。最后，通过案例研究的分析展示用Event-B对SPARDL模型建模和验证的方法的有效性。 　　关键词：需求建模语言；周期性控制系统；Event-B；需求分析；精化；验证 　　中图分类号：TP311.521 　　文献标志码：A 　　Event-B interpretation for space aircraft description language model 　　QI Yan-xia1， SHEN Hui-li2*， CHEN Zhao-hui1， GU Bin1 　　1. Beijing Institute of Control Engineering， Beijing 100080，China； 　　2. School of Software Engineering， East China Normal University， Shanghai 200062，China 　　Abstract： 　　A requirement modeling language called SPARDL was proposed for modeling and analyzing such periodic control systems consisting of periodic behaviors together with the mode transition mechanism. The Event-B interpretation was specified for the SPARDL model. The semantics of SPARDL were presented by Event-B and a refinement framework was introduced to develop the Event-B models based on the features of the SPARDL model. Finally， a case study was analyzed to show the effectiveness of our proposed approach to modeling and validation of the SPARDL model by Event-B. 　　英文关键词　Key words： 　　requirement modeling language； periodic control system； Event-B； requirement analysis； refinement； verification 　　0 引言 　　在软件的生命周期内，从需求分析到软件维护的任何阶段，都可能存在漏洞。因此工程师们期望在软件运行中尽可能早地（最好是在需求分析阶段）检测到错误。面对这样的挑战，本文提出一种用需求建模语言SPARDL[1]用于为周期性控制系统建模。 　　SPARDL是一种用于控制系统的需求建模语言，尤其适用于基于模式的、有着混合的（连须的/离散的）状态、有限的周期行为和通信特征的控制系统。在每个周期中，系统都会并且只会精确地处在一个模式下，它可以停留在这个模式或者根据它现在的状态转换到另一个模式。作为一个轻量级的形式化语言，SPARDL可以在需求阶段消除不确定性，而这通常对于系统的正确性来说是一个挑战。传统的模型检测技术，如文献[2-5]均致力于验证系统间的交互而不是系统状态，而文献[6-9]中提到的SLAM、BLAST、CBMC和Gitto这些工具也因为解决的模型与SPARDL不兼容而无法使用它们对SPARDL进行验证。但是，作为一款优秀的定理证明工具，Event-B却能很好地处理SPARDL要解决的问题。 　　Event-B是一个重量级的形式化语言，它基于传统的谓词演算和定理证明。在Event-B中，事件（event）是一个主要的特征，因此它非常适合用来为周期行为建模。另外，Event-B还支持逐步精化地建立系统模型。用户可以在建模之初构建一个粗略的原型，然后不断地使用精化策略，使之成为一个更为复杂但实用的系统。在软件开发模型中，增量开发是运用于复杂系统开发的常见方式，能够极大地减少漏洞的出现。Event-B中的精化机制使得在形式化的建模和分析中进行增量开发变得方便。本文首先根据基本需求建立一个粗略的SPARDL的Event-B模型，然后再