By Marjan Sirjani
On 19 June at 2 pm, in FC6 029, Marjan Sirjani will give a lecture entitled ‘Formal Verification and Runtime Assurance of Distributed Cyber-Physical Systems’.
Title:
Formal Verification and Runtime Assurance of Distributed Cyber-Physical Systems
Abstract:
Distributed cyber-physical systems such as autonomous vehicles, industrial controllers, and collaborative robots must operate correctly despite concurrency, timing uncertainty, faults, and dynamic environments. In this talk, I will present our work on combining formal verification, model-based analysis, and runtime assurance for trustworthy distributed systems. Using the actor-based modeling language Rebeca and its verification toolset, we model asynchronous and real-time behavior and analyze safety, timing, and fault-tolerance properties. I will illustrate how formal modeling helped us identify subtle inconsistencies in distributed redundant controller algorithms and how verification results can guide systematic test design. I will also present our recent work on runtime monitoring and anomaly detection using lightweight “Tiny Twin” digital twins derived automatically from formally verified models. The talk concludes with reflections on scalability, abstraction, and the role of formal methods in building resilient and dependable cyber-physical systems.
Bio:
Marjan Sirjani is a Professor at Mälardalen University, Sweden, where she leads the Cyber-Physical Systems Analysis research group. Her research focuses on formal methods for software engineering, particularly modeling and verification of concurrent, distributed, timed, and cyber-physical systems. She is one of the pioneers behind Rebeca, an actor-based modeling language with formal verification support, and has contributed extensively to model checking, compositional verification, and state-space reduction techniques for actor-based systems (https://rebeca-lang.org/). Her current work addresses safety, security, runtime assurance, and resilience of autonomous and cyber-physical systems. Marjan has served as program committee member and chair for numerous international conferences, including SEFM, iFM, FM, FMICS, Coordination, SAC, FSEN, and DATE, and is an editor of the journal Science of Computer Programming.
From June 2026, she serves as the leader of the research profile Trustworthy Smart Systems (TSS) at Mälardalen University (https://sites.mdu.se/tss).