Programming and Verifying Actor Systems in Rewriting Logic
摘要
Actors and rewriting logic were made for each other. This work explains the semantic relationship between both and describes research since 1990 at the intersection of both areas in topics such as: (i) software composition methods for distributed systems; (ii) formal verification of Actor systems; (iii) formal specification of probabilistic Actor systems and statistical model checking analysis of their qualitative properties; and (iv) automatic generation of correct-by-construction implementations of Actor system designs formally specified in the Maude rewriting logic language and verified in its formal tool environment.