"Our world has become a network of connected software systems, communicating with each other, and controlling physical systems. Large scale Systems of Cyber-Physical Systems (SCPS) emerge, where entities interact with the physical environment, communicate through networks and are coordinated over a distributed infrastructure. Soon we will see autonomous cars whooshing around, interoperable medical devices monitoring and controlling the health of patients and collaborating robots interacting with humans without separating fences. These systems are generally heterogenous and dynamic, with critical timing properties. In this talk, I will present our approach for formal verification and runtime monitoring of such interoperable systems and analysis of their timing properties. We use an easy-to-use actor-based language, Rebeca, with formal verification support. I will reflect on how we used this language and its toolset for timing analysis and safety assurance of different systems, such as Network on Chip architectures, sensor network applications, network protocols, and medical interoperable systems.

"