摘要：机电一体化系统是一类信息-物理系统，其日益增加的复杂性使得其验证和确认变得越来越困难，同时其需求也变得更加具有挑战性。本文介绍了一种基于模型设计、联合仿真和形式化验证的开发方法。本文的目的是展示该方法在工业环境中的适用性。一个应用案例研究来自精密伺服电机领域，在该领域中，形式验证已被用于为电机控制器的设计参数找到可接受的取值区间，并通过联合仿真进一步探索以找到最优值。报告的结果表明，该方法已成功应用于案例研究，通过稳定性的形式化验证、可接受参数范围的形式化识别和自动设计空间探索，增强了当前模型驱动的开发过程。

1.简介

       机电一体化（以及更普遍的网络物理）系统的复杂性不断增加，应用领域不断扩大，并且需要越来越高水平的可靠性和性能。因此，通过仿真和测试进行系统验证应辅以严格的分析和验证方法，从而实现正式的循环验证开发过程。

       这个概念是这项工作中提出的开发过程的基础。该过程假定一个高级规范，通常是自然语言或一些半正式语言，从中派生一组子模型。子模型可以表示系统的不同结构部件（例如，车辆的发电厂和齿轮系）或不同的方面（例如，电机的电磁和机械物理）。每个子模型都可以由不同的领域专家开发，他们使用适合每个领域的建模语言和工具。协同仿真（与传统的单片仿真相反）是对独立开发的异构子模型的协调仿真。

       建模语言通常面向仿真。它们可能基于不同的概念框架，例如，Simulink 的信号流和 Modelica 的方程，其支持环境提供了一个模拟器。但是，它们对核查的支持是有限的，如果有的话。在建议的开发过程中，还构建了可验证的模型。如果模型是用面向验证的语言编写的，并在提供自动或半自动验证工具的环境中实现，则该模型是可验证的。在这项工作中，我们建议使用抽象的数学规范作为面向模拟和可验证模型的基础。   

       并非所有子模型都需要正式验证，因为系统的许多方面都是众所周知的，并且可以使用经过充分验证和可靠的技术进行设计。对于系统中更具创新性的组件或方面，特别是控制系统，需要进行形式验证。在这种情况下，协同仿真特别方便。

       在这项工作中，我们提出了形式验证，协同仿真和设计空间探索（DSE）的应用，以实际感兴趣的案例研究，永磁同步电机的伺服驱动器。伺服驱动器是网络物理（更具体地说，机电一体化）系统，因为它们结合了物理和算法组件。之所以选择本案例研究，是因为伺服驱动器是特别感兴趣的系统，因为它们应用于工业自动化、工业机器人和汽车应用的所有领域。然而，这项工作的贡献不是一种新的无刷电机控制算法，而是提出了机电一体化系统背景下的控制算法验证程序。本案例研究中使用的算法之前由两位作者设计，并使用经典的软件在环（SIL）程序进行验证。

       本文旨在展示如何在设计过程中引入形式验证和协同仿真，以提高对系统符合要求的信心，并帮助设计人员做出基于经验法则和试错程序的选择。特别注意控制算法参数的调整，在经典的SIL方法中，其值只能通过进行多次仿真来选择。在本文中介绍的方法中，使用形式化方法来定义这些值的可接受范围，并使用基于协同仿真的DSE系统地探索参数空间。

       在本节的其余部分，介绍了关于机电一体化系统开发的大量文献的一小部分参考资料，按它们与这项工作的主要主题（即建模和仿真，协同仿真和形式方法）的相关性进行分组。

       关于建模和仿真，系统模型通常使用基于块的语言构建，这些语言将系统描述为功能块的集合，每个功能块代表一个可能复杂的数学运算，并通过数据流相互连接。这些块具有视觉表示形式，但它们的语义是在底层文本语言中定义的。然后通过运行测试场景对模型进行仿真，成功的运行增强了对设计正确性的信心。然而，详尽的测试是不可能的，系统的高可靠性需要高水平的测试覆盖率。

       MATLAB/Simulink 套件是支持基于块的建模环境的一个典型示例。在其大量面向应用的工具箱中，基于状态机形式的Stateflow工具箱可用于对混合系统进行建模，其特征在于具有有限数量的不同操作模式，并且在每种模式下，系统根据时间连续定律演化。

       近年来发表的机电系统仿真文献中可以引用几篇论文。Dell'Amico 和 Krus 使用单片仿真和硬件在环 （HIL） 仿真来设计电动液压助力转向系统。在 HIL 仿真 中， 控制器 和 车辆 轮胎 模型 都 在 软件 中， 而 机械 和 液压 部件 则 组装 在 由 方向 盘、 齿轮齿条、 泵 和 气 门 以及 相关 传感器 和 执行 器 组成的 测试 台 中。

       Orszulik和 Gabber提出了 Simulink 和有限元工具包 Abaqus 之间的接口，面向智能结构的仿真，即形状可以通过控制刺激（例如电场）修改的实体。作为案例研究，使用Abaqus模拟由压电传感器和执行器控制的铝梁，而使用Simulink模拟控制器，以研究振动行为。

       Isermann 等人讨论了 HIL 仿真在 发动机 控制 系统 开发 中 的 作用， 并 报告 了 柴油 机 与 真实 喷射 泵 以及 真实 的 发动机 和 泵 控制 单元 交互 的 仿真。

      关于协同模拟，Gomes等人最近发表了一项广泛的调查，根据各种作品中采用的计算模型提供了基本概念和文献分类法的定义：离散事件，连续时间和混合，即两者的混合。

       Hadas 等人 使用ADAMS 中的多体动态系统和 Simulink 中的控制器的协同仿真来分析各种类型的工业机器人。

       Sadovykh等人在一篇论文中讨论了SysML语言的使用，其中SysML模型定义了供暖，通风和空调系统的高级架构，该系统由在20-sim中建模的各种物理子系统和在VDM中建模的控制器组成。后者具有数字（事件驱动）组件，通过在操作模式（加热或冷却）之间切换来响应用户输入和温度变化，以及连续时间组件，在每种模式下使用PID算法控制温度。

       Foldager等人介绍了无人驾驶割草机开发的案例研究，描述了实验和仿真之间的相互作用，以研究物理参数，设计参数和操作条件。首先通过实验确定两个物理参数，然后采用协同仿真为控制器的设计参数选择最优值，并通过现场测试验证。最后，协同仿真再次用于评估不同速度下的系统行为。该工厂已在 20-sim 中模拟，控制器在 VDM 中进行了模拟。

       从形式方法的文献中，我们可以引用Giese等人，他们开发了UML状态图和组件的正式扩展，使开发人员能够将网络物理系统建模为混合自动机并支持子系统的模块化组合。

       Lindahl等人使用UPPAAL进行模型检查，以验证齿轮箱控制器，建模为定时自动机网络，满足不同类型的要求，包括性能和时间限制。

       Cimatti等人开发了HyComp，这是一种基于SMT的工具，用于验证混合自动机的网络。该工具还可以合成设计参数。

       KeYmaera X交互式定理证明器是由Fulton等人引入的。在这种环境中，连续时间行为用差分动态逻辑的语言表示。

      另一个定理证明环境是原型验证系统，它与KeYmaera不同，它使用通用的高阶逻辑。这种环境已被用于许多应用领域，例如医疗和控制系统，将在2.1节中更广泛地描述。

      下面列出了其他利用形式化验证方法的有趣作品。在中，作者提出了对汽车网络安全领域最新技术的回顾，评估了车载硬件仿真方法和形式验证方法的最佳组合，以涵盖特殊情况。在中，作者提出了一种控制配电系统的策略，以最大限度地减少电费并满足用户的舒适度限制。他们使用 UPPAAL 环境通过模型检查进行建模和验证。

       这项工作的组织如下：第2节提供了定理证明和协同仿真的背景信息;第3节介绍了本文中介绍的方法;第4节以无刷电机控制器的设计为例，以及形式验证的应用，第5节包含协同仿真和DSE结果，第6节总结本文。

2.PVS和协同仿真的背景

      本节介绍支撑所提议过程的两种主要技术：使用高阶逻辑进行验证，以及使用协同仿真进行验证和设计空间探索。验证由原型验证系统（PVS）和INTO-CPS框架的协同仿真提供支持。

2.1. PVS 环境

       总结来看，感知层主要负责的是采集物品相关信息，这是物联网发展运行的基础，主要是由摄像设备等能 胜任此任务的设备组成的[1]。

       PVS是一个基于类型化高阶逻辑语言和相继微积分演绎系统的交互式定理证明器环境，具有丰富的可扩展类型系统。

PVS理论是“名称理论开始”和“结束名称”语句之间的定义和公式的集合。用户可以定义类型、常量、变量和函数。公式是一个命名的逻辑语句，它可以是一个公理（用 AXIOM 关键字声明）或一个定理（用 THEOREM、LEMMA 等关键字声明）。公理被视为已证明，而定理则使用基于相继演算的大量证明器命令进行证明。PVS 语言具有算术和逻辑类型以及结构化类型，包括记录类型和谓词子类型。例如，特定电机的规格可能包括物理大小的定义，可能具有可接受的值范围：

       上述定义声明电流是具有非负实值（nnreal）的幅度，电阻取范围内的非负值，等等。类型阻力是谓词子类型的一个示例，通过向其超类型添加约束来定义。然后，可以将电动机的概念建模为包含通用电动机参数的记录类型。然后将特定电机建模为类型 electric_motor 的实例，并指定其参数值：

3.验证与协同仿真一体化的开发流程

      数学模型是系统的数学规范，其他两个模型就是从中派生出来的。该模型由三部分组成：（i）工厂动力学的定义，（ii）控制算法，以及（iii）系统要求。每个部分，依次。可以分解为子模型，反映系统的结构。

      仿真模型是工厂动力学和控制算法的可执行规范。此规范通常使用基于块的语言（如 Simulink）构建为整体模型，但协同仿真提供了对不同子模型使用不同语言的便利。当一个模型已经可用于一个子系统（例如，工厂）并且要重新创建另一个子系统（例如，控制器）的模型时，这特别有用。

       逻辑模型是将数学模型翻译成适合验证的语言。在目前的工作中，逻辑模型已经用PVS高阶逻辑语言表示。在这种语言中，逻辑模型可以结构化为一组理论，每个理论对应于数学模型的不同子模型。工厂和控制算法的数学模型直接转化为PVS公理和定义，而需求则成为定理，以证明理论。

       仿真流程使用工厂和控制部件的可执行模型从协同仿真活动中收集实验结果。在这个开发阶段，控制部分设计是软件设计，因此其可执行模型可以使用软件规范语言方便地构建，或者直接使用实现语言构建，而工厂则使用物理建模语言构建。选择协同模拟作为模拟方法，以适应不同的形式。

       验证流使用逻辑模型来证明是否满足要求。证明活动作为交互式定理证明进行，如第 2.1 节所述：定理证明器显示目标，即要证明的语句，用户发出简化目标或将其分解为子目标的命令。重复此操作，直到初始目标简化为一组足够简单的子目标，由定理证明器自动证明，或者直到没有命令可以简化某些子目标，在这种情况下，定理不被验证。然后，证明活动导致每个定理的验证或未验证的判决。作为副产品，验证可能会导致定义设计参数的约束，这些约束被反馈到数学模型并传播到仿真和验证流程中，如图2所示。

       这两个工作流合并到评估活动中，其中包括根据证明和协同模拟的结果采取行动。如果证明或仿真结果为阴性，则审查逻辑和仿真模型并相互比较。比较逻辑模型和仿真模型很有用，因为这两个模型虽然来自相同的数学规范，但都建立在不同的概念框架之上，任何一个都可以阐明另一个的问题。然后将这两个模型与数学模型进行比较，以确保其被正确翻译。在下文中，我们假设这三个模型是一致的。作为评估活动的结果，数学模型将更新，更新将传播到两个并行流。

       在仿真结果为负的情况下，可以设计测试来隔离规范中存在问题的部分，并且可以相应地更改数学模型。

       否定验证结论是由逻辑规范中的不一致引起的，例如错误、不完整或矛盾的假设或要求。没有机械程序可以查明这种不一致之处，但交互式定理证明过程通常会指导开发人员寻找不一致之处。通常，失败的证明会卡在试图证明错误的陈述中，其分析揭示了规范中的概念问题。

       根据项目上下文，可以更改规范的不同部分。如果要求和工厂是固定的，显然只能对控制部分采取行动。否则，可以考虑对工厂甚至要求进行修改。例如，可以选择具有不同特性的组件，或者可以放宽性能要求。

根据需要迭代上述循环，直到结果令人满意。在这种情况下，设计空间探索活动开始。DSE包括尝试不同的设计参数组合，以找到最大化某些品质因数或最小化某些成本的参数。在这项工作中提出的方法中，设计空间由参数值的间隔组成，这些参数值已被正式和实验证明可以满足要求。

      DSE 选择的设计参数值用于生成所有模型的最终版本，为进一步的开发阶段做好准备，例如 HIL 仿真和实现。

      上述架构的许多变体是可能的。特别是，逻辑规范既可以验证又可执行，然后用于验证和仿真。另一个变体是并行部署验证工具和自动化数学工具，如以下各节所示。

      此外，可以指出的是，本文中介绍的基于软件的流程可以包含在一个完整的流程中，其中使用HIL阶段来验证仿真。