ISO26262环境下需求验证的成本效益方法研究

工程科学与技术，国际期刊23（2020）494完整文章ISO26262环境下的（用户友好型）正式需求验证Denis Makartetskiya，Guido Marchettoa，Riccardo Sistoa，Fulvio Valenzaa，Rimini a，Matteo Rimilioa，Denise Lerib，Paolo Dentib，Roberto FiniziobaDipartimento di Automatica e Informatica，Politecnico di Torino，c.so Duca degli Abruzzi 24，Torino I-10129，ItalybCentro Ricerche Fiat（CRF），Str. Torino 50，都灵，意大利阿提奇莱因福奥文章历史记录：收到2019年2019年9月13日修订2019年9月18日接受在线发售2019年保留字：ISO26262形式化方法SysMLA B S T R A C T为了达到最高的安全完整性水平，ISO 26262建议在道路车辆安全相关嵌入式系统的整个生命周期中，对各种验证活动使用正式方法。由于正式的方法是众所周知的难以使用，这些ISO26262要求提出的主要挑战之一是找到符合它们的成本效益的方法。本文提出了一种需求形式化验证的方法，其中形式化方法、语言和工具只对用户暴露最少，并集成到一个常用的基于SysML的系统建模环境中。这种方法不需要特殊的专业知识，仍然允许应用它们。因此，应限制人员培训费用和发展费用。所提出的方法已被实现为Topcased环境的插件。虽然它仅限于离散系统模型，但它已成功地在工业用例上进行了实验。©2019 Karabuk University. Elsevier B.V.的出版服务。这是CCBY-NC-ND许可证（http://creativecommons.org/licenses/by-nc-nd/4.0/）。1. 介绍汽车系统的复杂性不断增加，给系统安全工程领域带来了新的挑战。我们的日常生活证实了这一说法，在日常生活中，我们不断与电气和/或电子（E/E）系统相互作用，其可能的故障可能会产生巨大的安全后果和影响（汽车安全气囊和巡航控制只是两个代表性的例子）。从这些考虑出发，ISO 26262[1]是为满足道路车辆内安全关键系统的特定需求而制定的标准，适用于完整的汽车安全生命周期：管理、开发、生产、运营、服务和退役。它提供了一种基于汽车特定风险的方法来确定汽车安全完整性等级（ASIL），这是标准中定义的一种风险分类方案，用于分析和分类特定潜在危险的影响ISO 26262标准第6部分中描述的V模型（图1）与软件开发的标准V模型非常相似。主要的区别是最初的重点*通讯作者：Dipartimento di Automatica e Informatica，Politecnico di Torino，c.so Duca degli Abruzzi 24，Torino I-10129，Italy.电子邮件地址：fulvio. polito.it（F.瓦伦扎）。由Karabuk大学负责进行同行审查安全性，以及增加的向上设计阶段验证阶段的数量该软件V模型包含在一个更广泛的V模型中，该模型涉及整个产品开发，并分为系统、软件和硬件开发阶段。在产品开发的各个阶段，ISO 26262建议使用各种规范和验证技术。在处理分类为ASIL最高级别的项目时，建议采用正式和半正式方法。关于形式化方法的最相关建议参考V模型的左侧，其中，对于不同抽象级别的安全要求和系统设计的规范，例如，必须验证软件安全性要求与技术安全性要求（表示系统级开发过程的输出要求）的符合性和一致性，为此建议使用形式验证技术。虽然形式验证技术在ISO 26262背景下的关键作用通常被很好地理解，但其应用仍然显得有点模糊，具有工业背景的人通常仍然不愿意利用形式方法，因为它们已知难以使用且非常耗时https://doi.org/10.1016/j.jestch.2019.09.0052215-0986/©2019 Karabuk University.出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。可在ScienceDirect上获得目录列表工程科学与技术国际期刊杂志主页：www.elsevier.com/locate/jestchD. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494495图1.一、ISO-26262 SW V模型。（从经济学的角度来看，这是一项艰巨的任务）[2]。所有这些观察使我们直觉地认为，需要更用户友好的工具来帮助不熟悉形式化方法的人，接近并有效地使用现代工具来正式建模和验证他们实际设计和实现的系统另一个可行的办法是培训人员，传播必要的知识和技能，以自主执行和完成核查任务。虽然从长远来看更具吸引力，但从成本角度来看，该解决方案并不容易实施，因为它需要培训时间和相关成本，更不用说许多公司可能无法负担的初始学习曲线。本文通过提出技术和工具来解决这些问题，这些技术和工具有助于消除在符合ISO26262的开发过程中使用正式方法的主要障碍。特别是，我们的目标是帮助在设计阶段验证预期在左手边的V模型，其中的能力在不同的抽象层次上比较模型（回到抽象层次）是必需的，并且在基于需求的测试活动中是必需的，在V模型的右边。更具体地说，我们的工作试图应对上述挑战，通过提出一种建模方法，该方法不需要形式化方法中的复杂技能，并且基于业界人士已经意识到和熟悉的概念进行定制：状态机，活动图和序列图是学术界和业界人士已经知道的“语言”的明显例子特别是，这些语言已经是基于UML的半形式化符号的一部分，例如SysML[3]，它在汽车行业中广为人知并被接受[4，5]。SysML的一个有价值的特性是，它包括了用上面提到的用户友好的语言表达的相关行为模型来规范分层需求的可能性这使得能够根据ISO26262的建议管理安全要求，同时通过这种行为模型正式规范要求。虽然SysML被认为是一种半形式化的符号，但它的非形式化符号非常接近于完全形式化的模型，并且可以通过解决这些语言定义中剩下的几个变量点来将它们在不同的抽象层次上创建了需求和系统的正式模型之后，就提出了这些模型如何相互关联的问题。一个较低层次的模型抽象的本质实际上是遵循更高层次的抽象，通过添加更多的细节，同时保留更高层次抽象的粗糙行为？为了以形式化的方式回答这个问题，可以使用精化检查，即对更抽象的形式工件是否正确地精化为不那么抽象的工件进行形式化检查。细化检查的主要优点是，com-与其他形式验证技术（如模型检查）不同的是，它不需要用户指定时态逻辑中的形式属性，这是已知的挑战[2]，但它可以直接应用于用户开发的模型，具有更用户友好的符号。特别是，我们提出了细化检查的appli-阳离子从SysML模型中提取的行为模型，这是一种新的方法，在ISO 26262的上下文中，讨论了相关工作部分。我们工作的最后一个组成部分是一种技术，用于自动生成测试用例的形式化需求规格说明，通过行为模型的方式表示。这些自动生成的测试用例可用于基于需求的测试，这是ISO26262在V模型右侧推荐的测试方法之一，也可作为细化检查的替代方案，用于向上的设计时验证，当细化检查由于形式模型过于复杂而不可行时。虽然从正式的行为规范自动生成测试用例本身并不是新的，但这种使用它的方式，通过提出的方法成为可能，是新的。本文的重点是离散系统和相关要求。虽然我们提出的方法可以扩展到处理连续时间系统或涉及定量时间的需求，但这种扩展超出了本文的范围。我们提出的方法利用了许多其他研究人员在过去已经开发的技术：从UML/SysML行为图中提取形式模型，验证形式模型的细化，以及从形式模型中自动生成测试用例。我们的主要贡献是它们被连接在一起的方式，以符合ISO 26262标准的建议，关于使用正式的方法（特别是设计时验证），而在同一时间隐藏的复杂性，正式的方法，从最终用户，从而实现了一个工具集，甚至可以使用的用户，没有特定的专业知识，在正式的方法。虽然有实现这种隐藏的替代方案，但它们都没有实现我们所做的所有目标。为了演示的目的，我们的想法已经开发和集成，在插件的形式，到Topcased，基于Eclipse的建模环境，支持SysML，其中所有的细节相关的正式验证过程保持，尽可能多的，幕后和自动处理的工具。[1]然而，需要注意的是，拟议的工具链并不打算完全取代所有与ISO-26262相关的活动，而是作为支持某些与正式方法相关的部分的可能方式。它可以被认为是一个核心功能，需要1该插件可从https://github.com/netgroup-polito/VeTeSS-Topcased-Verification-Plugin下载。496D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494然后与其他工具集结合，以实现完全符合ISO-26262的过程。在本文的其余部分，我们将通过以下议程涵盖所有这些方面：第二节介绍了在SysML上下文中指定安全需求的建议方法第三节展示了如何在设计时根据ISO 26262的建议开发新的安全要求时正式验证细化，而第四节展示了基于安全要求自动生成测试第五节介绍了将所提出的方法应用于行业用例的一些结果。第六节讨论了相关工作，最后，第七节总结了本文。2. 安全要求形式化只要有正式规格，就可以进行正式核查在我们的例子中，获得正式规范的起点SysML是一种基于UML的半形式化符号。它继承了UML的几个特性，并扩展了UML的其他特性，这些特性是系统建模所特有的SysML相对于UML的一个关键扩展是对需求及其关系建模的在SysML中，系统结构通过结构图来描述。主要的是方框图，将一个系统或其一部分描述为相互连接的方框。行为图通过允许通过各种形式主义规范系统行为来完成系统模型所有的行为图都继承自UML：活动图使用类似于Petri网的形式，序列图使用消息序列图，状态机基于分层扩展状态机，而用例图是表示接口和用例的一种方式最后，需求图是一种表示系统需求及其关系的方法。需求与需求之间的关系以及需求与系统模型元素之间的关系都是可能的。可以定义的主要关系派生关系将派生需求与其源需求之一相关联满足关系将模型元素与该元素要满足要求相细化关系将一个模型元素和一个需求联系起来，其中两个元素中的一个比另一个细化得更详细细化关系允许将行为模型与需求相关联;验证关系将需求与测试用例相关联，该测试用例可用于验证需求是否得到满足。请注意，一个需求可以源自一个或多个源需求，多个需求可以源自同一个源需求，并且类似的考虑适用于其他关系。SysML的一个可能的替代方案是EAST-ADL[6]，这是一个专门为汽车系统设计的丰富框架，并考虑到ISO-26262。由于我们所利用的关键语言特征同时存在于SysML和EAST-ADL中，因此本文提出的方法可以用EAST-ADL代替SysML。尽管EAST-ADL对汽车系统具有更好的特异性，但它的工具支持和扩散仍然较少。出于这个原因，我们更喜欢使用SysML进行概念验证。我们建议在ISO26262项目中使用SysML建模来指定系统级安全需求的方法如图2所示，其中黄色箭头表示派生关系（例如：技术安全要求源自功能图二.使用SysML指定ISO26262要求的可能方法。安全要求），红色箭头表示满足关系。在系统建模方面，分解关系（图中蓝色的）。 2）用于表示系统的层次分解，并细化关系（绿色），用于连接不同抽象级别的相应系统块（例如，功能块到相应的物理组件）。请注意，这里我们建议使用同样的细化关系，也用于将需求绑定到其相应的系统元素或行为模型，但要关联系统模型。我们建议的关键点是，负责定义安全需求的工程师应该将其指定为SysML需求，并且，对于需要正式规范的每个需求，他们必须提供相关的行为图，该行为图根据需求指定系统的预期行为。在图3中以其文本形式（左）和行为图（状态机）的形式示出了以高抽象级别表达的安全气囊要求规范的示例，该行为图（状态机）规范了根据该要求的系统的预期行为在图3的示例中，使用具有两个事件的状态机来表达要求：start_cc表示临界碰撞的开始，而deploy表示气囊的展开如果没有临界碰撞开始，安全气囊不能展开的事实可以由具有两个状态的机器表示：一个状态表示临界碰撞开始之前的系统行为，而第二个状态表示该事件之后的系统行为。部署事件只在第二种状态下是可能的，而在第一种状态下是不可能的，这一事实捕获了需求。图4展示了如何对更复杂的需求进行建模的另一个示例。从这些要求开始，可以制定更详细的要求，以具体说明满足原始要求的技术手段。新的、更详细的需求必须细化原来的抽象需求，并且这种细化关系可以被检查，如第3所讨论的。在我们看来，与需求相关的行为图是它的权威规范，而文本只是它的解释。我们通过将UML行为图转换为CSP（通信顺序进程）[7，8]，为与SysML需求相关的UML行为图分配了一个正式的语义，CSP是一种用于并发运行并可以相互通信的离散事件顺序进程的正式描述语言。这种将形式语义分配给UML行为模型的方法并不新鲜[9]：从行为图到CSP的转换算法已经存在，它可以解决剩下的几个变化点●●●●D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494497图三. 需求建模示例。见图4。 另一个需求建模的例子。图的UML语义（例如，事件被分派到状态机的方式）。这种基于CSP的方法的主要限制是CSP不能用于表达定量时间和连续时间模型（例如，我们不能正式表达两个给定事件之间经过的时间小于1ms的要求）。3. 安全要求推导的形式化验证3.1. 所提出的精化检查方法我们提出的验证方法的基本思想是，派生的需求必须细化其源需求。如果每个需求都与一个行为模型相关联，该模型根据该需求规范了系统的预期行为，则可以比较由派生关系约束的需求的行为模型，以便检查源需求的行为是否被派生需求的行为正确地细化。由于在我们的方法中，SysML需求由CSP过程形式化地表示，并且CSP具有精化理论，因此可以利用该理论来检查精化关系。精化关系的形式化验证称为精化检查[7]，它是CSP中一种众所周知的形式化验证技术。一般来说，细化关系可以是形式化细化概念的任何关系，理想情况下，细化概念应该在规范及其实现之间保持。 如果规范是一个需求，并且它的实现是应该满足需求的系统模型或一组（更详细的）派生需求，则可以使用细化检查来验证系统模型或派生需求是否满足原始需求。例如，如果M的每个执行跟踪（即事件序列）也是MA的执行跟踪，则更具体的模型M和更抽象的模型MA之间的跟踪细化成立。相反地，如果M可以具有在MA中不能发生的事件序列，则该关系不成立。已知迹线细化保留所有安全属性，即指定不想要的东西永远不会发生的所有属性。这意味着，如果M是MA的迹精化，则M满足MA所满足的所有安全性质。另一个可以考虑的关系是模拟细化。M是MA的模拟细化，如果M逐步模拟MA，即，如果M中的每个可能步骤总是对应于MA中的可能步骤，并且M中的步骤和MA中的步骤导致再次通过相同关系相关的状态。可以说，模拟细化比迹线细化更强，并且迹线细化隐含在模拟细化中。已知仿真精化保留所有线性时序逻辑（LTL）属性（不仅是安全属性）和所有计算树逻辑（CTL*）属性的大子集。通常，这些关系的弱化版本例如，弱模拟细化要求只有一些步骤（可观察的步骤）在另一个模型中具有匹配。以这种方式，可以正确地将抽象模型中的一个步骤对应于细化模型中的一系列步骤的情况相关联。当然，在这种情况下，只有不涉及不可观察步骤的属性才能被保留。由于我们主要对安全属性感兴趣，因此痕迹可以细化-这对我们的目的来说已经足够了。此外，由于我们必须在不同的抽象级别上关联模型，因此我们使用弱跟踪细化，这忽略了被分类为不可观察的事件。在我们的例子中，只有当事件属于抽象模型的字母表时，它们才被认为是可观察的，而发生的事件只被认为是不可观察的，除非它们被显式地声明为匹配抽象模型中的相应不同事件，在这种情况下，相应的事件被重命名为相同的事件。通过这种方式，允许细化模型在匹配抽象模型的任何两个可观察事件之间生成许多不可观察事件。由于我们允许更多的需求从一个抽象需求中派生出来，通常我们需要检查498D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494要求R 1，.. . ，Rn正确地细化抽象要求Ra。精化检查问题可以通过检查CSP过程I是另一个CSP过程Pa的弱迹精化来公式化，其中Pa表示Ra所需 的 系 统 行 为 ， I 表 示 R1 ， . . .. 过 程 I 计 算 为 I= （ Q1\a1 ） ||...（Qn\an），其中||是CSP 的并行组合操作符，这意味着所有共享事件的同步，Qi是表示Ri所需的系统行为的进程，具有应该映射的事件到Pa3.2. 将建议的方法集成到ISO 26262过程中由于其所提到的含义，细化检查可以用作执行ISO 26262所称的设计时符合性验证的一种方法。例如，ISO 26262第6部分第6.4.7条规定应验证软件安全性要求提供证据，证明其符合技术安全要求。这些设计时验证可以使用形式化方法完成（建议对最高ASIL级别进行形式化验证），前提是满足以下要求或系统模型进行比较。让我们假设需求的正式规范是使用SysML行为图完成的，如第3.1节所示，可能会添加一个规范，即某些不同事件对应该被视为相同。有了这些规范，形式验证可以通过细化检查，使用弱痕迹细化，并将事件分类为可观察和不可观察的，如上所述。在汽车工业中，一个典型的开发过程是使用SysML描述安全需求和表达初始系统结构，然后开发更详细的Simulink为了将我们的方法 扩 展 到 在 需 求 和 Simulink 模 型 之 间 执 行 细 化 检 查 ， 应 该 从Simulink模型中提取正式的CSP模型。另一种方法，使我们的方法，是通过测试验证细化。特别是，可以使用“背靠背比较测试”的形式在稍后阶段，当从Simulink模型生成C代码时，在适当转换所涉及的事件之后，可以应用相同的测试用例来测试C代码。这是一种基于需求的测试形式，是ISO 26262推荐的测试方法之一。3.3. 所提出的细化检查方法的实现存在几种基于CSP理论的精化检查器。在我们的Topcased插件中，验证由PAT（Process Analysis Toolkit）[10]提供的工具实现，该工具根据该理论有效地实现了细化检查，并提供了从UML行为图自动生成CSP流程的算法。我们实现的插件所遵循的过程如图5所示。其工作原理如下：在模型中识别派生关系，并且通过模型的XML表示的XML转换，从模型中提取与派生关系所绑定的需求相关联的状态机（或其他行为模型）。图五. 细化插件验证工作流。从每个提取的行为模型自动生成对应的CSP过程。这是通过利用PAT提供的算法从UML行为图创建CSP流程来实现的。对于必须检查细化的派生关系所约束的每组行为模型，构建CSP验证模型，该模型包括要检查的弱跟踪细化关系和所涉及的CSP过程的规范，如第3.1所述构建。在CSP验证模型上调用PAT，以便在相应的CSP规范之间执行细化检查。验证结果（包括在发现错误的情况下的反例）被转换回SysML世界，并由插件报告考虑到细化检查是我们正式验证方法的一部分，运行完整验证任务所需的具体工具链（从建模阶段开始，以验证结果结束）如图6所示（蓝色背景框表示专门为我们的目的开发的工具，而其他框是已经存在的工具;关于测试用例生成的部分不包括在图片中，但它将在第4节中讨论）。由于SysML用于需求及其相关行为模型的规范，因此可以使用任何支持SysML并可以以XMI格式导出模型的建模工具。SysML还用于表达绑定需求的派生关系（通过这种方式，用户可以指定如何从以前的需求派生出新的需求），并满足将需求绑定到实现它们的系统模型元素的关系。派生关系还支持需求跟踪，这也是ISO26262所要求的。关于在派生关系所约束的需求中发生的事件的映射的信息可以作为SysML中的属性添加到派生关系本身（它被指定为事件对的集合）。在[11]中初步描述的工具链集成在Topcased环境中，其中使用专门的插件来驱动整个验证过程。更准确地说，该插件分析SysML模型并自动提取派生关系绑定需求。用户可以通过选择验证中涉及的需求来交互式地决定应该检查哪种关系的细化。然后，对于每个选定的派生关系，插件自动提取与关系所绑定的需求相关联的行为模型，将其转换为CSP，并生成PAT的输入，如已●●●●●D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494499图六、使用状态机和细化检查的形式化验证工具链解释道最后，自动调用PAT并检查细化结果（包括失败情况下的反例）最终通过插件本身报告给用户。该工具提供的另一种可能性是使用测试来验证细化检查。在这种情况下，该工具自动执行测试用例生成（更多内容将在第4节中介绍），从更抽象的需求的行为模型，然后在更具体的需求的行为模型上执行生成的测试。图11中的屏幕截图显示了插件的GUI是如何出现的。在这个屏幕截图中，可以看到一个面板，在这个面板中，分层需求及其关系被图形化建模，在下面的面板中，Verification插件的视图带有RefinementChecking选项卡，插件在其中显示提取的派生关系。在此选项卡中，用户可以进行选择并开始细化检查验证。在图11所示的示例中，关于安全气囊系统使用情况，可以查看由DeriveReqt关系绑定的两个需求。示例中显示的两个需求具有行为模型，表示为与它们相连的状态机。每个状态机都在一个单独的图中指定，使用相同的建模环境。图9显示了更抽象的需求（Deploy_should_be_before_by_critical_collision）的状态机图，它表达了一种优先关系：deploy事件必须总是在critical_collision事件之前更具体的需求（Deploy_within_two_time_ticks_after_collision ）有一个状态机，如图所示。8 .第八条。为了验证两个需求之间的细化关系（即Deploy_within_two_time_ticks_after_collision正确细化Deploy_should_be_preced_by_critical_collision），我们必须在列表见图8。 状态机附加到更具体的要求。关系，如图所示。 11，然后按下开始验证按钮（刷新按钮用于创建关系列表或在修改模型后更新关系列表）。图 7显示了验证报告，表明细化关系不成立。为了理解为什么细化 不 成 立 ， 可 以 看 看 反 例 （ init -> [start] -> [collision] ->deploy），它是一系列事件，可能发生在具体行为中，但不会发生在抽象行为中，从而使细化无效。反例中方括号内的事件表示隐藏事件，即不被考虑的事件，因为它们不被两个行为模型共享在这个特定的例子中，可以看到deploy可以在没有critical_- collision的情况下发生（它在collision之前，这是一个隐藏的事件）。问题的出现是因为在两个要求的描述中，两个不同的事件被用来表示冲突（一种情况下是collision，另一种情况下是critical_collision通过在两个需求中使用相同的碰撞事件或指定在细化验证中应将这两个事件视为相同事件这可以通过选择细化关系和添加两个事件的映射来修复后，如果我们重复细化检查，我们会得到关系保持（有效）的结果。插件为此验证任务生成的CSP验证模型如清单1所示。其中，实现过程对应于第3.1节中I所示的过程，而前两个定义的过程是从两个状态机自动生成的过程。4. 基于需求的测试用例的自动生成测试是ISO 26262推荐的主要验证技术 图图10说明了针对一组需求测试被测系统（SUT）的过程（基于需求的测试）：见图7。 验证失败的验证报告（和反例）。500D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494见图9。 状态机附加到更抽象的需求。清单1.用于样本精化检查的CSP模型。见图10。基于数据的测试。首先，会编制一套测试程序，即一套涵盖所有安全规定的测试个案。测试用例由输入刺激和预期结果组成测试执行运行SUT，并将每个测试用例指定的输入提供给SUT，然后将SUT输出与预期的输出进行比较覆盖度量评估测试套件是否足够完整;如果不是，则必须创建更多的测试用例以达到目标覆盖率。作为手动测试用例生成的替代方案，基于模型的测试（MBT）包括从抽象模型中导出测试用例（对于基于需求的测试，必须使用需求模型）。本节介绍了如何在我们的方法中使用从SysML模型派生的正式行为模型（并与安全需求相关联）来自动生成测试根据ISO 26262，可用于基于需求的测试和验证软件安全需求的案例生成的测试用例集的大小可以随后通过基于仿真的算法来优化，该算法修剪冗余测试用例。请注意，基于需求的测试只是ISO-26262推荐的几种测试方法之一使用各种测试方法有助于更大的多样性和更好的发现错误的机会。大多数关于反应系统MBT的现有文献从形式模型开始，基于有限状态机（FSM）和标记转换系统（LTS）模型[12]。由于这些模型非常通用，许多其他规范形式主义（例如进程代数，Petri网，扩展/分层状态机模型），包括SysML支持的那些，可以根据这两个基本模型进行解释。这为将相同的MBT技术应用于各种建模语言提供了可能性。如前所述，即使我们考虑半形式化的UML和基于UML的规范语言，也有可能从UML模型的某些部分导出相应的形式化模型，只要UML模型中的语义变化点例如，使用这种方法，可以为UML状态机提供形式化的语义，这使得它们可以用LTS来解释基于有限状态机的方法的一个限制是，它们通常只考虑确定性机器。当然，非确定性机器可以变成确定性机器，但代价是状态爆炸。这个特性使得基于有限状态机的方法不适用于大型非确定性模型。一个很好的观点是，D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494501见图11。 插件的GUI然而，基于FSM的方法是，它们已经通过搜索最小测试进行了高度优化[13]。LTS方法更一般，因为它们处理不确定性和无限状态系统。对于大型或无限状态系统，通常使用惰性（动态）评估。由于它们能够处理不确定性和无限状态系统，基于LTS的方法似乎更适合我们的上下文。特别是，基于LTS的理论中似乎最合适的是处理I/OLTS的理论（[12]的第7章）。该理论包括几种实现关系的定义和构建测试套件的方法。4.1. 带I/O LTS的MBT根据MBT与I/O LTS的理论，与安全需求（即规范）相关联的SUT的行为模型被转换为I/O LTS（具有分为输入、输出和内部的标签的LTS）。模型必须是这样的，它永远不会拒绝输入（所有状态下的所有输入都可用;这可以通过完成不完整的规范来实现，例如，忽略未指定的输入即通过在所有状态中为非指定输入添加自循环如果模型具有静态（即，不可能发生输出的状态），这些通过向该状态添加自循环来标记，用特殊的D标签来标记 图12示出了从不拒绝输入的I/O LTS的示例，其具有两个输入（？C和？nc）和两个输出（！as和！ar），以及已经添加的额外的d个事件见图12。 I/O LTS的例子。测试生成可以针对一个或多个不同的实现关系。最简单的关系是迹线细化（见第3节）。最常用的关系是ioco（输入-输出一致性）[14]。该关系是考虑规范的迹线（包括特殊事件d）来定义的。如果在这些跟踪之一之后，实现可以执行的输出是规范在同一跟踪之后可以执行的输出的子集，则关系成立。这种关系比跟踪细化弱（跟踪细化意味着ioco），因为ioco不会以任何方式约束规范无法执行的跟踪之后的实现。然而，如果实现和规范都有相同的事件字母表，从不拒绝输入，并且用事件来从模型生成的每个测试用例也是一个I/OLTS，其最终状态被标记为成功、失败（和不确定）。该LTS具有与w.r.t.相反的输入和输出。规格。在每个州，502D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494或者发射恰好一个输出（即，到系统的输入）或者接收任何输入（即，来自系统的任何输出）或者对应于d的特殊事件（指示系统静止的超时）。应用测试用例意味着逐步执行它，直到达到最终状态。最终状态的标签决定了测试用例的结果。如果系统是不确定的，每个测试用例都应该重复几次，只有当所有的运行都以通过结果结束时，我们才可以说测试用例已经通过。4.2. MBT工具链在我们的方法中，MBT是通过执行测试用例生成与安全要求相关的行为模型这些模型会自动完成输入（因此它们永远不会拒绝执行输入）和d事件。当使用MBT进行测试细化时，SUT模型也以相同的方式完成，并且仅在实现中发生的事件被认为是内部的（即既不是输入也不是输出）。通过这种方式，我们可以确保ioco和traces细化一致。在 我 们 的 示 范 性 Top-cased 插 件 中 执 行 MBT 的 工 具 链 基 于CADP/TGV[15]，这是一个已经存在的工具，可以自动生成测试用例，用于测试I/O LTS模型上的ioco关系。TGV的输出是集合的测试用例，每个测试用例由一个I/O LTS表示，陷阱状态：TGV的输入由两个I/O LTS组成：一个规范和一个测试目的。规范是SUT预期行为的模型。测试目的是测试生成必须考虑的SUT行为部分的表示例如，这可以用于限制每个测试用例的大小。一个测试目的必须是完全的，也就是说，它必须是这样的，所有的事件必须是可能的，在所有的状态，它必须包括两组特殊的状态称为陷阱状态：一组接受状态和一组拒绝状态。每个接受或拒绝状态必须包含所有事件的自循环（这就是为什么它被称为陷阱状态）。接受状态的含义是，当达到它时，我们感兴趣的行为已经被观察到。相反，拒绝状态是这样一种状态，当达到该状态时，意味着观察到的行为与测试无关。在这两种情况下，测试都必须停止。如果达到接受状态，如果SUT的所有输出都在预期的输出中（如规范中所指定的），则生成接受判决。否则，如果达到拒绝状态并且SUT的所有输出都在预期的输出中，则发出不确定的判决。最后，如果SUT生成意外输出，则会生成失败判决，但这在输出I/O LTS中仍然是隐含的（如果输出不存在，则意味着失败）。TGV包括通过为所有缺失事件添加自循环来完成不完整测试目的的可能性。此外，TGV会根据需要自动添加d个事件。当TGV将规范和测试目的结合到单个I/O LTS中时，d事件的生成对于测试用例的生成，TGV使用了一种惰性评估技术，它可以限制内存消耗量。TGV可以接受以多种输入语言指定的输入，并将其转换为I/O LTS形式。不幸的是，TGV不能将CSP作为输入。但是，它可以采用LOTOS2[16]，这是另一种类似于CSP的正式规范语言。由于LOTOS受到CSP的启发，其进程代数与CSP非常相似请注意，TGV被选为最适合我们的问题，因为我们2LOTOS是一种专门为OSI（开放系统互连）体系结构的形式化描述而开发的规范语言，尽管它通常适用于分布式并发系统。图十三.执行MBT的工具链。MBT工具能够基于ioco关系执行测试用例生成，可以直接将CSP作为输入。由于我们已经有了从SysML抽象模型生成的CSP模型，我们创建了一个从CSP到LOTOS的转换工具，以便能够使用CADP TGV生成MBT测试用例。在LOTOS中，输入和输出事件之间的区别可能是不可能的，TGV使用一个单独的文件来给出此规范（即每个事件是否必须被视为输入或输出）。这也由转换器自动生成。最后，为了尽可能地限制用户的手动工作，创建了自动测试目的生成器。如有必要，用户可以编辑测试目的。图1显示了这种方法产生的完整MBT工具链。 13岁这个基本方法已经集成到我们的Topcased[17]环境插件中，以及细化检查工具。在同一个插件中使用这两个工具可以使代码重新...使用简单，并提供了一个单一的环境，用户可以在SysML中开发软件安全需求模型，使用精化检查工具检查需求之间的精化关系，并从安全需求模型开始生成测试用例。5. 实验结果在 VeTeSS （ 支 持 功 能 安 全 标 准 的 验 证 和 测 试 ） 欧 洲 项 目（https://artemis-ia.eu/project/43-vetess.html）中，通过示范性工具链对FCA（菲亚特克莱斯勒汽车公司）研究中心CRF（CentroRicercheFiat）VeTeSS开发了标准化的工具和方法来验证安全相关系统的鲁棒性，特别是针对瞬时共因故障。CRF为该项目选择的用例是用于HEV/EV的电动换档器（e-shift [18]）：当（由驾驶员或自动地）选择停车模式时，该系统提供变速器的机械锁定或解锁，避免车辆在停止时的不希望的运动。电动选档杆由车辆控制单元（执行控制策略）、多个开关（感知驻车、行驶、倒车和空档按钮）和驻车锁致动器（执行驻车棘爪电机的指令）组成。 在该项目中分析了两个已确定的安全目标：避免停车制动器的意外解锁（SG#1）和避免汽车移动时停车制动器的意外激活（SG#2）。从已有的e-shift系统模型及其安全需求的自然语言表达出发，建立了相应的SysML模型，并根据所提出的方法对安全需求进行了形式化。这项工作是由CRF的一组工程师完成的，他们D. Makartetskiy等人/工程科学与技术，国际期刊23（2020）494503不幸的是，目前，软件安全要求不适用于e-shift用例。仅系统级要求可用（功能和技术安全要求）。因此，使用可用要求进行了评价这意味着我们已经根据我们的方法检查了功能安全要求和技术安全要求之间的合规性和一致性。同样，测试用例也是根据技术安全需求而不是软件安全需求生成的。然而，我们认为这种实验仍然是有意义的演示和评估的方法，它也是相关的软件，考虑到测试用例派生的技术安全需求可以用于软件在环测试。即使不是所有可用的安全需求都已正式化，但其中的一个重要子集及其相关行为已在SysML中正式化。对于这些需求，插件能够检查细化关系，对于技术安全需求，它能够生成测试用例，正如预期的那样。正式化要求的子集包括安全目标SG#2、9项功能安全要求以及由此衍生的18项这些包括与D按钮相关对于其中一项要求（TSR#008），已将工具生成的测试用例手动转换为Simulink相关的时间历史。作为一个例子，这里给出了一个技术安全要求（TSR#011）的测试用例生成。要求文本为：此要求已使用中所示的状态机进行了形式化图 十四岁状态机由主状态（状态1）组成，该主状态由以下各项组成：两个区域（代表平行行为）。下部区域表示制动踏板状态的演变，而上部区域表示驾驶模式的演变。在状态机中发生的事件的含义在表1中定义 。 下 层 状 态 机 通 过 两 种 状 态 对 制 动 踏 板 状 态 进 行 建 模 ：PressedAndValidated和Other。最初的状态是其他的，但它可以随时改变。状态机表示当制动踏板状态处于“PressedAndValidated”状态时表1要求#011的事件含义。P_in进入P驾驶模式D_in进入D驾驶模式R_in进入R驾驶模式N_in进入N驾驶模式B_valid_pressed传达制动踏板状态的采集/验证结果，该结果为valid- pressedB_有效_未按下制动踏板状态的获取/验证结果被传送，并且该结果是有效的-未按下B_invalid制动踏板状态的采集/验证结果被传送，且该结果无效shifter_pos_to_D将Shifter_pos信号设置为D模式当状态为“其他”时，结果可能是有效-未按下或无效。上层状态机通过两种状态对驾驶模式进行建模：P模式和P模式。在PMode内部有两个子状态：PState1和PState2。后一状态仅在事件B_valid_pressed之后达到，即仅在制动踏板状态的最后