Abstract
We introduce and study a process algebra able to model the systems composed of processes (agents) which may migrate within a distributed environment comprising a number of distinct locations. Two processes may communicate if they are present in the same location and, in addition, they have appropriate access permissions to communicate over a channel. Access permissions are dynamic, and processes can acquire new access permissions or lose some existing permissions while migrating from one location to another. Timing constraints coordinate and control both the communication between processes and migration between locations. We completely characterise those situations when a process is always guaranteed to possess safe access permissions. The consequences of such a result are twofold. First, we are able to validate systems where one does not need to check (at least partially) access permissions as they are guaranteed not to be violated, improving efficiency of implementation. Second, one can design systems in which processes are not blocked (deadlocked) because of the lack of dynamically changing access permissions.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ancona, D., Fagorzi, S., Zucca, E.: A Parametric Calculus for Mobile Open Code. ENTCS 192, 3–22 (2008)
Baeten, J., Bergstra, J.A.: Discrete Time Process Algebra: Absolute Time, Relative Time and Parametric Time. Fundamenta Informaticae 29, 51–76 (1997)
Berger, M.: Towards Abstractions For Distributed Systems Imperial College, Department of Computing (2002)
Bettini, L., Kannan, R., De Nicola, R., Ferrari, G.-L., Gorla, D., Loreti, M., Moggi, E., Pugliese, R., Tuosto, E., Venneri, B.: The klaim project: Theory and practice. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, pp. 88–150. Springer, Heidelberg (2003)
Bugliesi, M., Giunti, M.: Secure Implementations of Typed Channel Abstractions. In: Proc. of POPL, pp. 251–262. ACM, New York (2007)
Cardelli, L., Ghelli, G., Gordon, A.: Secrecy and Group Creation. Inf. Comput. 196, 127–155 (2005)
Chothia, T., Duggan, D., Vitek, J.: Type-based Distributed Access Control. In: Proc. of CSFW 2003, pp. 170–184. IEEE Computer Society, Los Alamitos (2003)
Ciobanu, G., Koutny, M.: Modelling and verification of timed interaction and migration. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 215–229. Springer, Heidelberg (2008)
Ciobanu, G., Koutny, M.: TiMoTy: Timed Mobility with Types of Formal Methods Laboratory Romanian Academy, Institute of Computer Science, Iasi (2010)
Ciobanu, G., Prisacariu, C.: Timers for Distributed Systems. ENTCS 164, 81–99 (2006)
Corradini, F., Ferrari, G.L., Pistore, M.: On the Semantics of Durational Actions. Theoretical Computer Science 269, 47–82 (2001)
Hennessy, M.: A Distributed π-calculus. Cambridge University Press, Cambridge (2007)
Hennessy, M., Riely, J.: Resource Access Control in Systems of Mobile Agents. Information and Computation 173, 82–120 (2002)
Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press, Cambridge (1999)
Sewell, P., et al.: Acute: High-Level Programming Language Design for Distributed Computation. Journal of Functional Programming 17, 547–612 (2007)
Thorn, T.: Programming Languages for Mobile Code. ACM Computing Surveys 29, 213–239 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciobanu, G., Koutny, M. (2011). Timed Migration and Interaction with Access Permissions. In: Butler, M., Schulte, W. (eds) FM 2011: Formal Methods. FM 2011. Lecture Notes in Computer Science, vol 6664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21437-0_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-21437-0_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21436-3
Online ISBN: 978-3-642-21437-0
eBook Packages: Computer ScienceComputer Science (R0)