形式化需求描述

航空电子领域中基于形式化方法的安全需求描述1.基于形式化方法的安全需求描述意义和准则在许多领域软件系统的安全性与可靠性显得日益重要，尤其在对安全性和可靠性要求极高的综合航空电子领域中软件系统的安全性和可靠性更显重要。因为综合航空电子系统对于整个飞机的安全性起着至关重要的作用。然而，伴随着航电系统日益增长的复杂性和系统集成的问题依然会增加潜在的错误并可能直接影响到飞机的安全性和可靠性。传统的软件工程方法已经很难满足这样复杂和安全性要求极高的需求，这迫切需要新的方法来设计开发安全性更高，资金时间投入更少的系统，为了解决这些实际问题，基于模型的开发方法（MBD）被引入，通过对需求描述严格的形式定义，可执行的原型设计，定理证明，模型检测，和高质量代码的自动生成等形式化技术大大提升了系统的安全性和可靠性，同时也大大节省了时间和成本。大多软件开发的错误源于需求分析阶段的逻辑错误。这些逻辑错误会传递到软件开发的后续阶段，大量的重复工作花费在修补由于需求阶段的逻辑错误而导致的系统错误。而且，需求错误往往是相当严重的错误。需求阶段的错误比设计或实现阶段所引入的错误更加影响系统的安全性。发现错误的一个有效途径就是创建一个系统外部可见行为的精确且可执行的系统模型。为了建立可读的且数学形式上的精确的系统功能行为模型，已经有多种符号语言被开发出来。比较出名的有SCR,RSML,SpecTRM,和Statechartso基于这些符号语言来创建模型能够发现大量系统描述中的错误。而且能够作为与用户交互的实模型，并能够类仿真的形式向客户执行。最好的情形就是经过精心设计的符号语言能够支持系统模型的自动形式化安全分析（如图1.1）。它使得通过一致性和完备性检查来发现错误成为可能，同时有能力来检查应用程序建模的一些性能描述。总之，创建系统行为的精确模型不仅仅使得能够在系统生命期尽早地发现错误，并及时地解决，还能够提升后续的系统设计，编码，验证，测试的质量。FormalModelPerformAnalysisFormalModelPerformAnalysis图1.1基于形式化方法的安全性分析系统需求描述作为系统开发的蓝图，它应该是对系统期望行为的完备的，一致性的，精确的描述。否则将会把不安全因素带进后续的设计、编码、测试等环节，将严重影响系统的安全性能同时也增加更多的开发代价。所以提供方法和技术使尽可能早地排除与需求相关的错误显得非常重要。为了分析和发现需求描述的错误，描述语言所应具有的一些标准对于我们达到我们的目标至关重要。准则一是需求描述语言只详细描述系统的黑盒行为而不包括内部的设计信息；准则二是描述语言要让在保证形式化的准确性的同时能够方便专业技术人员和非专业人员易读易理解建立起他们对系统统一的认识；准则三，就是要具有描述复杂系统的能力，在这里主要借鉴了Harel所提出的“clustering“的概念，另一方面也用到了Harel“abstraction”思想；其他两个标准是最小性和简洁性。最小性就是需求描述仅包含对开发和分析有用的信息。这样能够节省更多的时间，同时让读者聚焦于对象的重点上。简洁性就是尽量避免描述语言让描述和分析过程复杂化。语言应该简单易于使用而且能让描述更可读和更易查错。2.RSML为了更好地描述需求，满足上面所提到的符号语言的要求，在这里我们引入了RSML语言，RSML(需求状态机语言)是源于DavidHarel的Statecharts，是加州大学的NancyLeveson研究组开发的一种基于状态的描述语言用于对过程控制系统的行为建模。RSML的主要设计目标就是让非计算机专业人员比如最终用户，应用工程师，管理者，以及来自监管机构的代表都能易读易理解用RSML语言写的需求描述。一个RSML描述由变量，状态，转移，功能函数，宏，常量，和接口组成。需求描述中的变量用于存储外部传感器的输入值，也用于暂存系统的输出值。Statecharts以分层的形式组织状态。RSML包括三种不同类型的状态：复合状态，平行状态，和原子状态。原子状态等同于传统有限状态机中的状态。平行状态用于模型固有的平行性或建模对象的局部。复合状态(superState)一方面用于隐藏状态机的局部细节来使得所得模型更易理解，另一方面封装状态机的确切行为。图2.1是ASW需求描述中状态的分层建模的例子，它包含以上所说的三种不同状态类型。aswRe<iModel图2.1High-levelASWModelRSML中的状态转移控制着一个状态到其他状态的转移。状态转移由一个原状态，一个目的状态，一个触发事件，一个监督条件和一组动作事件组成。为了执行一次RSML状态转移，必须有下列情况为真：(1)原状态当前处于激活状态，(2)触发事件出现在原状态处于激活态，(3)当触发事件发生时监督条件必须为真。当所有这些情况都满足时，目的状态将成为激活状态，而原状态将变为非激活状态，同时产生行为事件。监督条件简单地以说就是在不同的状态和变量之间的一种谓词逻辑表达式，用命题逻辑符号语言传统地去定义这些条件通常会陷入复杂的表达式并且变得不可读。为了克服这一问题，在RSML中使用了析取范式(DNF)的一种表格表示，这种表格被称为AND/OR表。AND/OR表格的最左一列列出了逻辑短语。其它的列是这些逻辑短语的连接，并且列出了表达式的逻辑真值。并规定只要有某一列的值为真则整个表的值就为真。而每列的真值为真当且仅当此列的真值与它们所关联的逻辑短语的真值都一致。AND/OR表2.1是谓词短语((Expression-1AnExpression-2)V(Expression-1八Expression-3))的逻辑等价描述。OR为了进一步增加需求描述的可读性，Irvine研究组在RSML中引进了许多其它的语法结构，例如，允许谓词中的表达式定义为形如case语句的函数，允许宏定义经常使用的且相同的条件。图2.2，“BelowThreshold”和“AltitudeQualityOK”都是宏。宏BelowThreshold的定义在图2.3中给出。Transition(S)：Transition(S)：Above一->BelowLocation:AltitudeStatusMacro:BelowThresholdDefinition:AltitudegAltitudeThreshold||T|NBelowThreshold。TDAltitudcQualityOK()TTriggerEvent:AltReceivedEventCondition:OutputAction:AltStatusEvaluatedEvent图2.2ATransitionandMacrofromtheASWrequirementsRSML支持系统级组件间通信的严格的描述和分析，系统组件间的的联系通过通道的形式。每个组件可能有多个输入/输出通道。通信的发生通过消息机制来驱动。3.RSML用于需求形式化描述的好处RSML语言易读易理解，能够使设计人员和各户之间对于需求描述的理解更一致。能够让各户更多地参与到系统开发中来，从而使开发的产品更加地符和期望。RSML形式化地描述系统的行为模型，能够方便地翻译为定理自动证明和模型检测的输入形式使模