Abstract
The main purpose of our work is the typing of concurrent, distributed and mobile programs based on the actor programming model, that is non-uniform behaviour concurrent objects communicating by asynchronous message passing. One of the key difficulties is to give a precise definition of ”message not understood” errors in this context. In this paper, we investigate temporal logic and model-checking based technologies for an asynchronous message passing process calculi. We focus on non uniform input interfaces for processes, and then define a temporal logic tailored to their description and analyses. This logic deals with infinite-state systems, as mailboxes of actors are unbounded multisets of messages, but yet happens to be decidable. We use our logic to specify possible communication errors in actor-based programs in order to give precise and sound definition of type disciplines.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cardelli, L.: A theory of primitive objects: untyped and first-order systems. In: Proc. Theor. Aspects of Computer Software (1994)
Agha, G.: Actors: A model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)
Boudol, G.: Typing the use of resources in a concurrent calculus. In: Shyamasundar, R.K., Ueda, K. (eds.) ASIAN 1997. LNCS, vol. 1345, pp. 239–253. Springer, Heidelberg (1997)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Colaço, J.-L., Pantel, M., Dagnat, F., Sallé, P.: Static safety analysis for non-uniform service availability in actors. In: Proc. of FMOODS (February 1999)
Colaço, J.-L., Pantel, M., Sallé, P.: Cap: An actor dedicated process calculus. In: Prof. of Proof Theory of Concurrent Object- Oriented Programming (May 1996)
Colaço, J.-L., Pantel, M., Sallé, P.: A set-constraint-based analysis of actors. In: Proc. of FMOODS (July 1997)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: Symposium on Principles of Programming Languages, pp. 45–57 (2002)
Dagnat, F., Pantel, M., Colin, M., Sallé, P.: Typing concurrent objects and actors. L’Objet – Méthodes formelles pour les objets 6(1/2000), 83–106 (2000)
Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes (1995)
Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)
Fournet, C., Laneve, C., Maranget, L., Rémy, D.: Implicit typing à la ml for the join-calculus. In: Müller-Olm, M. (ed.) Modular Compiler Verification. LNCS, vol. 1283, pp. 196–212. Springer, Heidelberg (1997)
Hewitt, C., Bishop, P., Steiger, R.: A universal modular actor formalism for artificial intelligence. In: Proc. of Int. Joint Conference on Artificial Intelligence (1973)
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)
Kobayashi, N.: A partially deadloack-free typed process calculus. In: Proc. of the conf. Logi. In Computer Science (1997)
Milner, R.: The polyadic π-calculus: a tutorial. Technical Report ECSLFCS- 91-180, LFCS (1991)
Nierstrasz, O.: Regular types for active objects. In: Object-Oriented Software Composition, October 1995. ACM SIGPLAN Notices, pp. 99–121. Prentice Hall, New York (1995)
Najm, E., Nimour, A., Stefani, J.-B.: Infinite types for distributed object interfaces. In: Proc. of FMOODS (February 1999)
Pierce, B., Turner, D.: Pict: A programming languages based on the π-calculus. Technical Report 476, Indiana Univ. (March 1997)
Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Supercomputing, pp. 4–13 (1991)
Puntigam, F.: Type for active objects based on trace semantics. In: Proc. of FMOODS, pp. 5–20 (March 1996)
Rajamani, S.K., Rehof, J.: A behavioral module system for the pi-calculus. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, p. 375. Springer, Heidelberg (2001)
Ravara, A., Vasconcelos, V.T.: Typing non-uniform concurrent objects. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 474–488. Springer, Heidelberg (2000)
Walker, D.: Objects in the π-calculus. Information and Computation (116) (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Colin, M., Thirioux, X., Pantel, M. (2003). Temporal Logic Based Static Analysis for Non-uniform Behaviours. In: Najm, E., Nestmann, U., Stevens, P. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2003. Lecture Notes in Computer Science, vol 2884. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39958-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-39958-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20491-6
Online ISBN: 978-3-540-39958-2
eBook Packages: Springer Book Archive