Abstract
The design of concurrent systems often assumes synchronous communication between different parts of a system. When system components are physically apart, this assumption becomes inappropriate. Desynchronization is a technique that aims to implement a synchronous design in an asynchronous manner by placing buffers between the components of the synchronous design. When queues are used as buffers, the so-called ‘diamond property’ (among others) ensures correct operation of the desynchronized design. However, this property is difficult to establish in practice. In this paper, we formally prove that the conditions for desynchronizability can be relaxed, and in particular the diamond property is no longer needed, when half-duplex queues are used as a communication buffer. Furthermore, we discuss how the half-duplex condition can be further relaxed when the diamond property can be partially guaranteed.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alfaro, L., Henzinger, T.: Interface-Based Design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, C.A.R. (eds.) Engineering Theories of Software Intensive Systems. NATO Science Series, vol. 195, pp. 83–104. Springer Netherlands (2005)
Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes, 1st edn. Cambridge University Press, New York (2009)
Balemi, S.: Control of Discrete Event Systems: Theory And Application. Ph.D. thesis, Swiss Federal Institute of Technology, Automatic Control Laboratory, ETH Zurich (May 1992)
Basu, S., Bultan, T.: Choreography conformance via synchronizability. In: Proceedings of the 20th International Conference on World Wide Web, WWW 2011, pp. 795–804. ACM, New York (2011)
Basu, S., Bultan, T., Ouederni, M.: Synchronizability for Verification of Asynchronously Communicating Systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 56–71. Springer, Heidelberg (2012)
Beohar, H.: Refinement of communication and states in models of embedded systems. Ph.D. thesis, Eindhoven university of technology (in preparation)
Beohar, H., Cuijpers, P.J.L.: Desynchronizability of (partial) synchronous closed loop systems. Scientific Annals of Computer Science 21, 5–38 (2011)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30, 323–342 (1983)
Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202, 166–190 (2005)
Fischer, C., Janssen, W.: Synchronous Development of Asynchronous Systems. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 735–750. Springer, Heidelberg (1996)
Forschelen, S.T.J.: Supervisory control of theme park vehicles. Master’s thesis, Eindhoven University of Technology, System Engineering Group, Dept. of Mechanical Engineering (2010)
van Glabbeek, R.J.: The Linear Time - branching Time Spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
Groote, J.F., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.: The formal specification language mCRL2. In: MMOSS 2006 (2006)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
Mateescu, R.: Specification and Analysis of Asynchronous Systems using CADP, pp. 141–169. ISTE (2010), http://dx.doi.org/10.1002/9780470611012.ch5
Peters, K., Schicke, J.-W., Nestmann, U.: Synchrony vs causality in asynchronous pi-calculus. In: Luttik, B., Valencia, F. (eds.) 18th International Workshop on Expressiveness in Concurrency, EXPRESS. EPTCS, vol. 64, pp. 89–103 (2011)
Plotkin, G.D.: A Structural Approach to Operational Semantics. Tech. Rep. DAIMI FN-19, University of Aarhus (1981)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM Journal on Control and Optimization 25(1), 206–230 (1987)
Salaün, G., Bultan, T.: Realizability of Choreographies Using Process Algebra Encodings. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 167–182. Springer, Heidelberg (2009)
Tanenbaum, A.: Computer Networks, 4th edn. Prentice Hall Professional Technical Reference (2002)
Udding, J.: Classification and Composition of Delay-Insensitive Circuits. Ph.D. thesis, Eindhoven University of Technology, Eindhoven (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beohar, H., Cuijpers, P.J.L. (2013). Avoiding Diamonds in Desynchronization. In: Păsăreanu, C.S., Salaün, G. (eds) Formal Aspects of Component Software. FACS 2012. Lecture Notes in Computer Science, vol 7684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35861-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-35861-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35860-9
Online ISBN: 978-3-642-35861-6
eBook Packages: Computer ScienceComputer Science (R0)