This Article 
 Bibliographic References 
 Add to: 
Compositional Programming Abstractions for Mobile Computing
February 1998 (vol. 24 no. 2)
pp. 97-110

Abstract—Recent advances in wireless networking technology and the increasing demand for ubiquitous, mobile connectivity demonstrate the importance of providing reliable systems for managing reconfiguration and disconnection of components. Design of such systems requires tools and techniques appropriate to the task. Many formal models of computation, including UNITY, are not adequate for expressing reconfiguration and disconnection and are, therefore, inappropriate vehicles for investigating the impact of mobility on the construction of modular and composable systems. Algebraic formalisms such as the π-calculus have been proposed for modeling mobility. This paper addresses the question of whether UNITY, a state-based formalism with a foundation in temporal logic, can be extended to address concurrent, mobile systems. In the process, we examine some new abstractions for communication among mobile components that express reconfiguration and disconnection and which can be composed in a modular fashion.

[1] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
[2] M. Staskauskas, "Formal Derivation of Concurrent Programs: An example from Industry," IEEE Trans. Software Engineering, vol. 19, no. 5, pp. 503-528, 1993.
[3] R. Milner, J. Parrow, and D. Walker, “A Calculus of Mobile Processes,” Information and Computation, vol. 100, pp. 1-77, 1992.
[4] W.D. Clinger, "Foundations of Actor Semantics," Technical Report AI-TR-633, MIT Artificial Intelligence Laboratory, 1981.
[5] G. Agha, ACTORS: A Model of Concurrent Computation in Distributed Systems, MIT Press, Cambridge, Mass., 1986.
[6] R.M. Amadio, "An Asynchronous Model of Locality, Failure, and Process Mobility," Coordination Languages and Models, pp. 374-391.Berlin: Springer-Verlag, 1997.
[7] J. Riely and M. Hennessy, "Distributed Processes and Location Failures," Technical Report 2/97, Computer Science, School of Cognitive and Computing Sciences, Univ. of Sussex, Brighton, England, 1997.
[8] C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, and D. Rémy, "A Calculus of Mobile Agents," Proc. Int'l Conf. Concurrency Theory. Lecture Notes in Computer Science 1,119, pp. 406-421. Springer-Verlag, 1996.
[9] M. Satyanarayanan, J.J. Kistler, L.B. Mummert, M.R. Ebling, P. Kumar, and Q. Lu, "Experience with Disconnected Operation in a Mobile Computing Environment," Proc. USENIX Symp. Mobile and Location-Independent Computing,Cambridge, Mass., pp. 11-28, 1993.
[10] D.B. Terry, M.M. Theimer, K. Petersen, A.J. Demers, M.J. Spreitzer, and C.H. Hauser, Managing Update Conflicts in a Weakly Connected Replicated Storage System Proc. ACM Symp. Operating Systems Principles, 1995.
[11] G.M. Voelker and B.N. Bershad, "Mobisaic: An Information System for a Mobile Wireless Computing Environment," Proc. Workshop Mobile Computing Systems and Applications,Santa Cruz, Calif., pp. 185-190, IEEE, 1994.
[12] B.N. Schilit, N. Adams, and R. Want, “Context-Aware Computing Applications,” Proc. IEEE Workshop Mobile Computing Systems and Applications, Dec. 1994.
[13] C. Perkins, "IP Mobility Support," RFC 2002, IETF Network Working Group, 1996.
[14] P.J. McCann and G.-C. Roman, "Mobile UNITY Coordination Constructs Applied to Packet Forwarding for Mobile Hosts," Coordination Languages and Models, Lecture Notes in Computer Science 1,282, pp. 338-354.Berlin: Springer-Verlag, 1997.
[15] F. Orava and J. Parrow, "An Algebraic Verification of a Mobile Network," R91:02, Swedish Inst. of Computer Science, 1991.
[16] B. Sanders, B. Massingill, and S. Kryukova, "Specification and Proof of an Algorithm for Location Management for Mobile Communication Devices," Proc. Int'l Workshop Formal Methods for Parallel Programming: Theory and Applications,Geneva, IPPS '97, Apr. 1997.
[17] G.-C. Roman, P.J. McCann, and Jerome Y. Plun, "Mobile UNITY: Reasoning and Specification in Mobile Computing," ACM TOSEM, vol. 6, no. 3, pp. 250-282, July 1997.
[18] J. Misra, "A Logic for Concurrent Programming: Safety," J. Computer and Software Eng., vol. 3, no. 2, pp. 239-272, 1995.
[19] J. Misra, "A Logic for Concurrent Programming: Progress," J. Computer and Software Eng., vol. 3, no. 2, pp. 273-300, 1995.
[20] C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969.
[21] M.J. Fischer, N.A. Lynch, and M.S. Paterson, “Impossibility of Distributed Consensus with One Faulty Process,” J. ACM, vol. 32, no. 2, pp. 374i–382, 1985.
[22] T.J. Chaney and C.E. Molnar, "Anomalous Behavior of Synchronizer and Arbiter Circuits," IEEE Trans. Computers, vol. 22, no. 4, pp. 421-422, 1973.
[23] C.A.R. Hoare,“Communicating sequential processes,” Comm. of the ACM, vol. 21, no. 8, pp. 666-677, Aug. 1978.
[24] N.A. Lynch and M.R. Tuttle, "An Introduction to Input/Output Automata," CWI Quarterly, vol. 2, no. 3, pp. 219-246, 1989.
[25] R. Kurki-Suonio, "Fundamentals of Object-Oriented Specification and Modeling of Collective Behaviors," Object-Oriented Behavioral Specifications, H. Kilov and W. Harvey, eds., pp. 101-120. Kluwer Academic, 1996.
[26] D. Dolev, C. Dwork, and L. Stockmeyer, “On the Minimal Syncrhony Needed for Distributed Consensus,” J. ACM, vol. 34, no. 1, pp. 77–97, Jan. 1987.
[27] G.-C. Roman, J.Y. Plun, and C.D. Wilcox, "Dynamic Synchrony Among Atomic Actions," IEEE Trans. Parallel and Distributed Systems, vol. 4, no. 6, pp. 677-685, 1993.

Index Terms:
Formal methods, mobile computing, Mobile UNITY, weak consistency, shared variables, synchronization, transient interactions.
Peter J. McCann, Gruia-Catalin Roman, "Compositional Programming Abstractions for Mobile Computing," IEEE Transactions on Software Engineering, vol. 24, no. 2, pp. 97-110, Feb. 1998, doi:10.1109/32.666824
Usage of this product signifies your acceptance of the Terms of Use.