Model checking of distributed real-time cyber-physical systems (DCPSs) is an inherently hard problem due to asynchronous communication, network delays, clock skews, as well as the state explosion caused by the system’s concurrency. PALS (“Physically Asynchronous, Logically Synchronous”) is a design pattern that drastically reduces the design and verification complexity of CPSs when the network infrastructure between the system components can guarantee bounds on the messaging delays and local clock skews. This presentation proposes a new method to verify PALS-compliant CPSs: first, we model them in Lingua Franca, and then we use the LF-mc verifier to check the properties of the model. As a case study to validate the efficiency of our approach, we analyze a PALS-compliant airplane control system, with ongoing work focused on comparing our approach against other model-checking methods for PALS-compliant CPSs. Upon completion, this method is intended to be integrated into the LF-mc tool for verifying CPSs specified in Lingua Franca.
Short Bio:
Casiana Monica Popovici is a first-year PhD student at the West University of Timișoara, where she also teaches Formal Languages and Automata Theory. Her research focuses on rule-based programming for the formal verification of hardware and software systems. Casiana holds a Bachelor’s Degree in Computer Science from the West University of Timișoara and a Master of Research in Bioinformatics from Imperial College London. Her master’s research culminated in her first academic publication, followed by a second publication in collaboration with the OncoGen Research Centre.
