安全攸关嵌入式系统的形式设计与分析｜CNCC Tutorial

本课程针对航天、核电、军工等领域安全攸关嵌入式系统的设计挑战，探讨基于形式化方法的建模、验证与代码生成核心理论和技术。

聚焦基于模型驱动的安全攸关嵌入式系统形式设计，提出了基于Simulink/Stateflow和混成CSP的能够描述嵌入式系统各种复杂行为的层次建模方法，既具图形建模的易用性又具形式模型的严格性；建立混成Hoare逻辑理论和验证系统，支持连续动态与时序性质的形式化规约与验证；提出不同层次模型之间的转换算法，包括从已验证的形式模型到代码的自动转换，通过互模拟证明确保语义一致性，从而保证代码生成的可靠性。建立了基于信号时序逻辑的系统运行时监测分析方法，保障了系统运行时安全性质。基于上述理论构建了原型工具MARS，并在探月工程"嫦娥三号"探测器控制软件及火星探测"天问一号"轨道控制模块等实现方法验证。 

参与者将能够：

目标1（了解形式化方法在安全攸关系统中的重要性和使用）

目标2（理解MBD的设计理念和整体流程）

目标3（深入理解形式验证和可靠代码生成的基本方法）

目标4（掌握基于时态逻辑的系统运行时验证方法）

1. 安全攸关嵌入式系统形式设计与分析介绍

总体介绍模型驱动的安全攸关嵌入式系统形式设计与分析方法。

2. 基于AADL和Simulink/Stateflow的协同建模与分析方法

安全攸关信息物理融合系统（CPS）的设计需要对其物理环境、软件功能以及系统体系结构进行协同建模与分析，然而现有的大多数建模方法难以统一兼顾这三个关键的设计方面。AADL在体系结构与硬件平台建模方面具有优势，但是在物理与软件行为的建模方面能力较弱；相比之下，Simulink/Stateflow在刻画连续物理行为、离散软件逻辑以及它们之间复杂交互方面表现出强大能力，却在系统架构与硬件平台的建模能力上存在不足。针对这一问题，我们将AADL与Simulink/Stateflow进行结合，发挥二者在架构与行为建模上的互补优势，并通过将这种图形的组合模型转换为形式化的混成通信顺序进程（HCSP），赋予其严格的形式语义，从而构建了一个支持协同建模、仿真分析与形式验证的综合框架，为复杂CPS的设计与可靠性保障提供了理论方法与技术支持。

3. 基于混成霍尔逻辑的混成系统验证

近年来，混成系统的演绎验证因其强大能力和可扩展性而日益受到关注，其中强大的混成系统规约逻辑是重要基础。混成系统通常自然地建模为相互通信的并发进程，然而，现有的规约逻辑难以处理此类模型。本报告针对混成通信顺序进程（Hybrid Communicating Sequential Processes, HCSP）提出了一种规约逻辑和证明系统，成为混成霍尔逻辑。HCSP 通过引入常微分方程（ODE）和中断机制，扩展了 CSP（通信顺序进程），用以建模连续演化与离散计算之间的交互。由于 HCSP 包含丰富的代数算子，复杂的混成系统可以方便地以类似代数的组合方式进行建模。混成霍尔逻辑由微分方程的一阶理论（First-Order Theory of Differential Equations, FOD）构成，并结合了记录通信、就绪状态和连续演化的迹断言。我们证明了该逻辑相对于 FOD 的连续相对完备性，以及在离散意义下可任意精度逼近连续行为意义上的离散相对完备性。最后，我们在定理证明器 Isabelle/HOL 中实现了上述逻辑，并通过验证实际案例展示了该逻辑的表达能力和实用性。

4.从形式模型出发的可靠代码生成

本文报告基于混成通信顺序进程（HCSP）形式模型自动生成可验证C代码的关键技术，重点解决同步通信机制转换、常微分方程（ODE）离散化及通信中断处理的挑战。针对HCSP同步通信语义与POSIX C线程异步模型的差异，提出利用互斥锁和条件变量实现同步通信的映射方法；通过时间离散化处理ODE连续演化并支持通信中断机制，确保数值计算与实时响应的可靠性。为严格证明代码生成正确性，建立POSIX C线程子集的形式语义，并基于近似互模拟理论建立代码生成正确性验证框架，定义时间与数值双误差指标，在鲁棒性条件下证明HCSP模型与生成代码的等价性。该工作实现融合连续动态、并发交互的混成系统形式模型到C代码的可验证转换，为高可信嵌入式系统开发提供基础。

5.基于信号时序逻辑的系统监测与分析

运行时监测是保障系统部署后运行时满足需求性质的关键技术。安全攸关嵌入式系统不仅涉及时序性质，往往还涉及复杂的实时性质和空间性质。本报告将介绍目前基于信号时序逻辑（Signal Temporal Logic, STL）的安全攸关信息物理融合系统复杂性质监测方法，并分析基于传统STL鲁棒语义监测所引起的信息屏蔽这一公认问题。接下来，本报告介绍最新提出的STL因果语义以及基于该语义的运行时系统监测方法，该方法有效的解决了信息屏蔽这一难题。