TECoSA seminar – Engineering Nondeterminism: Towards Trustworthy Cyber-Physical Systems  

TECoSA Seminar with Marjan Sirjani, Mälardalen University and KTH, will take place on Sept 10.

Zoom-link for the seminar is : https://kth-se.zoom.us/j/66857695267

Abstract: Distributed cyber-physical systems such as autonomous vehicles, industrial controllers, and collaborative robots must operate correctly despite the uncertainties in the system and environment. In this talk, I show how we use nondeterminism as the basis for modeling and analyzing uncertainty caused by concurrency, timing variations, faults, attacks, dynamic environments, and AI components. I present our work on combining formal verification, model-based analysis, and runtime monitoring for assuring trustworthiness of distributed systems.

We use the actor-based modeling language Rebeca and its model checking toolset. This lets us capture asynchronous and real-time behavior and analyze safety, timing, and fault-tolerance properties. We model uncertainty explicitly, verify against the specification at design time, and use the verified model to monitor and shield the system at runtime. I show how this approach uncovered subtle inconsistencies in distributed redundant controller algorithms. In one case, verification exposed a fault-handling bug in a protocol already believed correct. I also show how our verification approach can guide systematic test design. I then present our work on runtime monitoring, anomaly detection and shielding, using a lightweight “Tiny Twin” 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, and an affiliated professor at KTH, Sweden. 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).