有穷状态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. |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 51 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7404]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 赵海云. 有穷状态XYZ/E程序的模型检查研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2002. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。