- author = "Khouloud Gaaloul",
- title = "Verification of Design Models of Cyber-Physical Systems Specified in Simulink",
- school = "Faculty of Science, Technology and Medicine (FSTM), University of Luxembourg",
- year = "2021",
- address = "Luxembourg",
- month = "15 " # sep,
- keywords = "genetic algorithms, genetic programming, SBSE, SBST, Security, Reliability and Trust, Cyber-Physical Systems, Model-Based Verification, search-based testing, Model checking, machine learning",
-
URL = "
https://wwwfr.uni.lu/snt/news_events/phd_defense_verification_of_design_models_of_cyber_physical_systems_specified_in_simulink",
-
URL = "http://hdl.handle.net/10993/48071",
-
URL = "
https://orbilu.uni.lu/bitstream/10993/48071/1/thesis_final.pdf",
- size = "131 pages",
-
abstract = "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. CPS can be applied in various domains
such as safe transport, efficient medical devices,
integrated systems, critical infrastructure control and
more. The development of such critical systems requires
advanced new models, algorithms, methods and tools to
verify and validate the software components and the
entire system.
The verification of cyber-physical systems has become challenging: (1) The complex and dynamical behaviour 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, a common practice is needed to verify system components separately. This requires adding implicit assumptions about the operational environment of system components to ensure correct verification. However, identifying environment assumptions for cyber-physical systems with complex, mathematical behaviors is not trivial.
I focus on addressing these challenges by proposing a set of effective approaches to verify design models of CPS. The work presented in this dissertation is motivated by ESAIL maritime micro-satellite system, developed by LuxSpace, a leading provider of space systems, applications and services in Luxembourg. In addition to ESAIL, we use a benchmark of eleven public-domain Simulink models provided by Lockheed Martin, which are representative of different categories of CPS models in the aerospace and defence sector.
To address the aforementioned challenges, we propose (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 behaviours 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 assumptions with arithmetic expressions over multiple signals and numerical variables.",
-
notes = "Combining Genetic Programming and Model Checking to
Generate Environment Assumptions
SVV
Supervisor: Shiva Nejati and Lionel Briand",
