改进的以SMT为基础的实时系统限界模型检测
| Data(s) |
2010
|
|---|---|
| Resumo |
基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进. |
| Identificador | |
| Fonte |
徐亮.改进的以SMT为基础的实时系统限界模型检测,软件学报,2010,21(7):1491-1502 |
| Palavras-Chave | #Computer Science #限界模型检测 #可满足性模块理论 #实时系统 #时间自动机 #时间Kripke结构 #带时间参数的计算树逻辑bounded model checking #satisfiability modulo theories #real-time system #timed automata #timed Kripke structure #TCTL (timed computation tree logic) |
| Tipo |
期刊论文 |
