一种基于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建模与验证方法，其特征在于，包括如下步骤：步骤1：对混成系统描述语言HYSDEL进行扩展，得到在CPS‑ADL平台中对CPS行为建模的语言E‑HYSDEL；在HYSDEL声明部分INTERFACE中添加时间的声明，这部分时间属性的声明包括两部分：连续状态变化的连续时间变量t_x以及输入控制量的时间t_u或T_s，其中连续状态变化的时间t_x表示当前系统物理实体的时间，t_u表示连续的输入控制量u的时间，T_s则表示离散的输入控制量U的时间戳；步骤2：给出混合程序模型HPM的形式化定义：HPM＝(PD，VD，PC，SHPS)其中，PD表示参数声明；VD表示动态变量声明；PC表示前置条件，也就是系统运行前各数据满足的条件；SHPS表示混合程序中包含的子混合程序模型SHP集合，每个SHP的形式化定义如下：SHP＝(MS，DTS，CTS)MS(Mode Set)表示离散状态模式的集合；DTS表示离散状态迁移集合，即Mode之间的迁移；CTS表示连续迁移集合，描述单个Mode内部的连续变化过程；步骤3：建立CPS‑ADL模型元素与HPM元素之间的转换规则：CPS‑ADL各个模型元素由E‑HYSDEL的不同函数进行描述，建立两种模型之间的元素转换规则是给出CPS‑ADL模型中的函数与HPM中各元素之间的映射关系，按照内容不同，把转换规则分为数据转换规则、结构转换规则、模式转换规则、迁移转换规则和约束转换规则五类；本步骤中所述数据转换规则、结构转换规则、模式转换规则、迁移转换规则和约束转换规则具体为：数据转换规则：将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；步骤4：在CPS‑ADL平台上采用扩展的混成自动机描述语言E‑HYSDEL对CPS进行建模；步骤5：利用步骤3中建立的两种模型元素间的转换规则，根据步骤4中建立的CPS模型生成HPM，然后根据HPM得到混合程序；步骤6：将需要验证的CPS属性描述为符合微分动态逻辑的属性约束公式，进行规约；步骤7：根据定理证明器KeYmaera的输入格式要求，将步骤5中得到的混合程序和步骤6中得到的属性约束公式格式化，最后生成KeYmaera的输入代码；对照HP表示法和KeYmaera输入表示法，替换HP中运算符、标识符语法元素，添加辅助标识，调整构成元素的位置和结构；步骤8：在定理证明器KeYmaera中打开步骤7中得到的输入代码文件，进行验证，得到验证结论。