Abstract
The actor model eases the definition of concurrent programs with non uniform behaviors. Static analysis of such a model was previously done in a data-flow oriented way, with type systems. This approach was based on constraint set resolution and was not able to deal with precise properties for communications of behaviors. We present here a new approach, control-flow oriented, based on the abstract interpretation framework, able to deal with communication of behaviors. Within our new analyses, we are able to verify most of the previous properties we observed as well as new ones, principally based on occurrence counting.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-34895-5_20
Chapter PDF
Similar content being viewed by others
References
Agha, G.: Actors: A model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)
Amtoft, T., Nielson, F., Nielson, H.R.: Type and behaviour reconstruction for higher-order concurrent programs. Journal of Functional Programming 7(3), 321–347 (1997)
Boudol, G.: Typing the use of resources in a concurrent calculus. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol. 1345, Springer, Heidelberg (1997)
Carrez, C., Fantechi, A., Najm, E.: Behavioural contracts for a sound composition of components. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, Springer, Heidelberg (2003)
Chaki, S., Rajamani, S., Rehof, J.: Types as models: model checking message-passing programs. In: Proc. of POPL 2002, ACM Press, New York (2002)
Colaço, J.-L., Pantel, M., Dagnat, F., Sallé, P.: Static safety analysis for non-uniform service availability in Actors . In: Proc. of FMOODS 1999, vol. 139, pp. 371–386. Kluwer, B.V, Dordrecht (1999)
Colaço, J.-L., Pantel, M., Sallé, P.: An actor dedicated process calculus. In: Proc. of the ECOOP 1996 Workshop on Proof Theory of Concurrent Object-Oriented Programming (1996)
Colaço, J.-L., Pantel, M., Sallé, P.: Static analysis of behavior changes in Actor languages. In: Object-Oriented Parallel and Distributed Programming, Hermès Science, 8, quai du Marché-Neuf, 75004 Paris, France, pp. 53–72 (2000)
Colin, M., Thirioux, X., Pantel, M.: Temporal logic based static analysis for non uniform behaviors. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 94–108. Springer, Heidelberg (2003)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc of POPL 1977, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Feret, J.: Occurrence counting analysis for the pi-calculus. In: Proc of the 1st Workshop on GEometry and Topology in COncurrency Theory. ENTCS, vol. 39.2, p. 2. Elsevier, Amsterdam (2001)
Feret, J.: Dependency analysis of mobile systems. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, Springer, Heidelberg (2002)
Feret, J.: Abstract interpretation of mobile systems. Journal of Logic and Algebraic Programming, special issue on pi-calculus 63.1 (2005)
Feret, J.: Analysis of Mobile Systems by Abstract Interpretation. PhD thesis, École polytechnique, Paris, France (February 2005)
Fournet, C., Lavene, C., Maranget, L., Rémy, D.: Implicit typing à la ml for the join-calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, Springer, Heidelberg (1997)
Garoche, P.-L.: Static analysis of actors by abstract interpretation. Master’s thesis, École Normale Suprieure de Cachan (2005)
Hennessy, M., Rathke, J., Yoshida, N.: Safedpi: a language for controlling mobile code. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 241–256. Springer, Heidelberg (2004)
Hewitt, C., Bishop, P., Steiger, R.: A universal modular actor formalism for artificial intelligence. In: Proc. of IJCAI 1973 (1973)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoretical Computer Science 311(1-3), 121–163 (2004)
Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)
Kobayashi, N.: A type system for lock-free processes. Information and Computation 177(2), 122–159 (2002)
Najm, E., Nimour, A., Stefani, J.-B.: Infinite types for distributed object interfaces. In: Proc. of FMOODS 1999, vol. 139, Kluwer, B.V, Dordrecht (1999)
Palsberg, J., O’Keefe, P.: A type system equivalent to flow analysis. In: Proc. of POPL 1995, pp. 367–378 (1995)
Parikh, R.: On context-free languages. Journal of the ACM 13(4), 570–581 (1966)
Puntigam, F.: Types for Active Objects based on Trace Semantics. In: Najm, E., et al. (eds.) Proc. of FMOODS 1996, Paris, France, Chapman & Hall, Boca Raton (1996)
Rajamani, S., Rehof, J.: A behavioral module system for the pi-calculus. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 375–394. Springer, Heidelberg (2001)
Ravara, A., Vasconcelos, V.: Typing non-uniform concurrent objects. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, Springer, Heidelberg (2000)
Venet, A.: Static Analysis of Dynamic Graph Strutures in Untyped Languages. PhD thesis, École polytechnique, Paris, France (December 1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Garoche, PL., Pantel, M., Thirioux, X. (2006). Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. In: Gorrieri, R., Wehrheim, H. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2006. Lecture Notes in Computer Science, vol 4037. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11768869_8
Download citation
DOI: https://doi.org/10.1007/11768869_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34893-1
Online ISBN: 978-3-540-34895-5
eBook Packages: Computer ScienceComputer Science (R0)