| 题名 | 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的描述，然后对它进行了验证。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 59 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6024]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 沈伟. XYZ中的反应型系统的描述和验证[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1998. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论