计算机研究与发展 ›› 2015, Vol. 52 ›› Issue (1): 167-176.doi: 10.7544/issn1000-1239.2015.20130722
符宁1,杜承烈1,李建良2,刘志强3,彭寒4
Fu Ning1,Du Chenglie1,Li Jianliang2,Liu Zhiqiang3,Peng Han4
摘要: 针对嵌入式系统体系结构分析设计语言(architecture analysis and design language, AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性质描述为时序逻辑公式,通过模型检验工具对可调度性进行分析和验证.研究结果表明,使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确.
中图分类号: