Formal Development of Actor Programs using Structured Algebraic Petri Nets
This paper provides with 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. These synchronisation mechanism are defined in order to keep object state encapsulation, allowing to specify independantly 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 to describe the semantics of concurrent object oriented languages is shown by this formal semantic description of actor languages. Some particular implementations are suggested, improving the concurrency of executions of actor programs.
Keywords : Specification and verification, Formal program development methodologies, modular specification, semantics, actor languages semantics, high level Petri nets, algebraic abstract data types.
Record created on 2005-09-20, modified on 2016-08-08