Verification of Actor Systems Needs Specification Techniques for Strong Causality and Hierarchical Reasoning
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.