Abstract:Black-box runtime verification methods for cyber-physical systems can be used to discover errors in systems whose inputs and outputs are expressed as signals over time and their correctness requirements are specified in a temporal logic. Existing methods, such as requirement falsification, often focus on finding a single input that is a counterexample to system correctness. In this paper, we study how to create test generators that can produce multiple and diverse counterexamples for a single requirement. Several counterexamples expose system failures in varying input conditions and support the root cause analysis of the faults. We present the WOGAN algorithm to create such test generators automatically. The algorithm works by training iteratively a Wasserstein generative adversarial network that models the target distribution of the uniform distribution on the set of counterexamples. WOGAN is an algorithm that trains generative models that act as test generators for runtime verification. The training is performed online without the need for a previous model or dataset. We also propose criteria to evaluate such test generators. We evaluate the trained generators on several well-known problems including the ARCH-COMP falsification benchmarks. Our experimental results indicate that generators trained by the WOGAN algorithm are as effective as state-of-the-art requirement falsification algorithms while producing tests that are as diverse as a sample from uniform random sampling. We conclude that WOGAN is a viable method to produce test generators automatically and that these test generators can generate multiple and diverse counterexamples for the runtime verification of cyber-physical systems.
Abstract:We present the OGAN algorithm for automatic requirement falsification of cyber-physical systems. System inputs and output are represented as piecewise constant signals over time while requirements are expressed in signal temporal logic. OGAN can find inputs that are counterexamples for the safety of a system revealing design, software, or hardware defects before the system is taken into operation. The OGAN algorithm works by training a generative machine learning model to produce such counterexamples. It executes tests atomically and does not require any previous model of the system under test. We evaluate OGAN using the ARCH-COMP benchmark problems, and the experimental results show that generative models are a viable method for requirement falsification. OGAN can be applied to new systems with little effort, has few requirements for the system under test, and exhibits state-of-the-art CPS falsification efficiency and effectiveness.
Abstract:We propose an automatic approach to analyze the consistency and satisfiability of Unified Modeling Language UML models containing multiple class, object and statechart diagrams using logic reasoners for the Web Ontology Language OWL 2. We describe how to translate UML models in OWL 2 and we present a tool chain implementing this translation that can be used with any standard compliant UML modeling tool. The proposed approach is limited in scope, but is fully automatic and does not require any expertise about OWL 2 and its reasoners from the designer.
Abstract:WOGAN is an online test generation algorithm based on Wasserstein generative adversarial networks. In this note, we present how WOGAN works and summarize its performance in the SBST 2022 CPS tool competition concerning the AI of a self-driving car.
Abstract:We propose a novel online test generation algorithm WOGAN based on Wasserstein Generative Adversarial Networks. WOGAN is a general-purpose black-box test generator applicable to any system under test having a fitness function for determining failing tests. As a proof of concept, we evaluate WOGAN by generating roads such that a lane assistance system of a car fails to stay on the designated lane. We find that our algorithm has a competitive performance respect to previously published algorithms.
Abstract:We consider the problem of falsifying safety requirements of Cyber-Physical Systems expressed in signal temporal logic (STL). This problem can be turned into an optimization problem via STL robustness functions. In this paper, our focus is in falsifying systems with multiple requirements. We propose to solve such conjunctive requirements using online generative adversarial networks (GANs) as test generators. Our main contribution is an algorithm which falsifies a conjunctive requirement $\varphi_1 \land \cdots \land \varphi_n$ by using a GAN for each requirement $\varphi_i$ separately. Using ideas from multi-armed bandit algorithms, our algorithm only trains a single GAN at every step, which saves resources. Our experiments indicate that, in addition to saving resources, this multi-armed bandit algorithm can falsify requirements with fewer number of executions on the system under test when compared to (i) an algorithm training a single GAN for the complete conjunctive requirement and (ii) an algorithm always training $n$ GANs at each step.
Abstract:The Internet has become a prime subject to security attacks and intrusions by attackers. These attacks can lead to system malfunction, network breakdown, data corruption or theft. A network intrusion detection system (IDS) is a tool used for identifying unauthorized and malicious behavior by observing the network traffic. State-of-the-art intrusion detection systems are designed to detect an attack by inspecting the complete information about the attack. This means that an IDS would only be able to detect an attack after it has been executed on the system under attack and might have caused damage to the system. In this paper, we propose an end-to-end early intrusion detection system to prevent network attacks before they could cause any more damage to the system under attack while preventing unforeseen downtime and interruption. We employ a deep neural network-based classifier for attack identification. The network is trained in a supervised manner to extract relevant features from raw network traffic data instead of relying on a manual feature selection process used in most related approaches. Further, we introduce a new metric, called earliness, to evaluate how early our proposed approach detects attacks. We have empirically evaluated our approach on the CICIDS2017 dataset. The results show that our approach performed well and attained an overall 0.803 balanced accuracy.
Abstract:In this paper we present a novel algorithm for automatic performance testing that uses an online variant of the Generative Adversarial Network (GAN) to optimize the test generation process. The objective of the proposed approach is to generate, for a given test budget, a test suite containing a high number of tests revealing performance defects. This is achieved using a GAN to generate the tests and predict their outcome. This GAN is trained online while generating and executing the tests. The proposed approach does not require a prior training set or model of the system under test. We provide an initial evaluation the algorithm using an example test system, and compare the obtained results with other possible approaches. We consider that the presented algorithm serves as a proof of concept and we hope that it can spark a research discussion on the application of GANs to test generation.
Abstract:This paper explores the state of the art on to methods to verify and validate navigation algorithms for autonomous surface ships. We perform a systematic mapping study to find research works published in the last 10 years proposing new algorithms for autonomous navigation and collision avoidance and we have extracted what verification and validation approaches have been applied on these algorithms. We observe that most research works use simulations to validate their algorithms. However, these simulations often involve just a few scenarios designed manually. This raises the question if the algorithms have been validated properly. To remedy this, we propose the use of a systematic scenario-based testing approach to validate navigation algorithms extensively.