带过去时态的线性时态逻辑性质的有界运行时验证方法

摘要

本发明公开了一种带过去时态的线性时态逻辑性质的有界运行时验证方法，包括：通过性质挖掘子系统，在系统开发阶段，使用测试数据对系统进行仿真运行，以获取系统在实际运行中的事件信息并将其存储在事件日志中，并且从事件日志中自动地获取系统运行过程中具备的带过去时态的所有线性时态逻辑性质并将其存储于可筛选的性质规范集合中；通过性质验证子系统，在系统运行阶段，对系统事件进行监控，并且使用经筛选的性质规范集合对系统进行时态性质的检查验证。能够将设计阶段的验证规范运用于运行时验证阶段，方便非系统设计和开发人员能够通过自身解决以往解决不了从而必须依靠专业系统设计开发人员才能解决的问题，同时也避免了重新开发验证程序。