Universiteit Leiden

nl en

Proefschrift

Actors at work

Promotor: F.S. de Boer Co-promotor: P. T. de Gouw

Auteur
Behrooz Nobakht
Datum
15 december 2016
Links
Thesis in Leiden Repository

The core contributions of this thesis target the intersection of object orientation, actor model, and concurrency. We choose Java as the main target programming language and as one of the mainstream object-oriented languages. We formalize a subset of Java and its concurrency API to facilitate formal verification and reasoning about it. We create an abstract mapping from a concurrent-object modeling language, ABS, to the programming semantics of concurrent Java. We provide the formal semantics of the mapping and runtime properties of the concurrency layer including deadlines and scheduling policies. We provide an implementation of the ABS concurrency layer as a Java API library and framework utilizing the latest language additions in Java 8.