[00003303]基于抽象解释的线性混成系统不变式的生成方法
技术详细介绍
本发明提供一种线性混成系统不变式的生成系统，输入为线性混成系统模型——线性混成自动机，输出该线性混成系统的节点不变式；线性混成系统不变式生成系统包括转换模块和不变式生成部分两个组成部分如下：1）转换模块基于面向线性混成系统的等价迁移系统构造的模块，其输入侧为线性混成系统模型——线性混成自动机，输出侧为迁移系统模型；2）不变式生成部分，连接上述转换模块，针对上述迁移系统进行分析并根据其分析结果反馈得到线性混成系统模型的不变式；根据转换模块转换生成的迁移系统，输出为原线性混成系统的节点不变式；然后利用新工具进行不变式生成工作。
