Verification of Actor Systems Needs Specification Techniques for Strong Causality and Hierarchical Reasoning

Date Added: Sep 2011
Format: PDF

Actor languages become increasingly popular for modeling and programming concurrent and distributed system. Although several foundational proof systems are available for actor systems, the authors claim that there is a need for higher-level specification and verification techniques. To clarify and substantiate this position, they introduce a simple actor language together with a non-trivial example and show how language-based specification techniques, generalizing ideas from object-oriented specifications, can provide more structure and modularity. They explain the semantics of the specification constructs based on strong causality relations of incoming and outgoing messages and illustrate their use.