Formal development of actor programs using structured algebraic Petri nets

Abstract

This paper provides an actor semantics using a formalism called CO-OPN (Concurrent Object Oriented Petri Nets) which is modular and incorporates both concurrency and data structuring features. Actor languages are the main model of concurrent object-oriented languages, but they are rarely well formalized. CO-OPN is a structured extension of Petri nets and algebraic abstract data types. A CO-OPN specification is composed of a set of objects (algebraic abstract data types and Petri nets), and of a synchronous communication mechanism. This synchronization mechanism is defined in order to keep object state encapsulation, allowing the independent specification of each object. The translation of an actor program into a CO-OPN specification is done by building objects for actors. The adequacy of CO-OPN in describing the semantics of concurrent object-oriented languages is shown by this formal semantic description of actor languages. Some particular implementations are suggested, improving the concurrent execution of actor programs.