基于增量线性规划的动态系统在线增量式快速验证系统及方法

摘要

本发明提供一种基于增量线性规划的动态系统在线增量式快速验证系统及方法。所述方法是首先加载动态系统的问题模型，然后将其与原问题模型进行对比，根据对比结果修改原问题模型；然后使用新的问题模型、原线性规划求解模型根据编码规则修改原线性规划求解模型，从而得到修改后的线性规划求解模型；最后使用线性规划的增量求解技术，利用修改后的线性规划求解模型求解新的问题模型，并给出求解结果。该方法在基于线性规划的线性混成自动机可达性分析方法的基础上，提出了动态的问题模型修改策略，并复用原问题的求解结果来加速新问题的求解，以达到动态系统的在线增量式快速验证，显著提高了问题的求解速度，可以满足动态系统验证的实时性要求。

主权项

一种基于增量线性规划的动态系统在线增量式快速验证系统，其特征在于，包括：问题模型加载模块、求解模型修改模块和模型复用求解模块；其中，问题模型加载模块输入问题模型文件，并得到新的问题模型，求解模型修改模块根据新的问题模型、原线性规划求解模型和编码规则修改线性规划求解模型，模型复用求解模块调用修改后的线性规划求解新的问题模型，并给出求解结果；动态系统的问题模型文件包括单个自动机文件和动态系统模型文件；其中问题模型加载模块得到新的问题模型的步骤具体如下：先判断是否为初次求解，若为初次求解，则首先创建Vector容器存储模型内容，其中元素为单个自动机文件信息，包括文件地址、路径和参数集；若不是初次求解，则在加载问题模型的同时，查看Vector容器中是否已存在相应的自动机，从而得到问题模型的修改策略，根据标记结果加载新加入的自动机，并修改Vector容器的问题模型，得新的问题模型；其中求解模型修改模块修改线性规划求解模型的具体步骤如下：先判断是否为初次求解，若为初次求解，需要创建线性规划求解模型并将问题模型编码为求解模型；若不是初次求解，则根据已经得到的问题模型修改策略修改求解模型，从而得到与新的问题模型对应的求解模型；其中模型复用求解模块求解新的问题模型的具体步骤如下：设置模型复用求解参数，使底层线性规划求解器能复用上次求解结果，调用复用求解器，返回求解结果。