下载文档原格式
需求描述语言
需求描述语言（Requirement Description Language，简称RDL）是一种用于描述和表达软件需求的语言。
它通常用于在软件开发过程中，将用户需求、业务需求、功能需求等非技术性的需求转化为技术人员可以理解和实现的技术性描述。
需求描述语言应该具备以下特点：
1．明确性：能够清晰、准确地描述需求，避免歧义和误解。
2．结构性：能够支持层次化的需求描述，包括总需求、子需求、细节需求等。
3．可追溯性：能够建立需求与代码、测试用例等开发产物之间的关联，方便后续的变更管理和维护。
4．易读性：语言应该简洁明了，易于理解，方便非技术人员阅读和理解。
常见的需求描述语言包括自然语言、结构化语言、形式化语言等。
其中，自然语言是最常用的需求描述语言，但由于其存在歧义、模糊等问题，通常需要结合其他工具和方法进行补充和澄清。
结构化语言和形式化语言则更加严谨和规范，适合用于对需求进行精确的描述和验证。
软件工程形式化方法 z 语言软件工程是一个复杂而庞大的领域，要确保软件系统的正确性和可靠性，需要采用各种形式化方法。
形式化方法是一种严格、精确的描述和分析系统的方法，其中最著名的是Z语言。
1. 什么是形式化方法形式化方法是一种使用数学符号和形式化规范来描述和分析软件系统的方法。
它能够捕捉系统的各个方面，从而确保系统的正确性和可靠性。
形式化方法可以消除歧义和模糊性，提供严格的语法和语义定义，并进行可靠的推理和验证。
2. Z语言的引入和发展Z语言是一种基于数学集合论和一阶谓词逻辑的形式化规范语言。
它于20世纪70年代由牛津大学的J.R.阿兰·特拉弗斯和J.B.斯托拉兹提出，并继续在软件工程领域的学术界和实践中得到广泛应用。
3. Z语言的特点和优势- 精确性：Z语言使用严格的数学符号和形式化规范，可以精确地描述系统的各个方面，避免了自然语言的歧义和模糊性。
- 可读性：尽管Z语言使用了数学符号，但其符号系统和语法规则都经过严格定义，使得Z规范可以被可靠地解释和理解。
- 可验证性：Z语言规范的严格性使得系统的正确性验证变得可行。
通过形式化推理和模型检测等技术，可以对规范进行自动验证和分析。
- 模块化：Z语言支持模块化规范，可以将系统的不同部分进行独立的规范和验证，从而提高开发过程的灵活性和可重用性。
4. Z语言在软件工程中的应用- 需求分析和规约：Z语言可以用于对软件系统的需求进行精确描述和形式化规约，从而帮助开发人员和用户准确理解和交流需求。
- 设计规约和验证：Z语言可以用于对软件系统的设计进行精确描述和形式化规约，并进行验证和验证。
通过验证，可以发现设计冲突和错误，提高系统的可靠性。
- 系统建模和仿真：Z语言可以用于对软件系统进行形式化的建模和仿真。
通过建立形式化模型，可以进行系统行为的精确分析和评估，从而帮助设计和优化系统。
- 代码生成和自动化工具支持：Z语言可以作为设计工具中的一部分，与代码生成和其他自动化工具集成，从而提高开发效率和系统质量。
航空电子领域中基于形式化方法的安全需求描述
1. 基于形式化方法的安全需求描述意义和准则
在许多领域软件系统的安全性与可靠性显得日益重要，尤其在对安全性和可靠性要求极高的综合航空电子领域中软件系统的安全性和可靠性更显重要。
因为综合航空电子系统对于整个飞机的安全性起着至关重要的作用。
然而，伴随着航电系统日益增长的复杂性和系统集成的问题依然会增加潜在的错误并可能直接影响到飞机的安全性和可靠性。
传统的软件工程方法已经很难满足这样复杂和安全性要求极高的需求，这迫切需要新的方法来设计开发安全性更高，资金时间投入更少的系统,为了解决这些实际问题，基于模型的开发方法（MBD）被引入，通过对需求描述严格的形式定义，可执行的原型设计，定理证明，模型检测，和高质量代码的自动生成等形式化技术大大提升了系统的安全性和可靠性，同时也大大节省了时间和成本。
大多软件开发的错误源于需求分析阶段的逻辑错误。
这些逻辑错误会传递到软件开发的后续阶段，大量的重复工作花费在修补由于需求阶段的逻辑错误而导致的系统错误。
而且，需求错误往往是相当严重的错误。
需求阶段的错误比设计或实现阶段所引入的错误更加影响系统的安全性。
发现错误的一个有效途径就是创建一个系统外部可见行为的精确且可执行的系统模型。
为了建立可读的且数学形式上的精确的系统功能行为模型，已经有多种符号语言被开发出来。
比较出名的有SCR,RSML,SpecTRM,和Statecharts。
基于这些符号语言来创建模型能够发现大量系统描述中的错误。
而且能够作为与用户交互的实模型，并能够类仿真的形式向客户执行。
最好的情形就是经过精心设计的符号语言能够支持系统模型的自动形式化安全分析（如图1.1）。
它使得通过一致性和完备性检查来发现错误成为可能，同时有能力来检查应用程序建模的一些性能描述。
总之，创建系统行为的精确模型不仅仅使得能够在系统生命期尽早地发现错误，并及时地解决，还能够提升后续的系统设计，编码，验证，测试的质量。
图1.1 基于形式化方法的安全性分析
系统需求描述作为系统开发的蓝图，它应该是对系统期望行为的完备的，一致性的，精确的描述。
否则将会把不安全因素带进后续的设计、编码、测试等环节，将严重影响系统的安全性能同时也增加更多的开发代价。
所以提供方法和技术使尽可能早地排除与需求相关的错误显得非常重要。
为了分析和发现需求描述的错误，描述语言所应具有的一些标准对于我们达到我们的目标至关重要。
准则一是需求描述语言只详细描述系统的黑盒行为而不包括内部的设计信息；准则二是描述语言要让在保证形式化的准确性的同时能够方便专业技术人员和非专业人员易读易理解建立起他们对系统统一的认识；准则三，就是要具有描述复杂系统的能力，在这里主要借鉴了Harel 所提出的“clustering“的概念，另一方面也用到了Harel“abstraction”思想；其他两个标准是最小性和简洁性。
最小性就是需求描述仅包含对开发和分析有用的信息。
这样能够节省更多的时间，同时让读者聚焦于对象的重点上。
简洁性就是尽量避免描述语言让描述和分析过程复杂化。
语言应该简单易于使用而且能让描述更可读和更易查错。
2.RSML
为了更好地描述需求，满足上面所提到的符号语言的要求，在这里我们引入了RSML语言，RSML（需求状态机语言）是源于David Harel的Statecharts，是加州大学的Nancy Leveson研究组开发的一种基于状态的描述语言用于对过程控制系统的行为建模。
RSML的主要设计目标就是让非计算机专业人员比如最终用户，应用工程师，管理者，以及来自监管机构的代表都能易读易理解用RSML 语言写的需求描述。
一个RSML描述由变量，状态，转移，功能函数，宏，常量，和接口组成。
需求描述中的变量用于存储外部传感器的输入值，也用于暂存系统的输出值。
Statecharts以分层的形式组织状态。
RSML包括三种不同类型的状态：复合状态，平行状态，和原子状态。
原子状态等同于传统有限状态机中的状态。
平行状态用于模型固有的平行性或建模对象的局部。
复合状态（superState）一方面用于隐藏状态机的局部细节来使得所得模型更易理解，另一方面封装状态机的确切行为。
图2.1是ASW需求描述中状态的分层建模的例子，它包含以上所说的三种不同状态类型。
图2.1 High-level ASW Model
RSML中的状态转移控制着一个状态到其他状态的转移。
状态转移由一个原状态，一个目的状态，一个触发事件，一个监督条件和一组动作事件组成。
为了执行一次RSML状态转移，必须有下列情况为真：(1)原状态当前处于激活状态，(2)触发事件出现在原状态处于激活态，(3)当触发事件发生时监督条件必须为真。
当所有这些情况都满足时，目的状态将成为激活状态，而原状态将变为非激活状态，同时产生行为事件。
监督条件简单地以说就是在不同的状态和变量之间的一种谓词逻辑表达式，用命题逻辑符号语言传统地去定义这些条件通常会陷入复杂的表达式并且变得不可读。
为了克服这一问题，在RSML中使用了析取范式(DNF)的一种表格表示，这种表格被称为AND/OR表。
AND/OR表格的最左一列列出了逻辑短语。
其它的列是这些逻辑短语的连接，并且列出了表达式的逻辑真值。
并规定只要有某一列的值为真则整个表的值就为真。
而每列的真值为真当且仅当此列的真值与它们所关联的逻辑短语的真值都一致。
AND/OR表2.1是谓词短语
（(Expression-1∧┐Expression-2)∨(Expression-1∧Expression-3)）的逻辑等价描述。
AND/OR表2.1
为了进一步增加需求描述的可读性，Irvine研究组在RSML中引进了许多其它的语法结构，例如，允许谓词中的表达式定义为形如case语句的函数，允许宏定义经常使用的且相同的条件。
图2.2，“BelowThreshold”和“AltitudeQualityOK”都是宏。
宏BelowThreshold的定义在图2.3中给出。
图2.2 A Transition and Macro from the ASW requirements RSML支持系统级组件间通信的严格的描述和分析，系统组件间的的联系通过通道的形式。
每个组件可能有多个输入/输出通道。
通信的发生通过消息机制来驱动。
3.RSML用于需求形式化描述的好处
一．RSML语言易读易理解，能够使设计人员和各户之间对于需求描述的理解更一致。
能够让各户更多地参与到系统开发中来，从而使开发的产品更加地符和期望。
二．RSML形式化地描述系统的行为模型，能够方便地翻译为定理自动证明和模型检测的输入形式使模型可执行，通过模型检测和定理自动证明来保证系统行为的完备性和一致性，从而提升系统的安全性。
三．精确的行为描述，可以减少系统的冗余，节省时间。
四．提供了一系列针对复杂系统的语法机制，适用于描述复杂性的系统。
五．基于这种需求描述的需求形式化分析方法，可以使得大量错误在需求阶
段被找出，避免了错误的向后传递，大大减少后续排错，返工的时间消耗。
