Edward Lee
Invited Talk by Edward A. Lee at the Integrated Formal Methods (iFM) conference, held virtually from Lugano, Switzerland, on Nov. 18 2020.
Abstract: Many formal verification techniques rely on the concept of system state and base the formalism on transitions between such states. In many systems, however, the concept of system state is poorly defined, particularly for parallel and distributed systems and for cyber-physical systems. In physics, the state of a system depends on the observer, and it is rare for a formal verification framework to clearly define what is an observer. In this talk, I will illustrate this problem with variants of the actor model, which is widely used for developing parallel and distributed software. I will focus on a more deterministic version of the actor model called Reactors (and an implementation language called Lingua Franca) and show that scalability of model checking depends heavily on how one defines the observer.
Source
