SPECIFICATION AND VERIFICATION OF A SLIDING WINDOW PROTOCOL IN LOTOS

被引：0

作者：

MADELAINE, E ^{[1
]}

VERGAMINI, D ^{[1
]}

机构：

[1] CERICS, SOPHIA ANTIPOLIS, F-06565 VALBONNE, FRANCE

来源：

IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS | 1992年 / 2卷

关键词：

VERIFICATION; PROCESS CALCULUS; PARALLELISM; CONCURRENCY; LOTOS; PROTOCOL; TRANSITION SYSTEM; BEHAVIORAL SEMANTICS; AUTOMATA;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We give an example of protocol verification in Lotos, using automata-based verification tools available inside the Lotosphere Integrated Tool Environment (Lite). The current state of tools imposes a dedicated, behaviour oriented, specification style. The example we consider is a Sliding Window protocol. We present the specification of the various components of the protocol, and analyse its behaviour for various quality of the underlying communication media: we prove that the protocol is able to recover from the loss, the duplication, and the shuffling of messages. We give time and space measurements of the verification activities, highlighting the methods for state explosion control.

引用

页码：495 / 510

页数：16