Search

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.

GUI is a bridge connecting user and application. Existing GUI testing tasks can be categorized into two groups: functionality testing and compatibility testing. While the functionality testing focuses on detecting application runtime bugs, the compatibility testing aims at detecting bugs resulting from device or platform difference. To automate testing procedures and improve testing efficiency, previous works have proposed dozens of tools. To evaluate these tools, in functionality testing, researchers have published testing benchmarks. Comparatively, in compatibility testing, the question of ``Do existing methods indeed effectively assist test cases replay?'' is not well answered. To answer this question and advance the related research in GUI compatibility testing, we propose a benchmark of GUI compatibility testing. In our experiments, we compare the replay success rate of existing tools. Based on the experimental results, we summarize causes which may lead to ineffectiveness in test case replay and propose opportunities for improving the state-of-the-art.

Deep neural networks (DNNs) are widely developed and applied in many areas, and the quality assurance of DNNs is critical. Neural network verification (NNV) aims to provide formal guarantees to DNN models. Similar to traditional software, neural network verifiers could also contain bugs, which would have a critical and serious impact, especially in safety-critical areas. However, little work exists on validating neural network verifiers. In this work, we propose DeepGalaxy, an automated approach based on differential testing to tackle this problem. Specifically, we (1) propose a line of mutation rules, including model level mutation and specification level mutation, to effectively explore the two-dimensional input space of neural network verifiers; and (2) propose heuristic strategies to select test cases. We leveraged our implementation of DeepGalaxy to test three state-of-the-art neural network verifies, Marabou, Eran, and Neurify. The experimental results support the efficiency and effectiveness of DeepGalaxy. Moreover, five unique unknown bugs were discovered

Reactive systems are composed of a well defined set of input events that the system reacts with by executing an associated handler to each event. In concurrent environments, event handlers can interact with the execution of other programs such as hardware interruptions in preemptive systems, or other instances of the reactive system in multicore architectures. State of the art rely-guarantee based verification frameworks only focus on imperative programs, being difficult to capture in the rely and guarantee relations interactions with possible infinite sequences of event handlers, and the input arguments to event handlers. In this paper, we propose the formalisation in Isabelle/HOL of an event-based rely-guarantee approach for concurrent reactive systems. We develop a Pi-Core language which incorporates a concurrent imperative and system specification language by `events', and we build a rely-guarantee proof system for Pi-Core and prove its soundness. Our approach can deal with multicore and interruptible concurrency. We use two case studies to show this: an interruptible controller for stepper motors and an ARINC 653 multicore kernel, and prove the functional correctness and preservation of invariants of them in Isabelle/HOL., 15 pages, 6 figures, 1 table

Deep learning (DL) defines a new data-driven programming paradigm where the internal system logic is largely shaped by the training data. The standard way of evaluating DL models is to examine their performance on a test dataset. The quality of the test dataset is of great importance to gain confidence of the trained models. Using an inadequate test dataset, DL models that have achieved high test accuracy may still lack generality and robustness. In traditional software testing, mutation testing is a well-established technique for quality evaluation of test suites, which analyzes to what extent a test suite detects the injected faults. However, due to the fundamental difference between traditional software and deep learning-based software, traditional mutation testing techniques cannot be directly applied to DL systems. In this paper, we propose a mutation testing framework specialized for DL systems to measure the quality of test data. To do this, by sharing the same spirit of mutation testing in traditional software, we first define a set of source-level mutation operators to inject faults to the source of DL (i.e., training data and training programs). Then we design a set of model-level mutation operators that directly inject faults into DL models without a training process. Eventually, the quality of test data could be evaluated from the analysis on to what extent the injected faults could be detected. The usefulness of the proposed mutation testing techniques is demonstrated on two public datasets, namely MNIST and CIFAR-10, with three DL models., he 29th IEEE International Symposium on Software Reliability Engineering (ISSRE 2018)

Deep learning (DL) has achieved remarkable progress over the past decade and been widely applied to many safety-critical applications. However, the robustness of DL systems recently receives great concerns, such as adversarial examples against computer vision systems, which could potentially result in severe consequences. Adopting testing techniques could help to evaluate the robustness of a DL system and therefore detect vulnerabilities at an early stage. The main challenge of testing such systems is that its runtime state space is too large: if we view each neuron as a runtime state for DL, then a DL system often contains massive states, rendering testing each state almost impossible. For traditional software, combinatorial testing (CT) is an effective testing technique to reduce the testing space while obtaining relatively high defect detection abilities. In this paper, we perform an exploratory study of CT on DL systems. We adapt the concept in CT and propose a set of coverage criteria for DL systems, as well as a CT coverage guided test generation technique. Our evaluation demonstrates that CT provides a promising avenue for testing DL systems. We further pose several open questions and interesting directions for combinatorial testing of DL systems.

Separation kernels provide temporal/spatial separation and controlled information flow to their hosted applications. They are introduced to decouple the analysis of applications in partitions from the analysis of the kernel itself. More than 20 implementations of separation kernels have been developed and widely applied in critical domains, e.g., avionics/aerospace, military/defense, and medical devices. Formal methods are mandated by the security/safety certification of separation kernels and have been carried out since this concept emerged. However, this field lacks a survey to systematically study, compare, and analyze related work. On the other hand, high-assurance separation kernels by formal methods still face big challenges. In this paper, an analytical framework is first proposed to clarify the functionalities, implementations, properties and standards, and formal methods application of separation kernels. Based on the proposed analytical framework, a taxonomy is designed according to formal methods application, functionalities, and properties of separation kernels. Research works in the literature are then categorized and overviewed by the taxonomy. In accordance with the analytical framework, a comprehensive analysis and discussion of related work are presented. Finally, four challenges and their possible technical directions for future research are identified, e.g. specification bottleneck, multicore and concurrency, and automation of full formal verification., Comment: 35 pages, 5 figures, 13 tables

Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automated manner. Furthermore, we propose the first automated approach to checking rely-guarantee based simulations between infinite state concurrent programs. We have prototyped our algorithms and applied our tool to the verification of multiple refinements.

Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 has been complied with by mainstream separation kernels. Security of functionalities defined in ARINC 653 is thus very important for the development and certification of separation kernels. This paper presents the first effort to formally specify and verify separation kernels with ARINC 653 channel-based communication. We provide a reusable formal specification and security proofs for separation kernels in Isabelle/HOL. During reasoning about information flow security, we find some security flaws in the ARINC 653 standard, which can cause information leakage, and fix them in our specification. We also validate the existence of the security flaws in two open-source ARINC 653 compliant separation kernels., 17 pages, 4 figures