We present a novel framework for formal control of uncertain discrete-time switched stochastic systems against probabilistic reach-avoid specifications. In particular, we consider stochastic systems with additive noise, whose distribution lies in an ambiguity set of distributions that are ε − close to a nominal one according to the Wasserstein distance. For this class of systems we derive control synthesis algorithms that are robust against all these distributions and maximize the probability of satisfying a reach-avoid specification, defined as the probability of reaching a goal region while being safe. The framework we present first learns an abstraction of a switched stochastic system as a robust Markov decision process (robust MDP) by accounting for both the stochasticity of the system and the uncertainty in the noise distribution. Then, it synthesizes a strategy on the resulting robust MDP that maximizes the probability of satisfying the property and is robust to all uncertainty in the system. This strategy is then refined into a switching strategy for the original stochastic system. By exploiting tools from optimal transport and stochastic programming, we show that synthesizing such a strategy reduces to solving a set of linear programs, thus guaranteeing efficiency. We experimentally validate the efficacy of our framework on various case studies, including both linear and non-linear switched stochastic systems. Our results represent the first formal approach for control synthesis of stochastic systems with uncertain noise distribution.
In real world applications, uncertain parameters are the rule rather than the exception. We present a reachability algorithm for linear systems with uncertain parameters and inputs using set propagation of polynomial zonotopes. In contrast to previous methods, our approach is able to tightly capture the non-convexity of the reachable set. Building up on our main result, we show how our reachability algorithm can be extended to handle linear time-varying systems as well as linear systems with time-varying parameters. Moreover, our approach opens up new possibilities for reachability analysis of linear time-invariant systems, nonlinear systems, and hybrid systems. We compare our approach to other state of the art methods, with superior tightness on two benchmarks including a 9-dimensional vehicle platooning system.
DNN-based Adaptive Cruise Control (ACC) systems are very convenient but also safety critical. Although prior work has explored physical adversarial attacks on DNN models, those attacks are mostly static and their effects on a real-world ACC system are not clear. In this work, we propose the first end-to-end attack on ACC systems, and we test the safety indication on the state-of-the-art ACC products. The experimental results show that our approach can make the vehicle driving with ACC accelerate unsafely and cause a rear-end collision.
State-of-the-art industrial IoT solutions struggle to handle applications in which timing is important and deterministic event ordering is crucial. We illustrate this on the basis of a simple parking lot occupancy sensing use case that is easy to explain but virtually impossible to implement using commercially available IoT infrastructure. In this paper, we compare an implementation using AWS IoT Core against one using Lingua Franca, a time-centric coordination language for constructing deterministic concurrent and distributed reactive software. Our preliminary evaluation shows that Lingua Franca can reliably address our use case.
Cyber-physical systems (CPSs) are complex systems comprised of computational processes, communication networks, and elements interacting with the physical world. The design of the CPSs involves many domain-specific tools and design flows created by engineers with diverse domain knowledge. As the scale of the systems increases, the heterogeneity nature of CPS design prolongs the CPS design process, making exhaustive design-space exploration infeasible. The symbiotic design methodology, in which the designers interact with optimization tools during the design process, is therefore promising to facilitate the design process by performing design exploration in a properly restricted design space. We present a symbiotic design methodology, which explores the design space iteratively and optimizes the system by exploiting the collaboration between designers and tools. The optimization tools perform the design space exploration, while the human designers use their expertise to guide the exploration by restricting the design space. Experimental results based on a robot car configuration problem and an unmanned aerial vehicle design problem show that the methodology can efficiently and effectively discover unconventional designs while optimizing the design objectives.
In the paper titled " Stealthy attacks formalized as STL formulas for Falsification of CPS Security", we investigate a broad class of attacks on the sensor and actuation blocks in the form of additive perturbation that impacts the measurement and control, respectively. In this demo, we demonstrate the usage of our framework and the underlying technologies along with a case study on aviation systems using Microsoft Flight Simulator (MSFS).
This paper introduces CAN to ROS, a model-based code generation tool used in development, testing, and deployment of a heterogeneous fleet of vehicles with robotic sensing in ROS. Code generation supports two main features: (1) self-configuration for deployment in a heterogeneous vehicle fleet, and (2) quick iteration for testing and development of reading vehicle sensors and robotic control. This tool features the ability to detect the vehicle it is in and regenerate and rebuild itself at runtime to provide the proper two-way bridge between ROS and the sensed on-board vehicle sensor network. Code generation relies on a per-model defined JSON to map a CAN database (DBC) to the desired ROS topic names and message types. The live ROS publishing of CAN messages allows for instant feedback, and the code regeneration allows for adjustments in DBC or vehicle JSON to iteratively hone in on new vehicle signals. Generated ROS nodes are written in C++ for runtime use in lightweight embedded computers. This has been tested in vehicles from three different Original Equipment Manufacturers (OEMs), and can be extended to support a wide array of vehicles. By using a unifying ROS specification, a heterogeneous set of vehicles can be unified into a fleet with abstracted model-specific details; this opens the door for developing cross-model software applications for vehicle control, connected vehicle applications, or fleet monitoring systems.
The paper presents early work on LetSynchronise, an open-source framework that aims to facilitate research and collaboration on Logical Execution Time (LET) systems. It offers a web application for modelling, simulating, analysing, and optimising LET systems, which can be extended via user-defined plugins for the rapid prototyping of scheduling policies, timing analysers, and optimisation algorithms. Its capabilities are demonstrated through use cases and a small research case study.
Complex software systems often feature distinct modes of operation, each designed to handle a particular scenario that may require the system to respond in a certain way. Breaking down system behavior into mutually exclusive modes and discrete transitions between modes is a commonly used strategy to reduce implementation complexity and promote code readability. The work in this paper aims to bring the advantages of working with modal models to mainstream programming languages, by following the polyglot coordination approach of Lingua Franca (LF), in which verbatim target code (e. g., C, C++, Python, Typescript, or Rust) is encapsulated in composable reactive components called reactors. Reactors can form a dataflow network, are triggered by timed as well as sporadic events, execute concurrently, and can be distributed across nodes on a network. With modal models in LF, we introduce a lean extension to the concept of reactors that enables the coordination of reactive tasks based on modes of operation.
Recently, the number of security threats targeting cyber-physical systems has continued to increase, both in quantity and in sophistication. Modern signature-based Intrusion Detection Systems (IDSs) are no longer able to keep up to date with the most recent attack techniques. This gives rise to the need for an intelligent system that is able to learn the expected network traffic and to detect not only known but also novel attacks. This paper introduces a novel autoencoder-based IDS that can detect new malicious packets with high precision. The proposed technique is general and can be used to detect a wide range of attacks, including unseen ones. Extensive experiments in simulation and on real hardware show that our technique substantially outperforms state-of-the-art solutions in terms of detection accuracy and generality. An analysis of the inference times is presented to show the predictability of the detection mechanism, as well as its practical applicability in resource-constrained edge devices.
In this work, we propose a safety-guaranteed personalization for autonomous vehicles by incorporating Signal Temporal Logic (STL) into preference learning problem. We propose a new variant of STL called Parametric Weighted Signal Temporal Logic with a new quantitative semantics, namely weighted robustness. Given a set of pairwise preferences, and by using gradient-based optimization methods, we learn a set of valuations for weights that reflect preferences such that preferred ones have greater weighted robustness value than their non-preferred matches. Traditional STL formulas fail to incorporate preferences due its complex nature. Our initial results with data from a human-subject on an intersection with stop sign driving scenario, in which the participant is asked their preferred driving behavior from pairs of vehicle trajectories, indicate that we can learn a new weighted STL formula that captures preferences while also encoding correctness.
Cyber-Physical Systems (CPS) require seamless integration of physical and computation components through communication networks. They often contain sub-systems from different physical domains (e.g., electrical, mechanical, and electronic) that must coordinate over a communications network to achieve a joint function. Thus, network characteristics significantly affect CPS performance and must be accurately modeled and simulated. However, simulation efforts are often siloed into specific domains (e.g., manufacturing, transportation, and electric grid) due to the level of complexity required to simulate even one domain. Co-simulation standards such as the IEEE High Level Architecture (HLA) attempt to facilitate model sharing between domains through definition of common services such as time management on a shared message bus. However, a well-developed, integrated, and configurable network simulation component that can be readily deployed in CPS co-simulations is lacking due to both the network simulation complexity and customization needed for specific domains. This paper presents a novel approach to create a highly reusable and configurable network simulation for HLA co-simulations which includes a cyber-attack library for analyzing behavior of CPS under attack. This work could provide effective means to quickly develop cyber scenarios for analyzing CPS through networked co-simulations.
This paper summarizes the recent developments of hamiltorch,1 which is a PyTorch-based library for Hamiltonian Monte Carlo (HMC). HMC is a gradient-based Markov chain Monte Carlo technique that has favorable scaling properties to high-dimensional parameter spaces, leading to it often becoming the sampling method of choice when derivatives are available. HMC is therefore especially suited to performing Bayesian inference over neural networks (NN). As a result hamiltorch has been specifically developed to sample from PyTorch NN models. The development of hamiltorch has also led to new sampling schemes that are part of the library. In this paper I will highlight such novelties as well as provide a brief introduction to the features of hamiltorch and highlight its use-cases in recently referenced work.
In recent years, research on the detection and mitigation of non-line-of-sight (NLOS) conditions in the context of ultra-wideband ranging has received increasing attention. As a result, numerous statistical and machine learning methods have been proposed, and a selection of datasets has been made available to the community. In an attempt to benchmark the performance of state-of-the-art NLOS classification and error correction techniques on a newly-built ultra-wideband testbed at our premises, we have observed how reusing publicly-available datasets and applying existing solutions is a complex and error-prone task. Indeed, a multitude of minor details in the selection, pre-processing, collection, labeling, and blending of datasets can have a profound impact on the correctness of the employed methods and on the achieved performance. In this paper, we summarize the lessons we have learned, pointing out potential pitfalls and distilling a few recommendations for researchers and practitioners approaching this research domain.
Big data and data scientific applications in the modern agriculture are rapidly evolving as the data technology advances and more computational power becomes available. The adoption of big data has enabled farmers and producers to optimize their agricultural activities sustainably with cutting-edge technologies, resulting in eco-friendly and efficient farming. Wireless sensor networks and machine learning have had a direct impact on smart and precision agriculture, with deep learning techniques applied to data collected via sensor nodes. Additionally, internet of things, drones, and robotics are being incorporated into farming techniques. Digital data handling has amplified the information wave, and information and communication technology have been used to deliver benefits to both farmers and consumers. This work highlights the technological implications and challenges that arise in data-driven agricultural practices as well as the research problems that need to be solved.
Open-source software (OSS) is a critical element in the design and operation of complex cyber-physical systems. Contributions to OSS projects are typically the result of voluntary work and time allocation by researchers, software developers, hackers, and even opportunistic programmers. These communities often operate on a "trust" basis, and although they strive to evaluate the technical correctness and merits of contributed code, the processes they use are usually loosely supervised. Social rules, trust, reputation, and even arcane processes often govern these communities. While these components have undoubtedly contributed to the growth and expansion of OSS, they could also lead to opportunities for subversion [3], hindering the reliability of an OSS project. This, in turn, could not only compromise the integrity of cyber-physical systems depending on OSS but also affect their performance.
Ultra-wideband (UWB) technology has become very popular for indoor positioning and distance estimation (DE) systems due to its decimeter-level accuracy achieved when using time-of-flight-based techniques. Techniques for DE relying on signal strength (DESS) received less attention. As a consequence, existing benchmarks consist of simple channel characterizations rather than methods aiming to increase accuracy. Further development in DESS may enable lower-cost transceivers to applications that can afford lower accuracies than those based on time-of-flight. Moreover, it is a fundamental building block used by a recently proposed approach that can enable security against cyberattacks to DE which could not be avoided using only time-of-flight-based techniques. In this paper, we aim to benchmark the performance of machine-learning models when used to increase the accuracy of UWB-based DESS. Additionally, aiming for implementation in commercial off-the-shelf (COTS) transceivers, we propose and evaluate an approach to resolve ambiguities compromising DESS in these devices. Our results show that the proposed DE approaches have sub-decimeter accuracy when testing the models in the same environment and positions in which they have been trained, and achieved an average MAE of 24 cm when tested in a different environment. 3 datasets obtained from our experiments are made publicly available.
Program execution tracing is an important technique in software development and analysis. However, noninvasively obtaining cycle-level traces for modern low-power ARMv7-M-based SoCs is challenging, because convenient off-the-shelf high-speed tracing probes are expensive and cannot be applied to SoCs that lack high-speed debug components, notably Embedded Trace Macrocell (ETM) and parallel tracing port (PTP). To address this issue, in this work, we present FrankenTrace, a technique for generating full, noninvasive, cycle-level program counter traces and full, cycle-level data transfer traces of varying invasiveness on SoCs with only low-speed debug components, namely Debug Watchpoint and Trace unit (DWT), Instrumentation Trace Macrocell (ITM), Single Wire Output (SWO), and an inexpensive probe. We demonstrate the technique by tracing software running on a node of the 1KT testbed.
Computer simulation models are used extensively in scientific and engineering problems for complex design tasks and decision processes. Surrogate models generated using data-driven techniques can approximate the behavior of complex simulation models with high fidelity and can accelerate the design process. This paper presents a physics-guided learning architecture that integrates parameters extracted from physics-based simulations into the intermediate layers of a neural network to constrain the learning process during the training of surrogate models and to improve their generalization. The proposed architecture is used to develop a surrogate model for evaluating the structural integrity of the hull of an unmanned underwater vehicle. It is shown that physics-guided learning can improve generalization in less explored regions of the design space compared to black-box models. In addition, the architecture improves the explainability of the model predictions using physics-based parameters and allows the designer to make decisions based on the input and physics-based intermediate parameters.
