Speaker: Shuling Wang
Abstract: Simulink is widely used in the design of safety-critical embedded systems, including avionics and automotive applications. In this talk, we first present a formal semantic foundation for a core subset of Simulink by defining both denotational and operational semantics. The denotational semantics offers a mathematical interpretation of the diagram’s input-output behavior, faithfully capturing its hierarchical structure. In contrast, the operational semantics specifies the concrete execution of Simulink diagrams, resolving block execution order, solving continuous dynamics, and coordinating hybrid discrete-continuous interactions. Both semantics have been fully formalized in Isabelle/HOL, and we have established their consistency by proving the existence and uniqueness of the denotational semantics. Furthermore, to facilitate application, we developed a translator that automatically converts Simulink graphical diagrams into their Isabelle representation. Our formal semantics supports the rigorous analysis of Simulink diagram properties, as demonstrated by a PID control example. In the second part of this talk, we present how to define a verified numerical semantics for Simulink diagrams, from which we get a certified implementation.
Bio: Shuling Wang is an Associate Professor at the Institute of Software, Chinese Academy of Sciences. She obtained her Ph.D. from Peking University and completed postdoctoral research at the United Nations University International Institute for Software Technology. Her research focuses on formal methods for safety-critical software systems, including formal modeling and verification of cyber-physical systems and embedded systems, operating systems verification, large language model-assisted program verification, and interactive theorem proving.