Protocol Synthesis from Timed and Structured Specifications

Akio Nakata, Teruo Higashino and Kenichi Taniguchi
Department of Information and Computer Science, Osaka University

E-mail:{nakata,higashino,taniguchi}@ics.es.osaka-u.ac.jp

Abstract

In this paper, we propose a
method to synthesize protocol specifications
automatically from service specifications written in 
a time-extended LOTOS called LOTOS/T+. 
In LOTOS/T+, structured descriptions, such as parallelism and
interruption are allowed to describe service specifications,
and time-constraints among non-adjacent actions can be
described using Presburger formulas.
Here we assume that there is a reliable 
communication channel between any two nodes and the maximum communication
delay for each channel is bounded by a constant.
Moreover we assume service specifications have no deadlocks.
Under our simulation policy, a specification $S'$
is derived from a given service specification $S$ 
and a given maximum communication delay of each channel.
In $S'$, time-constraints necessary for exchanging synchronization messages 
are added. 
If $S$ and $S'$ can carry out the same behaviour, i.e., if $S$ and $S'$ are
bisimulation equivalent when time is ignored, then a correct protocol 
specification for simulating $S$ 
is derived from $S'$ automatically.