可执行模型的在线形式验证

摘要

本发明涉及可执行模型的在线形式验证。一种可执行系统的自动形式验证的系统和方法包括声明监测器，所述声明监测器配置成相对于规格书中的声明来验证系统。所述声明监测器包括：剖析器，所述剖析器配置成使用布尔命题来产生表示规格书中的声明的命题公式；滤波器，所述滤波器配置成使用命题符号的真值赋值来产生系统进程；以及迹线验证器，所述迹线验证器配置成使用命题符号的真值赋值和命题公式利用系统进程来验证所述声明。

主权项

一种相对于规格书中的声明来验证系统的方法，所述方法包括以下步骤：使用布尔命题来产生表示规格书中的声明的命题公式，每个布尔命题与声明中的原子声明相关联；生成测试案例，所述测试案例被设计成相对于所述声明来评估系统的性能；响应于测试案例在系统上的模拟来生成配置数据；将所述配置数据转换为命题符号的真值赋值；使用命题符号的真值赋值来产生系统进程；将系统进程转换为命题符号的真值赋值序列，从而命题符号含有来自于配置数据和系统进程两者的数据；以及以命题符号的真值赋值序列和命题公式来验证所述声明。