| 具体反例生成与图形化显示系统 |
| 其他题名 | CCGS System
|
| 信贤卫
|
| 2013
|
| 发表期刊 | 计算机系统应用
 |
| ISSN | 1003-3254
|
| 期号 | 11页码:51-57 |
| 摘要 | 模型检测是用来验证系统模型是否满足所期望性质的一种形式化方法，模型检测相对于其它的模型检验方法有两个显著的特点，一个是它对模型进行检测的过程是自动化的，另一个是当系统不满足所验证的性质时，它会给出一条反例路径，这条反例路径可以为系统修正提供帮助。本文研究的重点就是如何使这条反例路径的生成在高效的同时其反例信息又直观易懂，为系统修正带来更方便快捷的帮助。本文中实现了具体反例生成与图形化显示系统(简称 CCGS)，它能快速生成离散语义下具体反例并图形化显示时间自动机沿着该具体反例的运行过程。实验结果表明CCGS能够快速生成具体反例路径信息，并且能够图形化显示具体反例信息，为系统修正提供更直观的信息，提高系统的正确性和安全性。 Model checking is a formal method to verify the system satisfies an expected property or not. Trere are two significant advantages of it, one is that it is fully automatic and the other is that if the system doesn't satisfy the checked property, it will generate an counterexamples which can help to fix errors in the system. The main purpose of this paper is to generate this counterexamples efficiently and intuitively. In order to generate the counterexamples efficiently and graphically display the operating processes of the system running alongside the concrete counterexamples, a system CCGS has been developed. Experimental results have shown that CCGS delivers an expected performance, and can help to improve the correctness and safety of the checked systems. |
| 关键词 | 时间自动机
模型检测
Ltl性质
反例生成
模拟器
Timed Automata
Model Checking
Ltl Properties
Counterexample Generation
Simulator
|
| 部门归属 | 中国科学院软件研究所，北京 100190; 中国科学院大学，北京 100190
|
| 语种 | 中文
|
| 内容类型 | 期刊论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/17003
|
| 专题 | 中国科学院软件研究所
|
推荐引用方式
GB/T 7714 |
信贤卫. 具体反例生成与图形化显示系统[J]. 计算机系统应用,2013(11):51-57.
|
| APA |
信贤卫.(2013).具体反例生成与图形化显示系统.计算机系统应用(11),51-57.
|
| MLA |
信贤卫."具体反例生成与图形化显示系统".计算机系统应用 .11(2013):51-57.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论