• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >A method for the specification, composition, and testing of distributed object systems.
【24h】

A method for the specification, composition, and testing of distributed object systems.

机译：一种规范，组成和测试分布式对象系统的方法。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present a specification methodology based on three fundamental operators from temporal logic: initially, next, and transient. From these operators we derive a collection of higher-level operators that are used for component specification. The novel aspect of our specification methodology is that we require that these operators be used in the following restricted manner: (1) A specification statement can refer only to properties that are local to a single component. (2) A single component must be able to guarantee unilaterally the validity of the specification statement for any distributed system of which it is a part. Specification statements that conform to these two restrictions we call certificates.;Another novel aspect of our methodology is the introduction of a new temporal operator that combines both safety and progress properties. The concept underlying this operator has been used implicitly before, but by extracting this concept into a first-class operator, we are able to prove several new theorems about such properties. We demonstrate the utility of this operator and of our theorems by using them to simplify several proofs.;The restrictions imposed on certificates are severe. Although they have pleasing consequences as described above, they can also lead to lengthy proofs of system properties that are not simple conjunctions. To compensate for this difficulty, we introduce collections of certificates that we call services. Services facilitate proof reuse by encapsulating common component interactions used to establish various system properties.;We experiment with our methodology by applying it to several extended examples. These experiments illustrate the utility of our approach and convince us of the practicality of component-based distributed system development.;The first restriction is motivated by our desire for these component specifications to be testable in a relatively efficient manner. We characterize a subset of certificates that can be translated into a testing harness by a simple parser with very little programmer intervention. The second restriction is motivated by our desire for a simple theory of composition: If a certificate is a property of a component, that certificate is also a property of any system containing that component.
机译：我们提出了一种基于时间逻辑的三个基本运算符的规范方法论：初始，下一步和瞬态。从这些运算符中，我们得出了用于组件规格说明的高级运算符的集合。规范方法的新颖之处在于，我们要求以下列受限方式使用这些运算符：（1）规范语句只能引用单个组件本地的属性。 （2）单个组件必须能够单方面保证规范声明对它所组成的任何分布式系统的有效性。符合这两个限制的规范声明称为证书。我们的方法的另一个新颖之处是引入了结合了安全性和进度属性的新时间运算符。该运算符所基于的概念之前已被隐式使用，但是通过将该概念提取为一等运算符，我们能够证明有关此类性质的几个新定理。通过使用它们简化一些证明，我们证明了该算子和我们的定理的效用。尽管它们如上所述具有令人愉悦的结果，但它们也可能导致冗长的系统属性证明，而不是简单的结合。为了弥补这一困难，我们引入了称为服务的证书集合。服务通过封装用于建立各种系统属性的公共组件交互来促进证明重用。;我们通过将其应用于几个扩展示例来尝试我们的方法。这些实验说明了我们方法的实用性，并使我们确信基于组件的分布式系统开发的实用性。第一个限制是由于我们希望以相对有效的方式测试这些组件规范而引起的。我们描述了证书的子集，可以通过简单的解析器将其转换为测试工具，而程序员的干预很少。第二个限制是由我们对简单的组成理论的渴望所激发的：如果证书是组件的属性，那么该证书也是任何包含该组件的系统的属性。

著录项

  • 作者

    Sivilotti, Paolo A. G.;

  • 作者单位

    California Institute of Technology.;

  • 授予单位 California Institute of Technology.;
  • 学科 Computer science.
  • 学位 Ph.D.
  • 年度 1998
  • 页码 140 p.
  • 总页数 140
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号