《表4 CTL模态算子：航天器软件典型缺陷模式的自动检测技术》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《航天器软件典型缺陷模式的自动检测技术》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

航天器软件系统作为典型的并发系统，其运行过程和行为可以抽象为状态转移系统，程序性质则可以通过计算树逻辑（CTL-Computation Tree Logic）进行刻画．计算树逻辑是一种典型的模态/时序逻辑描述语言，可以描述状态的前后关系和分支情况，属于分叉时序逻辑．对于CTL，使用路径量词（包括:A、E）和模态算子（包括:F、G、X、U）对程序性质进行形式化描述[5]．其中，量词A（Always）和E（Exists）描述分支情况，分别表示全部计算路径存在和某条计算路径存在；模态算子描述状态的前后关系，如表4所示．