Reference : Verification of design models of cyber-physical systems specified in Simulink
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Verification of design models of cyber-physical systems specified in Simulink
Gaaloul, Khouloud mailto [University of Luxembourg > Faculty of Science, Technology and Medecine (FSTM) > >]
University of Luxembourg, ​Luxembourg, ​​Luxembourg
Docteur en Informatique
Nejati, Shiva mailto
Briand, Lionel mailto
Pastore, Fabrizio mailto
Menghi, Claudio mailto
Gay, Gregory mailto
Gurfinkel, Arie mailto
[en] Cyber-Physical Systems ; Model-Based Verification ; search-based testing ; Model checking ; machine learning
[en] Recent advances in cyber-physical systems (CPS) have allowed highly available and approachable 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, they 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. In this dissertation, we focus on addressing these challenges. In this dissertation, we propose 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 more complex assumptions with arithmetic expressions over multiple signals and numerical variables.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
BRIDGES18/IS/12632261 ; The European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 694277) ; NSERC of Canada under the Discovery and CRC programs
The European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme
Researchers ; Professionals ; Students
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

Open access
thesis_final.pdfAuthor postprint4.69 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.