基于HybridUML向微分代数程序转换的CPS建模与验证方法

摘要

本发明提出了一种基于HybridUML向微分代数程序转换的CPS建模与验证方法，实现了由HybridUML模型向DAP的转换，并依据微分代数动态逻辑(Differential-Algebraic Dynamic Logic，DAL)推理规则对CPS实例进行验证。该方法使用HybridUML对CPS进行建模，将其转换成DAL的操作模型DAP，并且基于DAL对CPS属性进行验证。

主权项

1.一种基于HybridUML向微分代数程序转换的CPS建模与验证方法，其特征在于包括如下步骤：步骤1)根据已有的HybridUML形式化描述定义，对HybridUML形式化描述进行扩充，给出agent和mode的形式化描述多元组；步骤2)利用HybridUML提供的图形化元素对CPS系统进行建模；HybridUML通过agent描述系统的结构，通过mode来刻画系统的行为；步骤3)依据提出的agent和mode的形式化描述多元组的定义，给出所建的图形化模型中每个agent和mode的多元组的形式化描述；步骤4)制定HybridUML中离散变迁语义向微分代数程序中离散变迁语义的转换规则，制定HybridUML中连续变化语义向微分代数程序中连续变化语义的转换规则：①离散变迁语义的转换：HybridUML中的变迁由五元组组成t＝(src，tar，trigger，guard，action)src和tar分别是变迁的源mode和目标mode的控制点；trigger是变迁的触发器；guard是变迁迁移的条件；action是变迁产生的动作(变量的离散赋值或产生信号)。微分代数程序中的变迁表示为state＝m_src∧guard；action；state：＝m_tar。HybridUML中的离散变迁可以通过如下规则转换成微分代数程序中的离散变迁：$\forall m_1,m_2\in M,$②连续变化语义的转换：HybridUML通过flow，alge和inv约束agent的连续行为。微分代数程序通过微分代数约束来刻画连续行为。微分代数程序的连续行为表示为state＝m∧DA-constraints_flow，alge∧DA-constraints_inv，系统处于发生连续行为的状态m时变量以DA-constraints_flow，alge的约束条件连续变化，并且在这一连续变化的过程中必须满足这一变化过程中所应保持的不变量约束DA-constraints_inv。HybridUML中的连续动态行为可以通过如下规则转换成DAP：步骤5)制定寻找HybridUML模型中共享变量的算法：寻找出模型中所有的共享变量集合，HybridUML中处于同一共享变量集中的变量在整个系统中刻画的是同一变量，即同一个共享集中的变量为同一个变量，为系统中相同的变量统一变量名，制定寻找HybridUML模型中共享信号的算法，寻找模型中的共享变量集；步骤6)HybridUML中所有agent某一时间段的连续变化共同刻画整个系统在这一时刻段的连续变化，根据步骤4)中的连续变化语义转换规则，制定从HybridUML模型中系统连续变化向微分代数程序中系统连续变化的转换规则；记HybridUML中所有的TopMode所组成的集合为{tm₁，tm₂…tm_n}，HybridUML中系统表示某一连续动态行为状态可以转换为如下DAP，其中表示tm_i中具有控制权的mode：步骤7)HybridUML系统中某一个agent中的离散变迁可能会触发另一个变迁，并且可能通过共享变量以及共享信号触发另一个agent中的离散变迁，制定算法，获取因某一个离散变迁所引起的一系列连续的离散变迁，根据步骤4)中的离散变迁语义转换规则，制定从HybridUML模型中系统离散变迁向微分代数程序中系统离散变迁的转换规则，基本思路是通过初始变迁的行为得到由该变迁行为所引起发生的其他变迁，然后再寻找由已发生的变迁的行为引起发生的变迁，重复这个过程，直到没有引起新的变迁的发生，这样就得到了因某一个离散变迁所引起的一系列连续的离散变迁；步骤8)根据步骤6)和步骤7)中提出的转换规则，依据系统执行的过程，将系统的HybridUML模型转换为DAP模型，系统在执行中会经历列离散变迁和连续变化的过程，在这个过程中，依据步骤6)中的规则将HybridUML中的离散变迁转换为微分代数程序中的离散变迁，依据步骤7)中的规则将HybridUML中的连续变化转换为微分代数程序中的连续变化；步骤9)使用微分代数动态逻辑对需要验证的系统属性进行描述，并使用微分代数动态逻辑的推理规则对属性进行推理验证；步骤10)验证结束。