Synthesizing Protocol Specifications from Service Specifications
in Timed Extended Finite State Machines
Synthesizing Protocol Specifications from Service Specifications
in Timed Extended Finite State Machines
Files
Publication or External Link
Date
1998-10-15
Authors
Park, Jun-Cheol
Miller, Raymond E.
Advisor
Citation
DRUM DOI
Abstract
We propose a specification model and present a method to algorithmically
derive a protocol specification from a service specification based on
the model.
Unlike the previous models based on finite state machines, the proposed
model can explicitly express concurrency, synchronization, and timing
requirements such as delays and timeouts. We assume that there exists
a reliable communication channel between any two protocol entities and
the maximum delay for each channel is bounded by a positive constant.
Because of the variable nature of the communication delays along with
the time constraints associated with events, no protocol specification
can fully simulate the service specification.
The proposed method derives a protocol specification that is optimal
in the sense that it provides the largest possible subset of the service
specification under the communication delay constraints.
We also give a method to derive a sub specification from a service
specification and a maximum communication delay of each channel such that
the sub specification, but no superset of it, can be simulated by the
derived protocol specification.