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
ASCII Text
x 
 
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.
 
 
BibTex
x
 
@article{ 10.1109/32.491647,
author = {C. Donald Wilcox and Gruia-Catalin Roman},
title = {Reasoning About Places, Times, and Actions in the Presence of Mobility},
journal ={IEEE Transactions on Software Engineering},
volume = {22},
number = {4},
issn = {0098-5589},
year = {1996},
pages = {225-247},
doi = {http://doi.ieeecomputersociety.org/10.1109/32.491647},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Reasoning About Places, Times, and Actions in the Presence of Mobility
IS - 4
SN - 0098-5589
SP225
EP247
EPD - 225-247
A1 - C. Donald Wilcox,
A1 - Gruia-Catalin Roman,
PY - 1996
KW - Mobile computing
KW - place
KW - time
KW - action
KW - formal derivation
KW - specification refinement
KW - UNITY.
VL - 22
JA - IEEE Transactions on Software Engineering
ER -
 

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.