计划覆盖

• 时序逻辑 LTL/CTL
• 状态爆炸
• 符号模型检验
• SPIN/NuSMV

原子清单