一种基于CPS-ADL模型向混合程序转换的CPS建模与验证方法

摘要

本发明公开了一种基于CPS-ADL模型向混合程序转换的CPS建模与验证方法，主要用于处理CPS建模与属性验证问题，其特征在于：在CPS-ADL平台上采用扩展的混成系统描述语言E-HYSDEL对CPS进行建模；给出HP模型的形式化定义HPM，并在满足模型转换一致性的前提下建立CPS-ADL模型元素与HP模型元素之间的转换规则；基于这些转换规则，将具体CPS的模型描述代码自动转换为混合程序；按照定理证明器KeYmaera的输入格式，由混合程序和以动态微分逻辑描述的系统属性公式生成KeYmaera的输入文件；在KeYmaera中打开输入文件，进行推理验证。本发明细化了基于CPS-ADL模型向HP转换的方法和机制，实现了CPS-ADL模型元素向HP模型元素转换的规则。

说明书

技术领域

本发明属于通讯技术领域，涉及一种基于CPS-ADL模型向混合程序转换的CPS建模与 验证方法。

背景技术

信息物理系统（Cyber Physical System,CPS）通过在物理设备中嵌入感知、通信和计算 能力，实现对外部环境的分布式感知、可靠数据传输和智能信息处理，并通过反馈机制实现 计算实体对物理设备的实时监测与控制。CPS应用领域十分广泛，包括智能交通系统，远程 医疗，智能电网，航空航天等。

CPS的实时性、安全性和可靠性等属性能否满足要求往往是其在关键领域应用的前提。 模型分析和验证技术可以在系统设计阶段确定CPS的属性是否满足实际应用需求，在确保 系统安全性、可靠性和实时性等方面起到了关键作用，同时也有效降低了系统开发风险。

近年来，模型检验和定理证明等形式化方法越来越多地被应用于CPS分析验证中。模 型检验的主要优点是自动化程度高，广泛应用于离散系统验证，但CPS通常为混成系统， 既有离散状态迁移，也有动态连续变化过程，系统的状态是无穷的。从实际应用角度看，定 理证明的思路更适合于复杂CPS的属性分析与验证。其中，Platzer提出的微分动态逻辑 （Differential Dynamic Logic，dL），语法严谨、语义清晰，在安全相关系统的分析验证中应用 较为广泛。

KeYmaera是一种支持微分动态逻辑的定理证明工具，自动化程度较高，适合于像CPS 这样的复杂混成系统的分析，已被成功用于空中交通管制、高速列车系统和汽车自动巡航控 制系统中，以减少潜在的危险隐患。

系统建模是对其属性进行分析验证的前提。在系统建模阶段，为了使模型直观易懂，通 常采用通用图形化的建模工具。微分动态逻辑的操作模型为混合程序（Hybrid Programs， HP），使用HP对CPS所建的模型便于验证，但模型表现形式比较抽象，在CPS的设计过 程中难以方便有效地使用。

CPS-ADL是图形化的CPS建模、分析与仿真的综合集成软件平台。该平台对架构分析 与设计语言（Architecture Analysis and Design Language，AADL）语言进行扩展，实现对CPS 静态结构建模；对混成系统描述语言HYSDEL进行扩展，实现对CPS动态行为建模。

图1给出了描述CPS模型的E-HYSDEL代码的组成结构。程序代码主要由两部分组成： 第一部分为INTERFACE，用于声明系统中所有的变量和参数，包括STATE,INPUT,OUTPUT 和PARAMETER四个函数，分别声明系统的状态、输入、输出和参数列表，并接受编译器 规则类型的检测；第二部分为IMPLEMENTATION，由各个定义变量间关系的专用函数构成， 包括AUX、AD、DA、LOGIC、CONTINUOUS、LINEAR以及AUTOMATA等函数，简单 介绍如下：

1）AUX函数：定义辅助连续变量和逻辑变量；

2）AD函数：允许根据连续事件定义的布尔变量；

3）DA函数：该函数是利用if-then-else语句，根据布尔变量定义连续变量；

4）LOGIC函数：允许定义任意布尔变量，特别是布尔变量模式选择器；

5）CONTINUOUS函数：这部分以微分方程或者差分方程来描述线性动态变化的物理规 律；

6）LINEAR函数：允许以连续变量分段函数形式来定义辅助连续变量；

7）AUTOMATA函数：该函数以布尔函数x′_b（k)=f_B（x_b（k），u_b（k），δ_e（k））的形式定 义有限状态机FSM的状态转换方程；

8）MUST函数：该函数可以指定连续变量和布尔变量的约束，线性约束和布尔准则；

9）OUTPUT函数：定义输出向量y=[y_r，y_b]^T的静态线性和逻辑关系，

在实际CPS建模过程中，根据需要实现其中的部分函数。

发明内容

本发明的目的在于克服上述技术存在的缺陷，提供一种基于CPS-ADL模型向混合程序 转换的CPS建模与验证方法，将CPS-ADL的建模能力与HP的形式化验证能力结合起来， 提出了一种基于CPS-ADL模型向HP转换的CPS建模与验证方法，主要用于处理CPS建模 与属性验证问题。细化了基于CPS-ADL模型向混合程序转换的方法和机制，实现了 CPS-ADL模型元素向HP模型元素转换的规则。

其具体技术方案为：

一种基于CPS-ADL模型向混合程序转换的CPS建模与验证方法，包括如下步骤：

步骤1：对混成系统描述语言HYSDEL进行扩展，得到在CPS-ADL平台中对CPS行为 建模的语言E-HYSDEL；

在HYSDEL声明部分INTERFACE中添加时间的声明，这部分时间属性的声明包括两 部分：连续状态变化的连续时间变量t_x以及输入控制量的时间t_u或T_s，其中连续状态变化 的时间t_x表示当前系统物理实体的时间，t_u表示连续的输入控制量u的时间，T_u则表示 离散的输入控制量U的时间戳；

步骤2：给出混合程序模型HPM（Hybrid Program Model）的形式化定义：

HPM=（PD，VD，PC，SHPS）

其中，PD（Parameters Declaration）表示参数声明；VD（Variables Declaration）表示动 态变量声明；PC（Precondition）表示前置条件，也就是系统运行前各数据满足的条件；SHPS （Sub Hybrid Program Set）表示混合程序中包含的子混合程序模型SHP集合，每个SHP的 形式化定义如下：

SHP=（MS，DTS，CTS）

MS（Mode Set）表示离散状态Mode（模式）的集合；DTS（Discrete Transition Set）表 示离散状态迁移集合，即Mode之间的迁移；CTS（Continues Transition Set）表示连续迁移 集合，一般描述单个Mode内部的连续变化过程；

步骤3：建立CPS-ADL模型元素与HPM元素之间的转换规则：

CPS-ADL各个模型元素由E-HYSDEL的不同函数进行描述，建立两种模型之间的元素 转换规则主要是给出CPS-ADL模型中的函数与HPM中各元素之间的映射关系。按照内容 不同，把转换规则分为数据转换规则、结构转换规则、模式转换规则、迁移转换规则和约束 转换规则五类；

步骤4：在CPS-ADL平台上采用扩展的混成自动机描述语言E-HYSDEL对CPS进行建 模；

步骤5：利用步骤3中建立的两种模型元素间的转换规则，根据步骤4中建立的CPS模 型生成HPM，然后根据HPM得到混合程序；

步骤6：将需要验证的CPS属性描述为符合微分动态逻辑（dL）的属性约束公式，进行 必要的规约；

步骤7：根据定理证明器KeYmaera的输入格式要求，将步骤5中得到的混合程序和步 骤6中得到的待验证属性公式格式化，最后生成KeYmaera的输入代码；

对照HP表示法和KeYmaera输入表示法，替换HP中的运算符、标识符等语法元素， 添加必要的辅助标识，调整构成元素的位置和结构；

步骤8：在定理证明器KeYmaera中打开步骤7中得到的输入代码文件，进行验证，得 到验证结论。

进一步优选，步骤3中所述数据转换规则、结构转换规则、模式转换规则、迁移转换规 则和约束转换规则具体为：

数据转换规则：将INTERFACE部分的INPUT函数、INTERFACEOUTPUT函数和AUX 函数映射为HPM中的元素VD；将PARAMETER函数映射为HPM中的元素PD；

结构转换规则：将STATE函数中的每个状态变量转换为一个SHP，从而STATE函数映 射为SHPS；

模式转换规则：从AD函数、DA函数、LOGIC函数、COUTINUOUS函数、LINEAR 函数和AUTOMATA函数映射各SHP中的MS，一般地，布尔型变量对应两个Mode，连续 型变量对应的Mode数量与其函数式的分段数量相等，每个Mode的基本属性包括名称、类 型等，对于连续型变量对应的Mode，还要描述变量在当前Mode下的变化公式，进一步， 根据变量间的依赖关系将Mode加入到相应HPM的MS中，同一个Mode若与多个状态变 量有直接或间接依赖关系，则可加入到多个HPM的MS中，若两个Mode分别是某个迁移 的源节点和目标节点，则加入到相同的HPM中；

迁移转换规则：从AD函数、DA函数、LOGIC函数、COUTINUOUS函数、LINEAR 函数和AUTOMATA函数映射各SHP中的DTS和CTS，一般地，分支结构的一个分支对应 一个迁移，迁移规则描述包括源节点、目标节点、迁移触发条件和迁移输出，根据迁移的源 节点和目标节点，将迁移加入相应的SHP；

约束转换规则：将MUST函数以及INPUT函数和STATE中对变量取值的限定条件转换 为HPM中的PC。

与现有技术相比，本发明的有益效果为：本发明基于CPS-ADL模型向混合程序转换的 CPS建模与验证方法主要用于处理CPS建模与属性验证问题。细化了基于CPS-ADL模型向 混合程序转换的方法和机制，给出了HP的形式化定义，实现了CPS-ADL模型元素向HP 模型元素转换的规则。

附图说明

图1是E-HYSDEL的语法结构；

图2是本发明基于CPS-ADL模型向混合程序转换的CPS建模与验证方法的流程图

图3是KeYmaera输入格式；

图4是室温控制系统示意图；

图5是室温控制系统状态图；

图6是HP表示符号与KeYmaera表示符号对照关系图。

具体实施方式

下面结合附图和具体实施例对本发明的技术方案作进一步详细地说明。

参照图2，本发明基于CPS-ADL模型向混合程序转换的CPS建模与验证方法，包括以 下步骤：

按步骤1，在HYSDEL的声明部分INTERFACE中添加时间的声明，这部分时间属性的 声明包括两部分：连续状态变化的连续时间变量t_x以及输入控制量的时间t_u或T_s。其中连 续状态变化的时间t_x表示当前系统物理实体的时间，即与物理世界的时间是一致的；而系 统的输入控制量有可能是连续输入量u，也有可能是离散的输入控制量U，因此需要对不 同的输入类型声明不同的时间属性，t_u表示连续的输入控制量u的时间，T_u则表示离散的 输入控制量U的时间戳，t_u或T_x与t_x可能会不一致，这正是由于控制指令到达该行为过 程中的时间延迟，即控制指令传输的时延ΔT_u=t_x-t_u或ΔT_u=t_x-T_u。假定这些时间参 数均属于系统状态或输入控制量的一种属性，将这类时间属性直接定义在相应状态量或输入 量的内部即可。

按步骤2，给出混合程序模型HPM的形式化描述形式：

HPM=（PD，VD，PC，SHPS）

其中，PD（Parameters Declaration）表示参数声明；VD（Variables Declaration）表示动 态变量声明；PC（Precondition）表示前置条件，也就是系统运行前各数据满足的条件；SHPS （Sub Hybrid Program Set）表示混合程序中包含的子混合程序模型SHP集合，每个SHP的 形式化定义如下：

SHP=（MS，DTS，CTS）

MS（Mode Set）表示离散状态Mode（模式）的集合；DTS（Discrete Transition Set）表 示离散状态迁移集合，即Mode之间的迁移；CTS（Continues Transition Set）表示连续迁移 集合。

按步骤3，建立CPS-ADL模型元素与HPM元素之间的转换规则，即建立两种模型之间 的元素转换规则，主要是给出CPS-ADL模型中的函数与HPM中各元素之间的映射关系。 转换规则分为数据转换规则、结构转换规则、模式转换规则、迁移转换规则和约束转换规则 五类。

按步骤4，在CPS-ADL平台上采用扩展的混成自动机描述语言E-HYSDEL对如图4所 示的室温控制系统进行建模。

室温控制是一个典型的CPS应用。在同一个房间的不同位置有两个人，房间装有加热 器、空调和窗户，这些装置都可以对房间内的温度产生影响。T1表示第一个人所处位置的 温度，T2表示第二个人所处位置的温度，Tamb表示室外的环境温度，Uhot表示加热器工作 时的能流，Ucold表示空调工作时的能流。当温度T1超过Thot1时，第一个人会感觉太热， 将打开空调；当温度T1低于Tcold1时，他会感觉太冷，将打开加热器。当温度T2超过Thot2 时，第二个人会感觉太热，此时若第一个人不感觉冷，他将打开空调：当温度T2低于Tcold2 时，他会感觉太冷，此时若第一个人不感觉热，他将打开加热器。其他情况下加湿器和空调 都是关闭的。房间的窗口总是打开的。图5进一步描述了该系统中各组成部分的状态变化。

已知T1和T2的变化规律可以用以下微分方程表示：

T1′=-alpha1*（T1-Tamb）+k1*（uhot-ucold）

或T1=TI+Ts*（-alpha1*（T1-Tamb）+k1*（uhot-ucold））

T2′=-alpha2*（T2-Tamb）+k2*（uhot-ucold）

或T2=T2+Ts*（-alpha2*（T2-Tamb）+k2*（uhot-ucold））

式中，uhot、ucold分别表示任意时刻加热器和空调的的能流。各系数的取值为：Ts=0.5， alpha1=1，alpha2=0.5，k1=0.8，k2=0.4，Thot1=30，Tcold1=15，Thot2=35，Tcold2 =10，Uc=2，Uh=2。

需要验证结论是为当10≤Tamb≤30，初始状态为35≤T1,T2≤40时，状态10≤T1,T2 ≤15是不可达的。

按照图1所示E-HYSDEL的语法结构，在CPS-ADL中对室温控制系统建模中需要实现 其中的STATE函数、INPUT函数、OUTPUT函数、PARAMETER函数、AUX函数、AD函 数、DA函数和CONTINUOUS函数。所得的E-HYSDEL代码如下：

按步骤5，将上述CPS-ADL模型转换成对应HP模型。

由数据转换规则，得到HPM中VD和PD：

VD={（R,T1），（R，T2），（R,Tamb），（R,uhot），（R,ucold），（R，t）｝

PD={（Ts,1），（alpha1，1），（alpha2,0.5），（k1，0.8），（k2,0.4），（Thot1,30），

（Tcold1，15），（Thot2,35），（Tcold2，10），（Uc，2），（Uh,2）｝

由约束转换规则，得到HPM中PC：

PC={（Tamb，>=，10），（Tamb,<=,30），（T1，>=，35），（T1，<=，40），（T2，>=，35），（T2，<=，40）}

由结构转换规则，得到HPM中的SHPS：

SHPS={S1,S2｝

由模式转换规则和迁移转换规则，进一步得到S1和S2两个SHPS集合成员的MS、DTS 和CTS。

根据HPM，得到描述室温控制系统混合程序如下：

按步骤6，需要验证的属性约束条件表示为。

利用dL公式ω→[heatcool*]Φ进行系统属性规约。其中，ω为初始条件，Φ为需要 验证的结论：

ω≡（Tamb≥10∧Tamb≤30）∧（T1≥35∧T1≤40）∧T2≥35∧T2≤40）

按步骤7，将步骤5中得到的HP及步骤6中得到的属性约束条件转化为符合KeYmaera 输入格式要求的文件，目标文件的格式如图3所示，具体内容如下：

按步骤8，在定理证明器KeYmaera中打开步骤7中得到的输入代码文件，进行验证。

以上所述，仅为本发明较佳的具体实施方式，本发明的保护范围不限于此，任何熟悉本 技术领域的技术人员在本发明披露的技术范围内，可显而易见地得到的技术方案的简单变化 或等效替换均落入本发明的保护范围内。