[发明专利]基于重写逻辑的并发实时程序验证的优化处理系统及其方法

摘要

一种计算机应用技术领域的基于重写逻辑的并发实时程序验证的优化处理系统及其方法，该系统包括：程序模型模块、性质模型模块和重写逻辑验证模块，通过重写逻辑验证并发实时程序，将系统的模型和即将验证的性质均采用代数模型进行状态空间优化，并特别采用时间元模型能够处理实时相关的性质，采用等价状态压缩和代数模拟优化以提高程序验证效率。

主权项

一种基于重写逻辑的并发实时程序验证的优化处理系统，其特征在于，包括：程序模型模块、性质模型模块和重写逻辑验证模块，其中：程序模型模块与重写逻辑验证模块相连接并传输系统的状态转换信息，性质模型模块与重写逻辑验证模块相连接并传输待验证的系统的安全性、活性等描述信息，重写逻辑验证模块与上述程序模型模块和性质模型模块相连接并接受系统描述与系统验证性质的信息，然后采用重写逻辑虚拟机进行验证；所述的程序模型模块包括：状态描述子模块、系统描述子模块和时间描述子模块，其中：状态描述子模块与系统描述子模块相连接并传输状态信息，系统描述子模块与时间描述相连接并传输信息，时间描述子模块与程序模型主模块相连接并传输经过有限抽样的时间信息；所述的性质模型模块包括：线性时态逻辑子模块、公式简化子模块和性质模板库子模块，其中：线性时态逻辑子模块与公式简化子模块相连并传输系统通过GUI接受用户输入，并转为线性时态逻辑公式的信息，公式简化子模块与性质模型主模块相连接并传输经过状态压缩和公式压缩的待验证性质描述信息，性质模板库子模块与性质模型主模块相连并传输常见的系统验证模板的信息简化用户输入；所述的重写逻辑验证模块包括：Kripke结构子模块，代数模拟优化子模块，和模型检验虚拟机引擎子模块，其中：Kripke结构子模块建立通过前端的性质模型模块和系统模型模块合成系统整体的Kripke结构信息并输出到代数模拟优化子模块，代数模拟优化子模块接收Kripke结构信息并采用代数模拟压缩等价状态，将优化过的Kripke结构输出到模型检验虚拟机引擎子模块，模型检验虚拟机引擎子模块采用重写逻辑验证系统是否符合安全性和活性等性质。