|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
Third International Conference on Network Protocols (ICNP'95)
Protocol synthesis from timed and structured specifications
Tokyo, Japan
November 07-November 10
ISBN: 0-8186-7216-1
| ASCII Text | x | ||
| A. Nakata, T. Higashino, K. Taniguchi, "Protocol synthesis from timed and structured specifications," 2012 20th IEEE International Conference on Network Protocols (ICNP), pp. 74, Third International Conference on Network Protocols (ICNP'95), 1995. | |||
| BibTex | x | ||
| @article{ 10.1109/ICNP.1995.524821, author = {A. Nakata and T. Higashino and K. Taniguchi}, title = {Protocol synthesis from timed and structured specifications}, journal ={2012 20th IEEE International Conference on Network Protocols (ICNP)}, volume = {0}, year = {1995}, isbn = {0-8186-7216-1}, pages = {74}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICNP.1995.524821}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - 2012 20th IEEE International Conference on Network Protocols (ICNP) TI - Protocol synthesis from timed and structured specifications SN - 0-8186-7216-1 SP EP A1 - A. Nakata, A1 - T. Higashino, A1 - K. Taniguchi, PY - 1995 KW - protocols; specification languages; synchronisation; protocol specifications; LOTOS/T+; parallelism; interruption; Presburger formulas; time-constraints; service specifications; bisimulation equivalent VL - 0 JA - 2012 20th IEEE International Conference on Network Protocols (ICNP) ER - | |||
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
Index Terms:
protocols; specification languages; synchronisation; protocol specifications; LOTOS/T+; parallelism; interruption; Presburger formulas; time-constraints; service specifications; bisimulation equivalent
Citation:
A. Nakata, T. Higashino, K. Taniguchi, "Protocol synthesis from timed and structured specifications," icnp, pp.74, Third International Conference on Network Protocols (ICNP'95), 1995
Usage of this product signifies your acceptance of the Terms of Use.
