Institutional Repository
| 改进的以SMT为基础的实时系统限界模型检测 | |
| Alternative Title | improved smt-based bounded model checking for real-time systems |
| 徐亮 | |
| 2010 | |
| Source | 软件学报
 |
| ISSN | 1000-9825 |
| Volume | 21Issue:7Pages:1491-1502 |
| English Abstract | 基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进. |
| Keyword | 限界模型检测 可满足性模块理论 实时系统 时间自动机 时间kripke结构 带时间参数的计算树逻辑bounded Model Checking Satisfiability Modulo Theories Real-time System Timed Automata Timed Kripke Structure Tctl (Timed Computation Tree Logic) |
| Department | 中国科学院软件研究所计算机科学国家重点实验室;中国科学院软件研究所; |
| Subject | Computer Science |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/9846 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | 徐亮. 改进的以SMT为基础的实时系统限界模型检测[J]. 软件学报,2010,21(7):1491-1502. |
| APA | 徐亮.(2010).改进的以SMT为基础的实时系统限界模型检测.软件学报,21(7),1491-1502. |
| MLA | 徐亮."改进的以SMT为基础的实时系统限界模型检测".软件学报 21.7(2010):1491-1502. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 改进的以SMT为基础的实时系统限界模型检（631KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment