SPECIFICATION AND ANALYSIS OF A COMPOSITION OF PROTOCOLS

被引：0
|
作者：
LUNDY, GM
机构：
[1] Department of Computer Science, Naval Postgraduate School, Monterey
来源：
INFORMATION SCIENCES | 1993年 / 70卷 / 03期
关键词：
D O I：
10.1016/0020-0255(93)90079-2
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
A composite protocol constructed from two smaller protocols is formally specified, and a proof of correctness is given. The formal specification of the composite protocol is constructed from the formal specification of the two protocols from which it is composed, and the proof of the composite protocol is an expansion of the correctness proofs of the two smaller protocols. The composite protocol is a data-compression protocol which combines two well-known data-compression protocols, achieving further compression. The protocol processes are specified as a set of actions, each of which has a guard, or Boolean expression. An action may take place only if its guard is true and is an atomic event. Verification is accomplished by proving that the set of states satisfying an invariant is closed.
引用
收藏
页码：221 / 239
页数：19
相关论文
共 50 条
12345