中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
一个并发传值系统自动验证工具的图形界面实现
作者: 肖颖奇
答辩日期: 2003
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 形式化方法 ; 模型检测 ; 并发传值系统 ; 带赋值符号迁移图 ; 仿真
其他题名: Implementing A Graphical User Interface for An Automated Proof Tool for Message-Passing Concurrent System
摘要: 随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为学术界和工业界共同关注的问题。在诸多的系统分析和验证方法中,模型检测技术是近二十年来最成功的自动验证技术之一。其因自动化程度高,效率高等优点而被广泛应用于有穷状态系统的分析与验证中。并发进程之间通过传送消息实现协作。但现有的基于进程代数的模型检测工具都不能直接处理进程间的数据传送。本文介绍一个并发传值系统自动验证工具图形用户界面的实现,主要工作如下:使用Motif标准图形界面开发工具包实现工具的图形用户界面窗口。给出函数式编程语言SML程序和C语言程序间的一种通信方案。并给出工具自动验证引擎与图形用户界面之间的通信方案以协同完成验证任务。对模型检测反例状态迁移图的图形显示进行讨论,给出了以树状结构图的显示反例状态迁移图的方案扩展工具分析系统的功能,实现系统仿真器。
英文摘要: 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.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6110
Appears in Collections:中科院软件所

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

Recommended Citation:
肖颖奇. 一个并发传值系统自动验证工具的图形界面实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2003-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