Abstract
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime. This allows to express a wide range of evolvability patterns for processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that at most k consecutive errors will arise in future states, the latter ensures that if the system enters into an error state then it will eventually reach a correct state. We study the (un)decidability of these two problems in different fragments of the calculus. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.
Supported by the French project ANR-2010-SEGI-013 - Aeolus, the EU integrated project HATS, the Fondation de Coopération Scientifique Digiteo Triangle de la Physique, and FCT / MCTES - Carnegie Mellon Portugal Program, grant NGN-44-2009-12 - Interfaces.
This is a preview of subscription content, log in via an institution to check access.
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
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109–127 (2000)
Acciai, L., Boreale, M.: Deciding safety properties in infinite-state pi-calculus via behavioural types. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 31–42. Springer, Heidelberg (2009)
Baeten, J., Bergstra, J.: Mode transfer in process algebra. Technical Report Report 00/01, Eindhoven University of Technology (2000)
Berger, M., Honda, K.: The two-phase commitment protocol in an extended pi-calculus. Electr. Notes Theor. Comput. Sci. 39(1) (2000)
Bravetti, M., Di Giusto, C., Pérez, J.A., Zavattaro, G.: Adaptable processes. Technical report, Univ. of Bologna, (2011), Draft, http://www.cs.unibo.it/~perez/ap/
Bravetti, M., Di Giusto, C., Pérez, J.A., Zavattaro, G.: Steps on the Road to Component Evolvability. Post-proceedings of FACS 2010. LNCS. Springer, Heidelberg (to appear, 2011)
Bravetti, M., Zavattaro, G.: On the expressive power of process interruption and compensation. Math. Struct. in Comp. Sci. 19(3), 565–599 (2009)
Bundgaard, M., Godskesen, J.C., Hildebrandt, T.: Bisimulation congruences for homer — a calculus of higher order mobile embedded resources. Technical Report TR-2004-52, IT University of Copenhagen (2004)
Busi, N., Gabbrielli, M., Zavattaro, G.: On the expressive power of recursion, replication and iteration in process calculi. Math. Struct. in Comp. Sci. 19(6), 1191–1222 (2009)
Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010)
Esparza, J.: Some applications of petri nets to the analysis of parameterised systems. Talk at WISP 2003 (2003)
Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. of LICS, pp. 352–359 (1999)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)
Francalanza, A., Hennessy, M.: A fault tolerance bisimulation proof for consensus (Extended abstract). In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 395–410. Springer, Heidelberg (2007)
Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture. Transactions of the American Mathematical Society 95(2), 210–225 (1960)
Milner, R.: Comunication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)
Nestmann, U., Fuzzati, R., Merro, M.: Modeling consensus in a process calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 399–414. Springer, Heidelberg (2003)
Pérez, J.A.: Higher-Order Concurrency: Expressiveness and Decidability Results. PhD thesis, University of Bologna (2010), Draft, http://www.japerez.phipages.com
Riely, J., Hennessy, M.: Distributed processes and location failures. Theor. Comput. Sci. 266(1-2), 693–735 (2001); An extended abstract appeared in Proc. of ICALP 1997
Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST–99–93, University of Edinburgh, Dept. of Comp. Sci. (1992)
Schmitt, A., Stefani, J.-B.: The kell calculus: A family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005)
Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)
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
Bravetti, M., Di Giusto, C., Pérez, J.A., Zavattaro, G. (2011). Adaptable Processes (Extended Abstract). In: Bruni, R., Dingel, J. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2011 2011. Lecture Notes in Computer Science, vol 6722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21461-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-21461-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21460-8
Online ISBN: 978-3-642-21461-5
eBook Packages: Computer ScienceComputer Science (R0)