改进的以SMT为基础的实时系统限界模型检测
文献类型：期刊论文
| 作者 | 徐亮 |
| 刊名 | 软件学报
 |
| 出版日期 | 2010 |
| 卷号 | 21期号:7页码:1491-1502 |
| 关键词 | 限界模型检测 可满足性模块理论 实时系统 时间自动机 时间Kripke结构 带时间参数的计算树逻辑bounded model checking satisfiability modulo theories real-time system timed automata timed Kripke structure TCTL (timed computation tree logic) |
| ISSN号 | 1000-9825 |
| 其他题名 | improved smt-based bounded model checking for real-time systems |
| 中文摘要 | 基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进. |
| 学科主题 | Computer Science |
| 公开日期 | 2011-05-23 |
| 附注 | SAT-Based bounded model checking (BMC) has high complexity in dealing with real-time systems. Satisfiability modulo theories (SMT) solvers can generalize SAT solving by adding the ability to handle arithmetic and other decidable theories. This paper uses SMT in BMC for real-time systems instead of SAT. The clocks can be represented as integer or real variables directly and clock constraints can be represented as linear arithmetic expressions. These make the checking procedure more efficient. TCTL (timed computation tree logic) is used to specify the properties of real-time systems and improvement of the encodings has been done. |
| 源URL | [http://124.16.136.157/handle/311060/9846]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _期刊论文 |
| 推荐引用方式 GB/T 7714 | 徐亮. 改进的以SMT为基础的实时系统限界模型检测[J]. 软件学报,2010,21(7):1491-1502. |
| APA | 徐亮.(2010).改进的以SMT为基础的实时系统限界模型检测.软件学报,21(7),1491-1502. |
| MLA | 徐亮."改进的以SMT为基础的实时系统限界模型检测".软件学报 21.7(2010):1491-1502. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。