基于CCTL的软件可靠性测试输入特性描述方法  

CCTL based description method of input characteristics for software reliability test

作　　者：盛云龙 魏长安[1] 姜守达[1] Sheng Yunlong;Wei Chang＇an;Jiang Shouda(Automatic Test and Control Institute, Harbin Institute of Technology, Harbin 150080, China)

机构地区：[1]哈尔滨工业大学自动化测试与控制研究所

出　　处：《仪器仪表学报》2018年第4期141-149,共9页Chinese Journal of Scientific Instrument

摘　　要：软件可靠性测试是指为了保证和验证软件的可靠性要求而对软件进行的测试。由于目前缺少满足被测软件输入的时序性、并发性和约束性等输入特性的有效的形式化描述方法,软件可靠性测试数据的生成无据可依,全面的软件可靠性测试难以实现。利用钟控计算树逻辑（CCTL）公式在模型检测领域能够准确描述模型内部时序关系的优势,提出了基于CCTL的软件可靠性测试输入特性描述方法,该方法对输入特性准确有效的描述,可为可靠性测试数据的生成提供依据。最后,通过对一个实例的输入特性进行描述,验证了方法的可行性和有效性。Software reliability test is to ensure and verify the reliability of software. There is no effective formalization description method to describe the input characteristics of timing sequence,concurrency and constraint. Thus,the generation of software reliability test data lacks clear guidance and comprehensive software reliability test is difficult to realize. Due to the advantage of modeling timing sequence in model checking,a clocked computation tree logic（ CCTL） based description method of input characteristics for software reliability test is proposed in this work. The proposed method can provide the basis for reliability test data generation by describing input characteristics accurately and effectively. Finally,the feasibility and effectiveness of the proposed method is verified by a real case study.

关 键 词：软件可靠性测试 时序输入特性 约束输入特性 形式化描述 钟控计算树逻辑 

分 类 号：TH701[机械工程—仪器科学与技术]