Mobile UNITY: reasoning and specification in mobile computing

ABSTRACT

Mobile computing represents a major point of departure from the traditional distributed-computing paradigm. The potentially very large number of independent computing units, a decoupled computing style, frequent disconnections, continuous position changes, and the location-dependent nature of the behavior and communication patterns present designers with unprecedented challenges in the areas of modularity and dependability. So far, the literature on mobile computing is dominated by concerns having to de with the development of protocols and services. This article complements this perspective by considering the nature of the underlying formal models that will enable us to specify and reason about such computations. The basic research goal is to characterize fundamental issues facing mobile computing. We want to achieve this in a manner analogous to the way concepts such as shared variables and message passing help us understand distributed computing. The pragmatic objective is to develop techniques that facilitate the verification and design of dependable mobile systems. Toward this goal we employ the methods of UNITY. To focus on what is essential, we center our study on ad hoc networks, whose singular nature is bound to reveal the ultimate impact of movement on the way one computes and communicates in a mobile environment. To understand interactions we start with the UNITY concepts of union and superposition and consider direct generalizations to transient interactions. The motivation behind the transient nature of the interactions comes from the fact that components can communicate with each other only when they are within a a certain range. The notation we employ is a highly modular extension of the UNITY programming notation. Reasoning about mobile computations relies on extensions to the UNITY proof logic.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, An Old-Fashioned Recipe for Real Time, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.1-27, June 03-07, 1991
• 2: BADRINATH, B. R. AND WELLING, G. 1995. Event delivery abstractions for mobile computing. Tech. Rep. LCSR-TR-242, Rutgers Univ., New Brunswick, N.J.
• 3: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 4: William D Clinger, Foundations of Actor Semantics, Massachusetts Institute of Technology, Cambridge, MA, 1981
• 5: JOHNSON, D.B. 1994. Routing in ad hoc networks of mobile hosts. In Proceedings of the Workshop on Mobile Computing Systems and Applications. IEEE Computer Society Press, Los Alamitos, Calif., 158-163.
• 6: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 7: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 8: MISRA, J. 1995. A logic for concurrent programming: Safety. J. Comput. Softw. Eng. 3, 2, 239-272.
• 9: NOBLE, B. D., PRICE, M., AND SATYANARAYANAN, M. 1995. A programming interface for application-aware adaptation in mobile computing. Comput. Syst. 8, 4, 345-363.
• 10: PERKINS, C. 1996. IP mobility support. Internet Draft Draft-IETF-Mobileip-16. Internet Engineering Task Force, Reston, Va. Available as ftp://ftp.ietf.cnri.reston.va.us/internetdrafts/draft-ietf-mobileip-protocol-16-txt.
• 11: Gruia-Catalin Roman , H. Conrad Cunningham, Reasoning About Synchronic Groups, Research Directions in High-Level Parallel Programming Languages, p.21-38, June 17-19, 1991
• 12: G. C. Roman , J. Y. Plun , C. D. Wilcox , S. Varma, Dynamic Synchrony Among Atomic Actions, IEEE Transactions on Parallel and Distributed Systems, v.4 n.6, p.677-685, June 1993 [doi>10.1109/71.242155]
• 13: SATYANARAYANAN, M., KISTLER, J. J., MUMMERT, L. B., EBLING, M. R., KUMAR, P., AND LU, Q. 1993. Experience with disconnected operation in a mobile computing environment. In Proceedings of the USENIX Symposium on Mobile and Location-Independent Computing. USENIX Assoc., Berkeley, Calif., 11-28.
• 14: SCHILIT, B. N., ADAMS, N., AND WANT, R. 1994. Context-aware computing applications. In Proceedings of the Workshop on Mobile Computing Systems and Applications. IEEE Computer Society Press, Los Alamitos, Calif., 85-90.
• 15: TAIT, C. D. AND DUCHAMP, D. 1992. An efficient variable consistency replicated file service. In Proceedings of the USENIX File Systems Workshop. USENIX Assoc., Berkeley, Calif., 111-126.
• 16: D. B. Terry , M. M. Theimer , Karin Petersen , A. J. Demers , M. J. Spreitzer , C. H. Hauser, Managing update conflicts in Bayou, a weakly connected replicated storage system, ACM SIGOPS Operating Systems Review, v.29 n.5, p.172-182, Dec. 3, 1995
• 17: VOELKER, G. M. AND BERSHAD, B.N. 1994. Mobisaic: An information system for a mobile wireless computing environment. In Proceedings of the Workshop on Mobile Computing Systems and Applications. IEEE Computer Society Press, Los Alamitos, Calif., 185-190.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Reliability, Theory, Verification

Keywords:
formal methods, mobile UNITY, mobile computing, shared variables, synchronization, transient interactions, weak consistency