Asynchronous Reactive Models – Event-based Analysis of Networks of Actors

Microsoft Research - Channel 9

Rebeca is designed for modeling and formal verification of asynchronous and reactive systems in 2001, and is supported by a model-checking tool, Afra. Followed by that, an actor-based family of languages are introduced to enable model driven development and provide a faithful and usable model for building distributed, asynchronous, and event-based systems. In Timed Rebeca, network and computational delays, periodic events, and required deadlines can be expressed in the model. Model checking and simulation tools are built based on the formal semantics of the language and its extensions. For deadlock-freedom and schedulability analysis special efficient techniques in state space exploration is proposed by exploiting the isolation of method execution in the model. I will show how these models can be used in safety assurance and performance evaluation of different systems, like Network on Chip Architectures, Sensor Network Applications, Traffic Control Systems, and Quadcopters. I show a general pattern in track-based traffic control systems, and a framework where self-adaptive actors are used to address self-adaptive traffic control systems.