中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
具体反例生成与图形化显示系统
Alternative Title: CCGS System
Author: 信贤卫
Keyword: 时间自动机 ; 模型检测 ; LTL性质 ; 反例生成 ; 模拟器 ; timed automata ; model checking ; LTL properties ; counterexample generation ; simulator
Source: 计算机系统应用
Issued Date: 2013
Issue: 11, Pages:51-57
Department: 中国科学院软件研究所,北京 100190; 中国科学院大学,北京 100190
Abstract: 模型检测是用来验证系统模型是否满足所期望性质的一种形式化方法,模型检测相对于其它的模型检验方法有两个显著的特点,一个是它对模型进行检测的过程是自动化的,另一个是当系统不满足所验证的性质时,它会给出一条反例路径,这条反例路径可以为系统修正提供帮助。本文研究的重点就是如何使这条反例路径的生成在高效的同时其反例信息又直观易懂,为系统修正带来更方便快捷的帮助。本文中实现了具体反例生成与图形化显示系统(简称 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.
Language: 中文
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/17003
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
信贤卫. 具体反例生成与图形化显示系统[J]. 计算机系统应用,2013-01-01(11):51-57.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[信贤卫]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[信贤卫]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2020  中国科学院软件研究所 - Feedback
Powered by CSpace