中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
有穷状态XYZ/E程序的模型检查研究
作者: 赵海云
答辩日期: 2002
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 有穷状态反应系统 ; 线性时序逻辑 ; 模型检查 ; XYZ/E语言 ; 自动验证
摘要: XYZ/E语言是一个可执行的时序逻辑语言,可以用来描述有穷状态反应系统.为了构造一个以XYZ/E语言作为系统描述语言的模型检查工具,可以在已有的成熟模型检查工具的基础上,实现一个语言转换工具,把对反应系统的XYZ/E语言描述转换成该模型检查工具可接受的描述,然后利用该工具进行模型检查.SPIN是一个得到广泛应用的线性时序逻辑模型检查工具,能够验证由若干个进程异步组合而成的有穷状态系统,它使用进程元语言Promela来描述反应系统.我们实现了一个语言转换工具,可以把满足一定限制的XYZ/E程序转换成Promela程序,从而可以利用SPIN来对用XYZ/E语言描述的有究状态反应系统进行模型检查,达到了能够对用XYZ/E语言描述的有穷状态系统进行模型检查的目的.Finite-state reactive systems arise naturally in several areas of computer science, particularly in the design of digital circuits and communication protocols. These systems are characterized by ongoing, typically nonterminating and highly nondeterministic behavior. Ofen such systems amount to parallel or distributed programs. During the past twenty years, temporal logic model checking has became the most thoroughly researched technology for automatic verification of finite-state reactive systems. In this approach specifications are expressed in a propositional temporal logic, and systems are modeled as a state-transition systems. An efficient search procedure is used to determine automatically if the specifications are satisfied by the transtion systems. Typically, the user provides a high level representation of the model and the specification to be checked. The model checking algorithm will either terminate with the answer true, indicating that the model satisfies the specification, or give a counterexample execution that shows why the formula is not satisfied. The counterexamples are particularly important in finding subtle errors in complex transition systems. Being an executable temporal logic language, XYZ/E can be used to describe finite-state reactive systems. To model-checking a finite-state system described by XYZ/E program, we can reimplement a model checking tool, which using XYZ/E as its system description language, or implement a language-translation tool, which can translation a system described by a XYZ/E program into the same system but described in another language, to utilizing an existing model checker, we choose the latter. Our goal is to model checking systems described by XYZ/E programs. For this end, we have implemented a language translation tool, which can translate a given system described by a XYZ/E program into the same system described by a Promela program, which can be model checked by the famous LTL model checker SPIN.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7404
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW008643.pdf(2024KB)----限制开放-- 联系获取全文

Recommended Citation:
赵海云. 有穷状态XYZ/E程序的模型检查研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2002-01-01.
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-2017  中国科学院软件研究所 - Feedback
Powered by CSpace