|
摘要： 随着控制系统复杂度的提升，系统开发效率和可靠性都在下降。在仿真技术和自动代码生成技术出现以后，基于模型的设计方法（Model-Based Design，简写为MBD）逐渐完善，并成为系统化的开发方法。从特斯拉汽车公司的Roadster、洛克希德马丁公司的F35战斗机到NASA的猎户座飞船，基于模型的设计方法广泛地应用于民用和军工行业。 MBD方法之所以受到大家的欢迎，最主要的原因是系统复杂度的快速提升已经由量变引起质变。简单的算法、逻辑通过数百行代码即可实现，而复杂的产品代码行数已经达到上亿行的规模，一些复杂逻辑的布尔输入数量就高达120多个。如果依然采用手工写代码的方式进行开发，不仅需要大量的工程师从事开发工作，测试工作也是极其耗费成本的。 采用MBD方法的另一些原因是可以边做开发，边做验证。开发过程的每一个阶段的产品均是经过验证和确认的，确保传递到下一个开发阶段的工作产品质量，避免了后期的大量返工。 本文以多旋翼飞行器顶层逻辑算法代码为开发目标，介绍了基于模型的设计方法在多旋翼顶层逻辑开发过程中的应用。 1、需求分析及确认 从飞控手的角度来说，对多旋翼顶层逻辑的需求应该至少包含两个方面的内容：一是多旋翼应严格执行飞控手的指令要求，指哪儿打哪儿，使飞控手获得良好的飞行体验；二是多旋翼对于突发状况的处置能力，对于飞行过程中飞控手无法掌控的突发状况，多旋翼应能自主决策，消除安全隐患。 飞控手的需求转换为开发工程师能实现的工程需求，中间需要有“翻译”的过程，即需求分析。需求工程师通过对飞控手需求的分析，将用户需求转换为可实现的系统需求、硬件需求和软件需求。
图1. 需求分解 好的需求应该具有表1的特性。 表1. 需求的特性
基于上述原则，首先对多旋翼顶层逻辑进行分析，将多旋翼顶层逻辑需求分为功能需求及安全需求(需求部分可以具体参看“全权著.杜光勋等译. 多旋翼飞行器设计与控制.电子工业出版社, 2018.”)。功能需求用于实现飞控手正常的操控要求，如：起飞→手动飞行→返航→手动飞行→着陆等等，可经历的飞行模态及其转换关系如图2。
图2. 正常功能需求的状态转换逻辑 安全需求包含了多旋翼出现突发故障（如GPS信号丢失、磁罗盘故障、气压计失效）时的应急处置策略，不对人员造成伤害是最重要的要求，如当飞行过程中如果出现磁罗盘失效的突发情况，出于对人身安全的考虑，则多旋翼应该立即着陆，而非强行在飞控手的要求下返航。避免出现“乱飞”造成不可控的风险。下图是安全需求下的飞行模态及模态之间的转移逻辑。我们又将故障条件下的转移逻辑分为两种工况，分别是遥控器未失联条件下（图3）和遥控器失联情况下（图4）的模态切换逻辑，这样划分的原因是在遥控器未失联的条件下，飞控手仍然能手动控制多旋翼降落等。
图3. 遥控器未失联条件下的模态切换逻辑
图4. 遥控器失联条件下的模态切换逻辑 通过对需求的分析，建立了需求模型，框架如图5所示。利用对需求模型的仿真分析，发现了模型中存在的死逻辑（无法实现的需求），给我们对需求的分析提供一种思路。
图5. 需求分析模型 2、模型设计及验证 模型是基于模型设计的核心，基于需求搭建，用于生成代码。在整个基于模型设计的流程中起到承上启下的作用。一个好的模型应忠实地实现需求，同时生成的代码也符合规范。 四旋翼的顶层逻辑，适宜采用Stateflow进行模型搭建。结合对需求的分析和理解，确定多旋翼的飞行状态以及状态之间的转移条件。将多旋翼的模态划分为五个模态，分别为(模态部分可以具体参看“全权著.杜光勋等译. 多旋翼飞行器设计与控制.电子工业出版社, 2018”)： （1）地面待命模态：具备飞行条件，等待起飞命令； （2）手动飞行模态：接收飞控手指令，执行飞行任务； （3）返航模态：接收飞控手指令返航，或故障条件下自动返航； （4）着陆模态：接收飞控手指令着陆，或故障条件下自动着陆； （5）地面错误模态：不具备起飞条件。 建立的多旋翼顶层逻辑模型如图6。顶层逻辑模型有12个输入，其中包含人工输入指令，如：解锁或锁定指令，飞行模态的切换指令，油门指令等；同时也包括多旋翼飞行器的状态信息，如：各传感器的健康状态信息、电池电量信息等。基于当前所处飞行模态和传感器健康状态，做出模态转换的逻辑判断，并给相关输出变量赋值，作为不同飞控算法的选择信号。
图6.多旋翼顶层逻辑模型 在模型设计阶段需要完成三个部分的工作： （1）建立与需求的链接，尤其是多人协同开发的大型项目，对于需求版本和模型版本的管理显得尤其重要。通过建立需求与模型之间的双向追踪链接，可以给需求和模型“打个基线”，当变更发生后，通过check consist...可以快速准确地识别变更内容，发现模型与需求存在冲突不同步的问题，便于我们对模型或者需求进行对应的更新和检查，对于大型模型的开发和维护非常重要。需求与模型链接的建立过程如图7。
图7.模型与需求之间的链接建立过程 Matlab/Simulink Report Generator可以自动化地生成具有超链接的需求追溯性报告。如图8。
图8. 需求追溯性报告 （2）模型的规范性检查，基于模型的设计技术，代码是通过模型自动生成的，模型的规范性最终会体现到代码中。Matlab/Simulink内置了多个行业标准和规范（如DO-178C、MAAB），以判断模型是否符合行业规范。用户也可以根据自身需求制定符合要求的规范。
（3）模型验证，建模标准检查可以保证模型格式上的正确性，无法保证内容的正确性。而真正对内容正确性的验证需要在模型验证环节完成。模型的验证包含两种验证手段：一个是基于需求的验证，是一种通过动态仿真手段验证模型满足需求程度的方法；一种是基于形式化验证方法的静态验证手段，如果把基于需求的测试用例看作是一个个穷举的特殊例子，形式化方法则更像是一种证明手段。从数学的角度确认系统具备某种特性。 图10是基于需求验证方法搭建完的验证模型。首先在EXCEL中撰写基于需求的测试用例，并导入Signal Builder中，作为激励输入到顶层逻辑模型，观察顶层逻辑模型的输入，通过与期望输出的对比来确认模型设计的正确性。
图10.顶层逻辑的动态仿真验证模型 基于需求的验证方法需要对用例设计的好坏进行评估，通过覆盖度度量的方式，确认模型的覆盖情况，对于无法实现的模型覆盖，利用自动测试用例生成功能完成补充测试用例的生成，通过对补充测试用例的分析来进一步评估是否需要完善模型或者需求。 图11是基于形式化验证方法搭建完的验证模型。特性验证子系统的输入来自于顶层逻辑模型的输入和输出，但是并无具体的测试用例输入，基于需求的分析搭建特性验证子系统。特性的撰写有很多“窍门”，如：根据基于安全需求撰写验证特性一般更容易发现设计模型中的问题。还可以根据系统需求撰写特性。总之，特性可以基于某一条具体的需求撰写，也可以基于整体要求撰写。
图11. 顶层逻辑的静态形式化验证模型 形式化分析完成后生成特性分析报告，给出分析结论，对于证伪的模型特性，Simulink Design Verifier会给出反例以方便用户进一步的调试分析。首次利用Proving Properties功能进行特性证明时，发现在0.2~0.4s内多旋翼不处于任何一个飞行模态，这显然与特性3（特性3：在任意时刻，多旋翼至少应该有一个模态处于激活模态）不符。通过对反例的单步仿真分析发现了模型中的问题并顺利解决。
图12. 特性3的模型
图13. 特性3的排故过程 3、代码的生成和验证 3.1 自动代码生成 代码的自动生成是基于模型设计方法的优势之一，自动化地代码生成工具可以帮助用户将Simulink算法模型自动生成代码。而且，代码的生成过程同样具有极高的灵活性，通过对代码生成工具的“配置”——选择合适的代码生成模板和优先级。同样的模型可以生成满足不同行业规范、不同目标平台的代码。实现了不同硬件/不同平台之间算法的快速移植。 “模板”文件由扩展名为tlc文件组成。Embedded Coder软件内置了多个模板供用户选择，如可以生成嵌入式源代码的ert.tlc，满足汽车行业规范的autosar.tlc等等。用户也可以根据自己的需求开发自己的模板。代码生成的优先级则可以根据实际工程约束（如硬件资源限制、安全相关的考虑、需求的追溯性等）选择，从而生成不同风格的代码。
图14.代码生成前的模板选择及优先级目标设定 生成代码的同时，Embedded Coder软件会根据要求生成代码追溯性报告等。通过超链接的方式建立需求——模型——代码之间的一一对应关系，并建立需求追踪矩阵。 多旋翼顶层逻辑模型生成的顶层逻辑代码约1400行，不包含传感器健康状态的判断逻辑。下图是基于自动代码生成技术生成的多旋翼顶层逻辑代码。同时生成的还有子系统报告、代码接口报告、追溯性报告等。虽然自动生成的代码可读性较差（原则上并不需要读代码），但是需求与代码、模型与代码之间的追溯链接非常具有可读性。可以帮助用户快速的进行代码定位。生成代码的文件数量也同样可以根据不同的模式进行配置。整个过程体现出足够的“柔性”以满足不同的工程需求。
图15.自动生成的多旋翼顶层逻辑代码及报告 3.2 代码的验证 任何软件都有bug。同样，代码生成器和编译器也不例外。利用包含错误的工具生成或编译后的代码可能会存在致命缺陷。这是需要对生成的代码进行验证的原始需求。与模型的验证一样，代码的验证包含两部分验证内容： 一是动态仿真验证，即以仿真的形式验证代码与模型的一致性，目的是确保所生成的代码与模型是“一致的”，称之为等效性验证或基于模型的验证。这里我们并不需要直接验证代码与需求的一致性。其基本的逻辑在于：在模型的验证环节已经验证过模型是符合需求的，如果可以证明模型和代码在任意输入条件下的响应是一致的，则代码自然满足需求。 二是静态分析，通过代码自动比对、形式化分析方法验证代码是否存在运行时错误、数组访问越界等常规仿真方法难以发现的问题。 3.3 代码的动态仿真验证 从源代码的生成到部署到最终的控制器中，除了代码生成器、编译器之外，还有目标硬件参与。工程上为了便于定位问题所在，每次只允许引入一个变量。所以每次引入新的硬件、软件，原则上都需要进行验证。如图16，常用的代码验证方式有SIL测试、PIL测试和HIL测试。不同的测试方法，所搭建的测试环境和测试目的均有差异，总结如表2。
图16.不同的模型及代码测试方法 如做SIL测试的目的是验证代码与模型的等效性，即在任意相同输入的条件下，模型的输出与代码的输出应保持一致，故测试用例的设计应该具有足够高的模型覆盖度和代码覆盖度。可以利用Simulink Design Verifier的自动测试用例生成功能进行测试用例的生成，并符合一定的覆盖度标准（如100%的MCDC覆盖）。当然，重用Requirement based testing的用例得到的结果也应该保持一致。 表2. 测试架构的比较
不同测试方法的模型及软硬件环境配置结构如图17。
图17. SIL、PIL及HIL测试模式下的模型及硬件结构 3.4 代码的静态分析 代码的静态分析主要是对生成的代码进行审查和形式化分析，目的是识别出代码生成过程中和运行过程中可能产生的错误。Simulink Code Inspector是独立于Embedded Coder的代码审查工具。可以自动地对代码与模型进行比较分析以达到代码审查效果，并提供结构等效性及代码追溯性报告，因软件版本问题，本次多旋翼顶层逻辑算法开发过程中并未利用该软件进行代码审查。Simulink Code Inspector的基本分析原理如下图。
图18. Simulink Code Inspector代码审查原理 3.5 代码的形式化分析 有一些代码缺陷，如运行时错误、并发性问题、数据溢出错误等非功能性错误，很难通过构造测试用例发现。基于抽象解释（Abstract Interpretation）技术的代码形式化分析方法，能够识别代码中存在的上述缺陷，并生成分析报告。利用Polyspace Code Prover对所生成的多旋翼顶层逻辑算法代码进行分析，证明代码中不存在运行时错误等，代码覆盖率达到100%。
图19. 代码分析结果 4. 总结和后记 利用基于模型的设计方法，完成了多旋翼顶层逻辑算法的代码开发及验证工作。HIL平台环境下对部分需求进行了验证，从代码执行结果来看，与需求一致。达到了最初的目的。虽然采用基于模型的设计方法，整个开发和验证过程显得很复杂但实际难度并不大。最困难的地方在于需求的分析及验证，这是全部设计工作的起点。基于正确的需求搭建的模型和生成的代码才能实现正确的工程设计，因需求缺陷导致的返工将带来最大程度的成本损失，甚至有些缺陷无法修复。
NASA、柯林斯等航空航天、军工行业的巨头很早就开始了对需求的形式化验证，目的是提高需求分析的质量，发现复杂需求中的逻辑错误。目前形式化方法在控制系统开发过程中的需求分析阶段的应用不是很广泛，最主要的原因除了对需求重要性的认识不足，另外一个原因就是对需求进行形式化描述的语言较多、门槛较高。 在需求分析阶段，常见的形式化建模工具或语言有PVS、Isabelle、NuSMV、BLESS、AADL、Event-B、RSML-e；在模型设计阶段，常见的形式化分析工具有Simulink Design Verifier、SCADE、SPIN 、PROMELA、JKind；在代码实现阶段，常见的形式化分析工具有Astree、SCADE、Polyspace、Parasoft、Frama-C。 另外，基于模型的设计方法对于解决当前系统开发面临的问题也并非万能药，由于自动生成的代码与手工编写的代码相比在代码结构方面差异较大，对于习惯了传统调试方式的工程师来说，遇到问题后的排故可能会效率低下。其次，基于模型的设计方法依赖于被控对象模型的精确性，对于算法类的开发更是如此，所以对被控对象的精确建模也是需要解决的首要问题。 |
|
|
