Multiway synchronization verified with coupled simulation
We consider the problem of implementing multiway synchronization in a distributed environment providing only binary asynchronous communication. Our implementation strategy is formulated as a transformation on transition systems and we give a distributed algorithm for multiway synchronization. Correctness assertions and proofs are based on a new method: coupled simulations. The coupled simulation equivalence is weaker than observation equivalence and stronger than testing equivalence and combines some of their advantages. Like observation equivalence (and unlike testing) it is established through case analysis over single transitions. Like testing equivalence (and unlike observation) it allows an internal choice to be distributed onto several internal choices. The latter is particularly important when relating our distributed implementations to their specifications.
KeywordsTransition System External Action Parallel Composition Couple Simulation Correctness Property
Unable to display preview. Download preview PDF.
- 3.T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. In P. H. J. van Eijk, C. A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS, pages 23–73. North-Holland, 1989.Google Scholar
- 6.P. Eklund. Synchronizing multiple processes in common handshakes. Reports on Computer Science and Mathematics 39, Åbo Akademi, Finland, 1984.Google Scholar
- 8.N. Francez and I. R. Forman. Superimposition for interacting processes. In J. C. M. Baeten and J. W. Klop, editors, Proceedings of CONCUR '90, volume 458 of Lecture Notes in Computer Science, pages 230–245. Springer-Verlag, 1990.Google Scholar
- 10.Y.-J. Joung and S. A. Smolka. Coordinating first-order multiparty interactions. In Proc. 17th Annual ACM Symposium on Principles of Programming Languages, pages 209–220, Orlando, Florida, January 1991.Google Scholar
- 11.D. Kumar. An implementation of N-party synchronization using tokens. In Proc. 10th International Conference on Distributed Computing Systems, pages 320–327. IEEE, 1990.Google Scholar
- 12.R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
- 13.K. Mitchell. Implementations of Process Synchronization and their Analysis. PhD thesis, Department of Computer Science, University of Edinburgh, July 1986.Google Scholar
- 15.S. Ramesh. A new and efficient implementation of multiprocess synchronization. In Parallel Architectures and Languages Europe, volume 259 of Lecture Notes in Computer Science, pages 387–401. Springer-Verlag, 1987.Google Scholar
- 16.S. Ramesh and S. L. Mehndiratta. A methodology for developing distributed programs. IEEE Transactions on Software Engineering, SE-13(8):967–976, August 1987.Google Scholar
- 17.P. Sjödin. From LOTOS Specifications to Distributed Implementations. PhD thesis, Department of Computer Systems, Uppsala University, Uppsala, Sweden, 1991.Google Scholar