具体反例生成与图形化显示系统

CORC > 软件研究所 > 软件所图书馆 > 期刊论文

	具体反例生成与图形化显示系统
	信贤卫
刊名	计算机系统应用
	2013
期号	11 页码:51-57
关键词	时间自动机模型检测 LTL性质反例生成模拟器 timed automata model checking LTL properties counterexample generation simulator
ISSN号	1003-3254
其他题名	CCGS System
中文摘要	模型检测是用来验证系统模型是否满足所期望性质的一种形式化方法，模型检测相对于其它的模型检验方法有两个显著的特点，一个是它对模型进行检测的过程是自动化的，另一个是当系统不满足所验证的性质时，它会给出一条反例路径，这条反例路径可以为系统修正提供帮助。本文研究的重点就是如何使这条反例路径的生成在高效的同时其反例信息又直观易懂，为系统修正带来更方便快捷的帮助。本文中实现了具体反例生成与图形化显示系统(简称 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.
语种	中文
公开日期	2014-12-16
内容类型	期刊论文
源URL	[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.