安全计算机平台测试序列的生成与优化

Generation and Optimization of Safety-critical System Test Sequence

基于模型检验的测试序列生成及优化方法,在描述符号模型检验原理和CTL(计算树逻辑,Computation Tree Logic)覆盖标准的基础上,通过分析测试序列的覆盖范围,证明了测试序列的覆盖完整性,并生成和优化了安全计算机平台测试序列.

To improve the completeness and efficiency of SCS testing program,the testing based on model checking method as a kind of formalization is introduced in the paper,and to avoiding present tradi—tional solution occurring question,such as low efficiency lead by subj ectivity and no—guarantee of complete—ness of system performance.Analysis and modeling of SCS is completely described in this paper through the model checking tool NuSMV,simulation testing is conducted and result is given.