Dr. Khouloud Gaaloul gave a research seminar in CIS

December 3, 2021

Dr. Khouloud Gaaloul, a post-doc in the CIS Department, gave a research seminar on verification of design models of cyber-physical systems

Dr. Khouloud Gaaloul, a post-doc in the CIS Department, gave a research seminar on verification of design models of cyber-physical systems. After receiving her Ph.D. from The University of Luxembourg, Dr. Gaaloul held the position of a post-doctoral researcher at The SnT Centre for Security, Reliability, and Trust, University of Luxembourg. She is currently a post-doc research fellow in the Computer and information Science Department at the University of Michigan - Dearborn. Her research interests include model-based software development and analysis of Cyber-Physical Systems, search-based testing and machine learning. She has been conducting her research in close collaboration with an industry partner in the aerospace sector.

Recent advances in cyber-physical systems (CPS) have allowed highly available technologies with interconnected systems between the physical assets and the computational software components. This has resulted in more complex systems with wider capabilities. For example, these systems can be applied in various domains such as safe transport, efficient medical devices, integrated systems and more. The development of such critical systems requires advanced new models, algorithms and tools to verify and validate the software components of the entire system.

The verification of cyber-physical systems has become challenging: (1) The complex and dynamic behavior of systems requires resilient automated monitors and test oracles that can cope with time-varying variables of CPS. (2) Given the wide range of existing verification and testing techniques from formal to empirical methods, there is no clear guidance as to how different techniques fare in the context of CPS. (3) Due to serious issues when applying exhaustive verification to complex systems, verifying system components separately has commonly been practiced. However, this practice requires adding implicit assumptions about the environment under which the system components operate, which is not trivial. My talk will focus on addressing these challenges in the context of the verification of design models of CPS specified in Simulink.

In this talk, Dr. Gaaloul presented (1) an automated approach to translate CPS requirements specified in a logic-based language into test oracles specified in Simulink. The generated oracles are able to deal with CPS complex behaviors and interactions with the system environment; (2) An empirical study to evaluate the fault-finding capabilities of model testing and model checking techniques for Simulink models. We also provide a categorization of model types and a set of common logical patterns for CPS requirements; (3) An automated approach to synthesize environment assumptions for a component under analysis by combining search-based testing, machine learning and model checking procedures. We also propose a novel technique to guide the test generation based on the feedback received from the machine learning process; and (4) An extension of (3) to learn more complex assumptions with arithmetic expressions over multiple signals and numerical variables.

Back to top of page