轨道交通控制软件中基于场景的需求分析方法

闫倩倩，缪炜恺

（华东师范大学上海市高可信计算重点实验室，上海 200062）

0 概述

对于轨道交通系统、航空航天控制系统、核电控制系统等安全控制系统，其嵌入式控制软件是否能正确执行预期功能会影响到人身安全。因此，如何确保嵌入式控制软件的正确性成为研究人员的关注热点［1-3］。众所周知，形式化的需求规约可有效提高软件的质量，精确描述软件功能，并通过形式化建模执行严格的需求确认和验证，为后续的开发提供便利。

然而，如何把形式化方法应用到真实的工业软件中依然是一大挑战［4］。首先，目前缺乏建立形式化规约的方法。一方面，由于软件需求大多使用自然语言撰写而自然语言描述具有不准确性，软件工程师在构建需求规约时未必能准确且精确地描述系统功能；另一方面，领域专家几乎不可能使用复杂的形式化表示法描述系统需求，多数领域专家缺少坚实的离散数学基础，并且学习复杂的数学符号和证明技巧既费时又费力。其次，形式化的需求确认和验证大多由软件工程师主导，缺乏领域专家视角。传统的形式化验证侧重于使用形式化证明方法发现软件中的逻辑错误，如不一致性，但这对领域专家来说是难以理解的。

在形式化方法的需求建模阶段，根据不同的建模需求，大致有基于统一建模语言的方法UML［5］、基于属性描述语言的方法PSL［6］、基于规约描述语言的方法SDL［7］、基于逻辑的方法Z［8］和Event-B［9-10］、基于进程代数的方法CCS［11］和CSP［12］等。而在需求分析阶段，需求审查因其易推广、实施容易的特点，广泛应用于需求确认过程中。研究人员提出了一系列需求审查方法，如基于查询模型的提问式审查方法［13］、以认知模型为基础的审查方法［14］、以虚拟原型为基础的审查方法［15］等。规约测试技术也是一种经常应用于需求确认的方法。VDMTools 工具［16］执行用VDM 语言写成的规约显示系统动作供测试人员确认。同时，ProB 为B 语言需求规约提供一种确认手段［17］。模型检查也是一种常用的形式化分析方法，如：基于特定语言的建模方法DSL［18-19］；一种用EAST-ADL 描述的架构模型分析技术［20］，包括EAST-ADL 的模拟执行；基于组件的BIP 模型被用来进行软件建模和验证［21］，用于对无界时间属性的马尔可夫链进行统计模型检查的算法［22］等。在工业上的应用方面，StateChart 广泛应用于工业软件建模和分析［23］，Matlab/Simulink 提供了Stateflow［24］。然而这些方法都没有为大型工业项目提供一个系统的需求建模方法。

场景是一种用于分析软件的重要途径，且符合领域专家的思维方式。在基于场景的设计分析方面，基于模型驱动的方式被广泛使用。基于场景的CBTC（Communication Based Train Control）系统建模［25］方法，通过场景模型和需求间的追溯关系，指导如何撰写场景的方法［26］，用一阶线性逻辑验证需求场景的正确性等方法［27］。目前，研究人员大都关注软件代码功能，生成测试用例，给出优化方法［28-29］。然而这些方法都没有提供一个基于物理场景的需求确认和验证方法。

本文针对面向轨道交通领域的嵌入式控制软件，提出一种以领域专家为中心的基于场景的需求分析方法。使用三步演化式建模方法建立形式化的需求规约，避免复杂的数学运算，并导出需求模型。在此基础上，领域专家根据规则撰写场景分析场景执行结果验证需求规约是否正确地描述了期望的场景。为验证需求的正确性，提高需求确认和验证的效率，分别从特殊变量场景、效率、场景质量这3 个方面对场景进行优化。

1 方法框架

如图1 所示，本文方法主要包括演化式需求建模和需求的确认和验证2 个部分。首先，通过和领域专家的大量交流，从嵌入式控制软件中提取特定领域的特征，并根据这些周期性、模式转化等特征，建立需求规约模板，领域专家可以根据模板的指导使用自然语言构建非形式化规约，软件工程师和领域专家都可以快速地理解非形式化需求；然后，在非形式化需求被确认后，非形式化需求被转化为半形式化需求，所有的数据结构都被形式化的定义，在这个阶段，系统结构仍然可以被方便的修改重塑；最后，当半形式化规约确认后，用户需求被最终转化为形式化地需求规约，此时，所有的变量、功能都被形式化地定义。

图1 本文方法框架Fig.1 Framework of the proposed method

需求形式化规约构建完成后，接下来验证需求正确性，需求规约首先被转化为形式化需求模型。在嵌入式控制软件领域，传统的基于场景的测试方法是把场景放到仿真平台上执行，然而对大规模的嵌入式软件来说，为了验证其中一个子系统的需求正确性，仿真执行时需要配置大量初始信息，费时费力。设想，如果场景能直接在需求模型中执行，则可以节约大量时间资源。为此，本文规定场景描述规则，即在场景中加入相关需求变量的取值，从而在执行需求模型时可以快速从这样的场景中得到需要的测试数据。因此，在本文中，领域专家首先需要根据规定的场景描述规则撰写场景，然后在需求模型中执行该场景，验证需求规约是否正确地描述了期望的场景。

在嵌入式控制软件领域，存在一些特殊变量，如状态变量，对于这类变量来说，普通的场景可能不足以验证它们的性质。此外，由于场景由领域专家手动撰写，导致效率较低，并且手动撰写的场景无法保证场景的质量，如果需求覆盖率较低，则说明场景质量不高，造成分析质量低下。为了解决这些问题，本文从特殊变量场景、效率、场景质量这3 个方面对场景进行优化。

轨道交通控制系统由车载设备和地面设备组成，车载设备和地面设备相互协作保证列车的安全运行。其中车载设备包括列车自动防护（Automatic Train Protection，ATP）系统、列车自动运行（Automatic Train Operation，ATO）系统、列车自动检测（Automatic Train Supervision，ATS）系统3 个部分。ATP系统是轨道交通系统中的安全控制系统，它通过监控列车速度和各种传感信号控制列车的运动状态进行安全控制。ATS系统采集行车信息，实时传到指挥中心，ATP系统根据ATS给出的信息，按照列车制动能力、列车载重、外部环境等诸多条件计算出列车是否需要减速、制动，并给出最佳方案保证列车的行车安全。ATO系统接收来自ATS和ATP 的信息，控制列车使其在安全范围内运行，必要时自动制动。ATP系统是一个典型的周期执行系统，它是轨道交通控制软件的核心，如果发生错误会给人们带来不可估计的生命财产损失，因此保证其安全性和可靠性至关重要。本文以列车自动防护系统（ATP）为例介绍整个需求分析过程。

2 演化式需求建模

在构建形式化需求规约前，首先根据嵌入式控制软件特点定义需求模板，为领域专家撰写需求提供指导。

2.1 需求模板

尽管每个软件系统都有它独特的特征，但在相似的领域，仍然存在一些相同的特征，这些特征实际上是需求建模的基本元素，需求模板的设计需要满足这些领域特征。

经研究发现，嵌入式控制软件大多具有以下特点：1）系统功能基于确定的周期信号运行；2）控制软件中包含大量全局变量；3）系统明确指定功能的组织，以表示系统架构。这些特点实际上是一些基础的领域知识，假如为正确且准确的描述这些特点设计一种恰当的机制，那么领域专家可以方便地参与到需求建模过程中。本文通过定义需求模板来指导建立需求规约。需求模板如图2 所示。所有的领域特点都被组织为模板中的节点和关键字，如系统需求可以被描述为功能函数、数据字典和不变量，每个函数的输入输出变量都应该在数据字典中指定，前置、后置条件指出了输入和输出变量间的关系。根据需求模板，领域专家可以遵循他们传统的系统需求获取方式，而不用处理复杂的数学细节。

图2 ATP系统的需求模板Fig.2 Requirements template of ATP system

2.2 形式化需求规约构建

基于需求模板，可以使用三步演化式的建模方法逐步建立需求规约。

2.2.1 非形式化需求规约构建

在需求规约的构建过程中，需求分析人员更关注全局变量等被多数功能共享的数据资源。特别是对于嵌入式控制软件来说，在构建非形式化需求规约阶段，力求充分地将系统需要的全局变量等数据资源予以描述，对后续工作有重要指引作用。

大多数使用基于模型方法开发的软件，其开发起点都是需求的获取和分析。在需求规约建立初期，用户需求通常是粗糙且不完整的，在这个阶段，领域专家和软件工程师之间频繁的交流非常重要，因此，在撰写规约时使用自然语言更合适。非形式化需求文档的构建是一个初步建立需求描述的过程，在此过程中，需求内容的充分性是首要考量因素，而非需求内容本身的准确性。通过以自然语言书写需求，不同角色的工程人员可无障碍地参与需求分析过程。图3 为非形式化需求规约的示例。

图3 非形式化需求规约示例Fig.3 Example of informal requirement specification

2.2.2 半形式化需求规约构建

构建半形式化需求规约主要思想是对数据结构或系统结构等易于形式化定义的系统特征进行精确描述，而将功能的输出与输出变量之间的关系或者软件时序行为等难以直接用形式化语言描述的特征仍以自然语言描述。这样的需求文档可视为形式化和非形式化需求描述方式的一种平衡：既便于程序开发者理解需求，又便于需求分析者检查文档。

半形式化的需求文档侧重于对数据结构的形式化定义。在多数嵌入式控制软件中，存在大量全局变量，需要在需求分析和系统设计早期予以明确。需求分析人员需要形式化定义需求规约中涉及的所有数据结构，并精确定义每个需求条目的输入输出变量，最后将需求重新定义为独立函数。此时，需求规约是一个包含准确接口定义的结构化文件，但每个函数的前置、后置条件仍然是非形式化的。这一过程基于对领域知识和需求的理解，因为明确非形式化需求实际上是一个脑力工作，它依赖于对目标系统中预期功能的理解。图4 为上述非形式化规约对应的半形式化规约。其中，编号为［SWRQ-0200］的需求被分解为多个函数，每个函数都准确地定义了输入输出变量，但它们的前置、后置条件仍然是非形式化的。例如，变量MoOvEsState 是一个枚举类型变量，WhMaSp 是一个速度单元，被定义在数据字典中。半形式化规约是一个结构化的需求规约，它兼顾了准确性和易读性，可以方便地进行快速审查和简单验证。

图4 半形式化需求规约示例Fig.4 Example of semi-formal requirement specification

2.2.3 形式化需求规约构建

构建形式化需求规约的主要任务是把半形式化需求规约中的所有组件转化为形式化规约。此处使用CASDL（CAsco Specification Description Language）［16］形式化语言构建形式化需求规约。这个形式化表示法和Python 语言的风格类似，领域专家和软件工程师都可以很快掌握它。图5 为形式化规约示例。

图5 形式化需求规约示例Fig.5 Example of formal requirement specification

在形式化规约中，每个函数通过定义if-else 条件，形式化的描述了前置、后置条件，即输入、输出变量间的关系。为了表示需求变量所在周期，使用了信号变量k。如：需求变量MaMoDuBrOrS1（k）表示变量MaMoDuBrOrS1在当前周期的值，变量MaMoDuBrOrS1（k-1）表示上一周期的值，当变量表示当前周期的值时，k可以省略。

2.3 需求模型导出

需求规约构建完成后，为了进行后续的确认和验证，需要把形式化规约转化为可以执行的需求模型。此时，编译器是必须的，编译器包括解析器和模型生成器两部分。解析器把形式化规约转换为语法分析树AST（Abstract Syntax Tree），模型生成器通过遍历AST，把它转化为需求模型。

本文使用ANTLR（Another Tool for Language Recognition）作为实现解析器的组件。根据给定的语法信息，ANTLR 可以生成解析器解析生成AST，并返回词法、语法信息。模型生成器使用深度优先遍历的方法遍历AST 的每个叶子节点，生成需求模型。需求模型等价于形式化规约，但它更适用于机器读取。通过分析需求模型，可以生成多个图表以便验证需求正确性。算法1 解释了如何从需求模型中自动导出状态转化图。它以控制流图CFG（Control Flow Graph）作为输入，把结构化的数据流转化为状态转化图。类似地，其他图表也可以用同样的方式导出。

3 需求确认和验证

领域专家更关心它们关注的场景是否正确且充分的被形式化规约描述，而不是一些难以理解的数学符号，需求的确认和验证应该考虑到领域专家的需要，而不是一个黑盒。因此，在本文中，需求的确认和验证以领域专家为主导，场景及其预期输出由领域专家撰写。

3.1 场景撰写及执行

首先考虑场景撰写。对嵌入式控制软件而言，场景表示的是在一定的时间空间条件下，软件的载体的状态，但不同的人看到同一个场景的感觉是不同的。如对ATP系统，在外行人看来，ATP系统是列车的车载设备，其对应的场景是列车的停车、加速、匀速运动等列车运行状态。而在领域专家的视角下，列车的每一个运行状态都对应ATP 软件中的一系列变量的取值。

根据这个特点，本文规定了场景描述规则：每一个场景状态下都需要给出对应需求规约中的变量取值。例如：在ATP系统中的停车状态下，需求规约中的变量取值应和停车相符，即此时TrainStop 的取值应为True，而TrainSpeed 的取值应为0。图6 为场景描述示例，此类场景描述为后面的场景执行提供了便利。

图6 场景示例Fig.6 Example of scenario

图6 中‘->’后面的是列车运行动作，括号里的内容为动作参数，它表示的是在当前动作下的量化值。如“start”动作的动作参数是列车起始位置和延迟时间，所有的场景动作定义见表1。在图6 中，被’’’包围的是对该运行状态的解释，剩下的是需求变量赋值和对应的预期输出。需求变量的取值应和场景动作相符，如start 动作下的”车轮滤过停止”变量的取值应为True。预期输出表示的是在场景动作下，待测需求的预期值。

表1 场景动作Tabel 1 Scenario action

表1 中的场景动作1 为领域专家撰写的场景，为了方便后续的需求变量赋值，本文在对场景逻辑检查的同时加入了需要的参数信息，即场景动作2。

动态验证的下一个阶段是场景执行。由于规定了场景中必须包括相关需求变量的值，因此在执行需求模型时，测试数据方便的从场景中得到。但由于场景由人手工撰写，因此难免会漏掉一部分变量，导致场景执行出错。因此为了保证场景的正确执行，本文规定场景执行时需要遵循以下规则：1）周期执行，即对于周期控制系统，应保持其周期性；2）不影响执行结果原则，即对于没有输入数据的变量，在执行时，应根据模型特点对这类变量单独处理，保证执行结果不受影响。例如：在对ATP系统的验证中，列车的实际运行场景只有几个运行状态变化的场景，而ATP 软件执行了几百个周期，因此场景执行时不可能完全模拟现实生活中的列车场景。所以为了保持其周期性，正确的执行场景，列车的每个运行状态应被看作需求模型的一个周期，对应运行状态下的需求变量取值应为该状态执行完毕后相应变量的值。这样做不仅可以简化执行周期，缩短场景撰写时间，而且不会影响执行结果。

3.2 场景优化

为了进一步验证嵌入式控制软件的正确性，本文提出了场景优化方法。首先在大多数的嵌入式控制软件中，都存在模式变化。对于这类表示模式变化的特殊变量，如状态变量，不同状态间的转化关系需要严格定义，因此普通的场景不足以满足对这类特殊变量的验证。其次，在本文方法中，场景由领域专家手工撰写，导致效率不高。最后，在本方法中，场景的质量高低对整个验证结果有较大的影响。因此本文从特殊变量的场景优化、效率优化和场景质量优化这3 个方面优化场景。

下文将以列车自动防护系统（ATP）为例具体介绍场景优化方法。

3.2.1 特殊变量的场景优化

在对特殊变量的场景优化中，本文主要考虑状态变量的优化，从领域专家的角度来看，状态变量的如下性质需要被满足：

性质1无二义转化，对每个系统状态，每周期只能有一个状态转化条件被满足。

上述性质在嵌入式控制软件中是非常普遍的。它表示对任意一个状态变量来说，虽然存在多个转化条件，但要求在任意一个周期内，只有一个条件是被满足的，否则，系统的行为将会不可确定。

为保证状态转化的无二义性，各个状态间的转化条件应该是互斥的。本文从以下3 个步骤判断转化条件是否是互斥的：1）收集转化条件；2）通过两两组合，组成转化条件对；3）使用z3 求解器检查每对条件是否可以同时被满足。

图7 所示为列车运动打滑控制状态转化图，从中可以查看每个状态间的关系。显然，当一个状态和m个转化条件相连时，有m（m－1）/2 个条件组合需要被检查。

图7 状态转化图示例Fig.7 Example of state transition diagram

对条件组合的检查实际上是一个约束求解问题，如果一对条件有解，则说明它们不互斥，即状态转化是不正确的。本文使用z3 求解器求解这个约束问题，如果z3 求解器求解条件对的返回值是UNSATISFIABLE，则证明这2 个条件互斥，符合要求。

从状态SLIDING 转化到其他状态时的转化条件C1、C2、C3 如下：

这3 个转化条件组成了3 个条件组合：C1&&C 2，C1&&C3，C2&&C3，把它们代入Z3 求解器中求解，Z3 求解器的返回值是UNSATISFIABLE。所以这表明状态SLIDING 的转化条件是互斥的。

3.2.2 效率优化

为提高需求验证的效率，本文提出一种效率优化方法――自动生成场景。如在ATP系统中，自动生成列车场景中的列车运行状态和需求变量部分。自动生成场景时无需手动计算动作参数中的量化数据，并且场景中的需求变量赋值部分可以根据场景动作、动作参数和变量赋值规则自动生成。事实证明，这样可以提高验证效率。

在自动生成场景时，首先获取待测需求的所有输入；然后自动生成列车运行时的场景动作；最后根据变量赋值规则生成变量赋值部分。具体的场景生成方法如图8 所示。

图8 自动生成场景流程Fig.8 Flow chart of automatically scenario generation

首先考虑自动生成场景动作。在表1 的场景动作中，不同的动作的参数不同。如匀速动作的动作参数只有“匀速运行时间”一个参数，而加速动作参数中必须有“加速度”。因此本文根据场景动作的特点，自动生成对应参数，并计算此时的位置、速度等信息，方便后续需求变量赋值。具体的场景动作生成过程见算法2，其中，逻辑检查的目的是保证动作参数的值不能超过规定区间。本文使用速度公式和加速度公式计算列车的速度和加速度，并确保这些值在领域专家规定的最大范围内。

接下来考虑需求变量赋值。为了保证变量赋值的合理性，经研究发现，需求变量的取值与所在场景动作和场景序列的顺序有关，根据这个特点，本文定义了变量赋值规则，主要包括场景情景和变量赋值，具体见表2和表3 所示。其中，“场景情境”表示的是需求变量在不同的情境下应该如何赋值，“变量赋值”指的是不同类型变量应该如何赋值。根据变量赋值规则可以自动生成场景中的需求变量赋值部分。

表2 场景情境赋值内容Table 2 Assignment of scene situation

表3 变量赋值规则Table 3 Variable assignment rules

3.2.3 场景质量优化

领域专家撰写的场景，如果只能覆盖较少的一部分需求，则难以确定其他未被覆盖的需求是否正确地描述了预期的场景，造成分析质量低下。由于场景由领域专家撰写，因此，本文通过为领域专家撰写场景提供参考的方法，达到优化场景质量的目的。具体过程如下：1）求解未覆盖路径；2）生成未覆盖路径对应的测试用例。

未覆盖需求对应的测试用例为领域专家撰写场景提供参考。首先考虑未覆盖路径的生成。执行需求模型后，可以得到每个场景中的各个周期的需求覆盖行和整个场景的需求覆盖率。根据场景的需求覆盖情况，可以从中得到覆盖行和未覆盖行，通过向上追溯未覆盖语句的直接判断条件、间接判断条件，可以得到需求未覆盖路径。算法3 为未覆盖路径具体生成过程。其中cfg.mark 是覆盖语句标志，当它的取值为－1 时，表示该语句未被覆盖，其对应的判断条件及前置条件为未覆盖路径。

接下来生成未覆盖路径对应的测试用例。本文在生成测试用例时，采用MC/DC 覆盖准则，其广泛应用于嵌入式系统控制软件。MC/DC（Modified Condition/Decision Coverage）修正的判定条件覆盖准则，要求首先实现条件覆盖（每个判断中每个条件的可能取值至少满足一次）和判定覆盖（程序中的每一个判断至少获得一次“真”或“假”），并在此基础上，每个判定中的条件必须独立影响一个判定的输出。独立影响的意思是在其他条件不变的情况下，改变条件C1 的取值，判定结果也会随之改变。

算法4为测试用例生成算法，MCDC 函数的输入有表达式、前置条件。在求解测试用例时，为了实现MCDC中的独立影响原则，需要反复迭代计算判断条件。

3.3 需求确认和验证

本文目标是动态地验证需求规约是否准确且充分描述了期望的场景。领域专家首先撰写相应场景，然后根据场景中的数据信息执行需求模型，最后判断需求规约是否正确地描述了该场景，验证需求正确性。通过场景优化，可以提高整个验证效率，提高需求分析的质量。其中，通过验证状态转化条件的互斥性，保证了状态转化的唯一性。这些特殊变量往往贯穿于嵌入式控制软件的整个需求中，因此，对它们进行更严格的验证是必要的。

4 实验与结果分析

为评估本文方法的可行性，在CASCO 的ATP 项目中应用了需求建模和需求确认和验证。ATP系统的形式化需求规约由450 个功能函数组成，其中，为动态需求确认和验证生成了8 个状态转换图，对状态变量进行了更严格的验证。

为验证需求规约是否正确描述了期望的场景，通过执行领域专家撰写的场景，笔者发现了2 个需求错误。在对状态变量的验证中，发现了3 个“无二义转化”错误。除了状态转换图，还生成了300 个变量依赖图，以进行严格审查。通过变量依赖图，领域专家可以追溯和当前变量相关的所有变量，验证变量间的依赖关系是否符合要求。如果变量a的取值依赖于变量b、c的值，而在需求描述中，它的取值还和变量d有关，显然这种依赖关系是错误的。

本文方法还提高了需求建模和需求确认和验证的效率。具体结果见表4。可以看出，与传统的正式规约构建相比，使用演化式需求建模方法构建形式化需求规约的时间成本从3 个月减少到不到2 个月。其中，自动生成场景的方法可以大幅提高场景撰写的效率，手工撰写一条场景可能需要5 min～10 min的时间，而自动生成多条场景只需几秒钟。本文还验证了8 个状态变量的性质，与手动验证相比，验证时间从1 h～2 h 缩减到2 s。由于各种因素，例如：用户的经验或项目内容的不同，这种改进可能会有所不同。尽管如此，本文方法仍有助于验证验证需求正确性，从而可以发现更多潜在的错误。

表4 实验结果比较Table 4 Comparsion of experimental result

未覆盖路径及测试用例生成为测试人员撰写高质量场景提供了帮助。为了提高场景的质量，在一般情况下，测试人员需要先找到未覆盖语句，向上追溯未覆盖路径，分析需求未覆盖原因，从而撰写高质量的场景。本文方法为测试人员分析未覆盖原因节省了手动推导未覆盖路径的过程，并且测试用例的生成进一步为分析未覆盖原因提供条件。在表4中，根据场景执行结果，在450个需求条目中生成了60条未覆盖路径及测试用例，与手动分析相比，大幅缩短了未覆盖路径推导时间。

在整个需求验证过程中，需求建模往往需要耗费更多的时间，而当需求变更时，模型改动也较复杂，因此，如果能用有效的建模方法更快的建立需求模型，就可以大幅提高整个需求验证效率。在对场景的优化方面，本文通过自动生成场景，解决了在撰写场景过程中大量重复的物理计算问题，使领域专家可以重点关注领域专业相关的内容。

如在ATP系统中的列车运动打滑控制模块中，其需求描述中存在速度、加速度，如“进入可补偿的打滑状态时速度”“瞬时加速度”“平均加速度”等变量，如果场景要尽可能多的覆盖需求时，则需要考虑到不同的速度、加速度组合才能满足不同的判断条件。在我们的方法中，通过自动生成场景，可以省去大量的重复计算。

而当场景在需求模型中执行结束后，可以知道需求中哪一部分的内容没有被覆盖，为了验证这部分未覆盖需求的正确性，则需要分析需求未覆盖原因，撰写对应场景。在这个过程中，领域专家首先需要找到未覆盖需求，然后找到和该未覆盖行相关的所有判断条件，最后需要在判断条件中分析每个变量对场景的影响，从而撰写出对应的场景。这个过程中的一些重复操作可以自动完成，因此本文方法根据需求覆盖情况自动生成了未覆盖路径及其对应的测试用例。在图9 中的未覆盖路径示例中，为了满足判断条件，需要经过计算才能得到每个需求变量的取值。本文基于MC/DC 覆盖准则生成未覆盖路径对应的测试用例，如图10 所示，为领域专家分析需求未覆盖原因提供了帮助。

图9 未覆盖路径示例Fig.9 Example of uncovered path

图10 测试用例示例Fig.10 Example of test case

实验结果表明，本文方法可以有效地帮助嵌入式控制软件领域的领域专家改善需求建模和分析。它使从业人员可以有效地构建形式化的需求规约，而不是使用非形式化的规格说明进行分析需求。根据精确的形式化规约，将自动检测更多错误。从时间成本的角度来看，建立形式化规约可能会花费一些时间。根据领域专家的反馈，这种方法的一个重要优势是“考虑了特定领域的知识和功能”。与传统的形式化方法相比，这种方法可以使领域专家参与整个需求建模和需求确认和验证过程。在构建形式化需求规约时，它直接告诉从业人员“做什么”和“怎么做”，而不是只给出复杂的符号和形式化证明规则。另一个重要的方面是“工程过程”，它以连贯的方式结合了演化式需求建模和基于场景的需求确认和验证。

5 结束语

本文面向嵌入式控制领域提出一种基于场景的需求确认和验证方法。利用领域知识和特征设计需求模板，在模板指导下构建需求规约，并使用三步演化式建模方法逐步构建形式化的需求规约，导出需求模型，同时生成需求确认和验证需要的各种图表。在此基础上，领域专家根据规则撰写场景。通过执行场景，领域专家可以判断需求规约是否正确的描述了期望的场景。本文通过设计特殊场景，验证了特殊变量的正确性；通过自动生成场景，提高了需求验证的效率；并通过求解未覆盖路径及测试用例，为提高场景质量提供了帮助。实验结果证明了本文方法的可行性。未来将对场景做进一步优化以适用更多情况，如给出场景撰写规则以提高场景质量。