This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Reasoning About Places, Times, and Actions in the Presence of Mobility
April 1996 (vol. 22 no. 4)
pp. 225-247

Abstract—The current trend toward portable computing systems (e.g., cellular phones, laptop computers) brings with it the need for a new paradigm to facilitate thinking about and designing distributed applications. We use the term mobile to refer to distributed systems that include moving, autonomous agents which loosely cooperate to accomplish a task. The fluid nature of the interconnections among components of a mobile system provides new challenges and opportunities for the research community. While we do not claim to have fully grasped all the issues involved in specifying and modeling such systems, we believe that the notions of place, time, and action will play a central role in any model that is developed. In this paper, we show that these concepts can be expressed and reasoned about in the UNITY logic with a minimal amount of additional notation. The formal derivation of a control system for a radio-dispatched elevator is used to show how considerations involving place, time, and actions impact the design process, be it formal or semiformal.

[1] M. Abadi and L. Lamport, “An Old-Fashioned Recipe for Real Time,” Proc. REX Workshop, Real-Time Theory in Practice, pp. 1-27, June 1991.
[2] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
[3] T.A. Henzinger, Z. Manna, and A. Pnueli, "Timed Transition Systems," Real-Time: Theory in Practice, J.W. De Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, eds., Lecture Notes in Computer Science, vol. 600, pp. 226-251.Berlin: Springer-Verlag, 1991.
[4] S.S. Lam and A.U. Shankar, "A Relational Notation for State Transition Systems," IEEE Trans. Software Engineering, vol. 16, no. 7, pp. 755-775, 1990.
[5] L. Lamport and S. Owicki, "The Temporal Logic of Actions," ACM Trans. Programming Languages and Systems, vol. 16, pp. 872-923, May 994.
[6] N. Lynch and F. Vaandrager, "Forward and Backward Simulations for Timing-Based Systems," Real-Time: Theory in Practice, J.W. De Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, eds., Lecture Notes in Computer Science, vol. 600, pp. 397-446.Berlin: Springer-Verlag, 1991.
[7] N. Rescher and A. Urquhart, Temporal Logic.New York: Springer-Verlag, 1971.
[8] G.-C. Roman, R.F. Gamble, and W.E. Ball, "Formal Derivation of Rule-Based Programs," IEEE Trans. Software Engineering, vol. 19, no. 3, pp. 227-296, 1993.
[9] A.U. Shankar and S.S. Lam, "Time-Dependent Distributed Systems: Proving Safety, Liveness, and Real-Time Properties," Distributed Computing, vol. 2, pp. 61-79, 1987.
[10] M. Staskauskas, "Formal Derivation of Concurrent Programs: An example from Industry," IEEE Trans. Software Engineering, vol. 19, no. 5, pp. 503-528, 1993.

Index Terms:
Mobile computing, place, time, action, formal derivation, specification refinement, UNITY.
Citation:
C. Donald Wilcox, Gruia-Catalin Roman, "Reasoning About Places, Times, and Actions in the Presence of Mobility," IEEE Transactions on Software Engineering, vol. 22, no. 4, pp. 225-247, April 1996, doi:10.1109/32.491647
Usage of this product signifies your acceptance of the Terms of Use.