A RELY AND GUARANTEE METHOD FOR TIMED CSP - A SPECIFICATION AND DESIGN OF A TELEPHONE EXCHANGE

被引：13

作者：

KAY, A ^{[1
]}

REED, JN ^{[1
]}

机构：

[1] UNIV OXFORD, COMP LAB, OXFORD OX2 3QD, ENGLAND

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1993年 / 19卷 / 06期

关键词：

COMMUNICATING PROCESSES; CORRECTNESS; DISTRIBUTED DECOMPOSITION; FORMAL SPECIFICATION; LIVENESS; RELY AND GUARANTEE; SAFETY; SWITCHING SYSTEMS; SYNCHRONIZATION;

D O I：

10.1109/32.232027

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We describe a rely and guarantee method for Timed CSP, by which we specify the behavior of a component belonging to a composite system in terms of what it guarantees to its neighbors and what it relies on from them. We illustrate the method by presenting an overview of our specification of POTS (Plain Old Telephone Service) together with part of a design which provably satisfies this specification. The specification and design deal with safety, liveness, and troublesome race conditions.

引用

页码：625 / 639

页数：15