| Title: | 一个并发传值系统自动验证工具的图形界面实现 |
| Author: | 肖颖奇
|
| Issued Date: | 2003
|
| Major: | 计算机软件与理论
|
| Degree Grantor: | 中国科学院软件研究所
|
| Place of Degree Grantor: | 中国科学院软件研究所
|
| Degree Level: | 博士
|
| Keyword: | 形式化方法
; 模型检测
; 并发传值系统
; 带赋值符号迁移图
; 仿真
|
| Alternative Title: | Implementing A Graphical User Interface for An Automated Proof Tool for Message-Passing Concurrent System
|
| Abstract: | 随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性成为学术界和工业界共同关注的问题。在诸多的系统分析和验证方法中，模型检测技术是近二十年来最成功的自动验证技术之一。其因自动化程度高，效率高等优点而被广泛应用于有穷状态系统的分析与验证中。并发进程之间通过传送消息实现协作。但现有的基于进程代数的模型检测工具都不能直接处理进程间的数据传送。本文介绍一个并发传值系统自动验证工具图形用户界面的实现，主要工作如下：使用Motif标准图形界面开发工具包实现工具的图形用户界面窗口。给出函数式编程语言SML程序和C语言程序间的一种通信方案。并给出工具自动验证引擎与图形用户界面之间的通信方案以协同完成验证任务。对模型检测反例状态迁移图的图形显示进行讨论，给出了以树状结构图的显示反例状态迁移图的方案扩展工具分析系统的功能，实现系统仿真器。 |
| English Abstract: | As computer hardware and software systems become more and more complex, the problem of how to assure the correctness and reliability of such systems has attracted much attention from both industry and research communities. Among the solutions to the analysis and verification of such systems, model checking is one of the most successful automatic verification techniques in the past two decades. Because of its high level automation and high efficiency, model checking has been widely used in the analysis and verification of finite-state systems. Concurrent processes cooperate with each other by exchanging message. The existing model checking tools based on process algebras cannot directly handle data passing between processes. This thesis describes the implementation of a graphical user interface for an automated proof tool for message-passing concurrent system. The main work includes: Programming a graphical user interface for the tool using Motif toolkit. Presenting a solution to implementing the communication between functional. programming language SML and C language, and designing a protocol between the two parts to cooperate with each other to accomplish verification commands. Discussing how to graphically display counter-example and presenting one solution. Extending the functionality of the tool by implementing a simulator. |
| Language: | 中文
|
| Content Type: | 学位论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/6110
|
| Appears in Collections: | 中科院软件所
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| LW011234.pdf（2413KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
肖颖奇. 一个并发传值系统自动验证工具的图形界面实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2003-01-01.
|
|
|
