中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
XYZ中的反应型系统的描述和验证
作者: 沈伟
答辩日期: 1998
专业: 计算机软件
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: XYZ系统 ; 反应型系统 ; Hoare逻辑 ; 逐步求精 ; 前断言 ; 后断言 ; 通讯 ; 通道 ; 握手
摘要: 反应型系统(Reactive System)是现实生活中存在广泛应用的一种系统,它跟以往的串行程序不同,它由一些并行的进程构成,这些进程通过彼此之间的通讯或共享变量来发生联系,并且对外界的信息进行处理。对一个封闭的串行系统,我们可以利用Hoare逻辑对之进行正确性的验证。其特征是将一程序或其中一完整的子部分(如过程)的形式语义表示为两个一阶逻辑的断言。其中之一为此程序(输入参数)必须满足的前提条件,称为前置条件(Pre-condition)或前置断言(Pre-assertion),另一是该执行之后,其结果(包括输入与输出两类参数)必须满足的终结条件,称为后续条件(Post-condition)或后续断言(Post-assertion)。当一程序在前置条件被满足后开始执行,到它执行到终止时,其后续条件亦被满足,则该程序的安全性成立(活性,或终止性另行证明)。这是迄今关于程序正确性验证最为完整并为计算机科学界普遍肯定的方法。但是到了反应型系统,传统的Hoare逻辑就不适用了,它只适用于串行程序。本文讨论了如何在并行通讯进程中使用Hoare逻辑的问题。我们对进程之间的通讯语句加入断言进行限制。我们把一个通讯的进程当作过程类似地进行验证,对输入语句,我们对之加入前断言,以便对输入的变理进行限制,我们可以把它当作是初时的输入变量,而对输出语句,我们可以将它看作是整个进程的输出,对它加入后断言进行描述。这样,由于每个输入我们都有前断言进行限制,我们可以对每个通讯的进程进行单独验证,证明它的后断言以及每个输出语句的后断言成立。作为一个组通讯进程,它的后断言就是各个进程的后断言以及它们之间的握手的情况的结合。对于不终止的进程,由于我们对通讯语句有断言限制,我们可以将每次循环看作一次执行,对之写出前后断言。这样,我们就可以利用Hoare逻辑进行描述和验证。本文后半部分反应型系统的一个具体例子-RPC-Memory描述问题进行了细致的讨论。PRC-Memory描述问题是国际计算机界的一个著名问题,它要求对一系列Component进行描述及验证,各个Component之间互有调用发生。我们在XYZ系统物框架内先用逐步求精的方法得到各个Component的描述,然后对它进行了验证。
英文摘要: Reactive System is widely used computing system in real life. It is different from the traditional sequential system. It is composed of a series of parallel processes. These processes connect with each other by communication or shared variable. They also communicate with the environment, dealing with the information from the environment. We can specify a sequential program by Hoare logic. We express the formal semantics by two assertions of first-order logic. One is the Pre-assertion (or Pre-condition), which is the restriction of the input variables. The other is Post-assertion (or Post-condition), which the output variables should satisfy when the execution of the program finishes. A program begins to execute when the pre-assertion is satisfied, and when the execution finishes, the output variables satisfy the post-assertion, we can say that the safety property of the program is verified (The liveness property should be verified in other way). Hoare logic is the most widely used and acknowledged method for verifying a program. Unfortunately, it can only be used to verify sequential program. As to reactive system, because there can be communication or shared variable, we can't use traditional Hoare logic to verify reactive system. In this thesis, we discussed how to use Hoare logic in a communicating reactive system. We add restriction on communication, and then we can verify a process just like a procedure. A Channel link with two processes, one process write to the channel and the other read from the channel. We consider the variables read from the channel as one special kind of the input parameter of the process. Just like the ordinary input parameters require pre-conditions to constrain their values in order to guarantee the validity of the post assertions, this kind of input variables read from the channel also need some constraints to protect the semantics of the process. And we add a pre-assertion on it. We consider the variables written to the channel as the output variables as if they are the output at the end, and add a post-assertion on them. Then we can verify communicating processes separately, and the whole post-assertion is the conjunction of all the post-assertion of each the process, together with the condition of the shake-hand of each other. As to the process that will not finish, because we have restriction on communication, we can regard each loop as one execution, and write the pre- and post-assertion, so we can verify this sort of system by Hoare logic. we discussed an example of reactive system, RPC-Memory Specification Problem, in the second part of this thesis. RPC-Memory Specification Problem is a famous problem. It requires specifying and verifying a series of components; each component can issue calls to other component and the other issue returns later. We first got the specification of these components by stepwise refinement, and then verify these components.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6024
Appears in Collections:中科院软件所

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

Recommended Citation:
沈伟. XYZ中的反应型系统的描述和验证[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1998-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