基于CTL时序逻辑公式的反例分析及可视化方法、介质及设备

本发明提出了一种基于CTL时序逻辑公式的反例分析及可视化方法、介质及设备，属于软件工程领域。本发明仅关注反例和CTL时序逻辑公式本身，集中分析第一个错误的原因，将因果关系的概念运用到查找引起属性第一次失败的原因，据此设计因果关系算法；使用变量表、属性视图和属性公式树这三种可视化手段对反例进行呈现，同时根据因果关系算法提供的原因集将失败的原因信息展示在对应的可视化视图中。本发明独立于反例生成工具和模型本身，可以作为轻量级的外层应用于任何模型检查工具，帮助用户更好地理解错误的原因。