This website provides the supplementary materials of the paper "MOSAIC: Model-based Safety Analysis Framework for AI-enabled Cyber-Physical Systems", which presents detailed research workflow and  experiment results not shown in the paper due to the page limit. The source code is available in the repository: https://anonymous.4open.science/r/mosaic-code-reviewed-FD6F/

The website is organized as follows:

• Home page: The motivation why the safety analysis for industrial-level AI-enabled CPS is urgently needed.

• Model Abstraction: We describe the model abstraction procedure.

• Safety Analysis: In this section, with the constructed abstract model, we describe the sebsequent safety analysis methods.

• Benchmark: This page contains the benchmark we perform experiment on.

• Experiment Setting: We gives details on the experimental evaluations on the proposed safety analysis framework 

• RQ1:Preciseness : In this page, we show the preciseness of the abstract model.

• RQ2: Monitoring : This page introduces the results of online safety monitoring.

• RQ3: Falsification: In this section, we describe the results of the proposed falsification method, which we aim to outperform existing state-of-the-art techniques on AI-CPS.

• RQ4: Overhead: We aim to assess the overhead introduced by the safety monitoring in the simulation.

Abstract

Cyber-physical systems (CPSs) are now widely deployed in many industrial domains, e.g., manufacturing systems and autonomous vehicles. To further enhance the capability and applicability of CPSs, there comes a recent trend from both academia and industry to utilize learning-based AI controllers for the system control process, resulting in an emerging class of AI-enabled cyber-physical systems (AI-CPSs). Although such AI-CPSs could achieve obvious performance enhancement from the lens of some key industrial requirement indicators, due to the random exploration nature and lack of systematic explanations for their behavior, such AI-based techniques also bring uncertainties and safety risks to the controlled system, posing an urgent need for effective safety analysis techniques for AI-CPSs. Hence in this work, we propose Mosaic, a model-based safety analysis framework for AI-CPSs. Mosaic first constructs a Markov decision process (MDP) model as an abstract model of the AI-CPS, which tries to characterize the behaviors of the original AI-CPS. Then, based on the derived abstract model, safety analysis is designed in two aspects: online safety monitoring and offline model-guided falsification. The usefulness of Mosaic is evaluated on diverse and representative industry-level AI-CPSs, the results of which demonstrate that Mosaic is effective in providing safety monitoring to AI-CPSs and enables to outperform the state-of-the-art falsification techniques, providing the basis for advanced safety analysis of AI-CPSs.

Research Workflow

First, as the preparation step, we simulate the AI-CPS under analysis and collect relevant data that includes the states and traces of the system, as well as their safety properties. Then, the collected data is used to build a Moore machine [16] that provides a suitable representation of the behaviors of the AI-CPS for further safety analysis. In practice, the state, input, and output representation spaces of such a Moore machine are often high-dimensional and continuous, which poses computational challenges in performing the safety analysis. Therefore, to address such a challenge, we pro- pose constructing an abstract model from the Moore machine as an MDP by using a four-level abstraction in terms of state, transi- tion, action and labeling. While preserving the representativeness of critical safety properties, such an abstract MDP model enables an ef- ficient analysis for AI-CPSs. Since the preciseness of the constructed abstract model is imperative for performing further analysis, there- fore, the first research question that we would like to investigate is, RQ1: How precise are the constructed abstract models?

Based on the constructed abstract MDP model, we further pro- pose safety analysis techniques from two directions: online safety monitoring and offline falsification. As the first direction, we pro- pose an online safety monitoring method that aims to increase the safety of the system while maintaining a similar performance of the original system. In particular, the monitoring module intelligently computes online safety predictions by observing the system status and performing PMC on the abstract MDP model. Then, according to the safety predictions, the actually applied controller is switched between the efficient AI-based controller and a predefined safety controller for keeping the AI-CPS safe. For examining, whether online safety monitoring is able to result in a safety improvement of AI-CPS while keeping a similar performance compared to the original system, we would like to investigate, RQ2: Can Mosaic provide effective safety monitoring? 

As the second direction, we further propose a novel offline model-guided falsification technique specially designed for AI-CPS. Falsification is a well-established safety validation technique that explores the CPS system behavior space to search for a counterexample that violates the specification. However, traditional falsification is ineffective in AI-CPS since it easily falls into the local optimum. To address this problem, we design and develop a novel falsifica-tion technique that combines global model-guided search and local optimization-based search to effectively detect counterexamples for AI-CPS. To assess whether the proposed technique is useful and outperforms existing state-of-the-art falsification techniques for AI-CPSs, we perform a comparative study to demonstrate, RQ3: Is Mosaic effective in guiding the falsification procedure? 

Furthermore, as an overall analysis, we would like to investigate how much overhead is introduced by safety monitoring. Hence, we record the time cost by the query and analyze its impact on the online safety monitoring process to examine the ratio of the time spent on the monitoring components and the whole simulation. This leads to another RQ that we would like to investigate, RQ4: How much overhead is introduced by the safety query in the analysis?