Search

With ever-expanding computation and communication capabilities of modern embedded platforms, Internet of Things (IoT) technologies enable development of Reconfigurable Manufacturing Systems---a new generation of highly modularized industrial equipment suitable for highly-customized manufacturing. Sequential control in these systems is largely based on discrete events, while their formal execution semantics is specified as Control Interpreted Petri Nets (CIPN). Despite industry-wide use of programming languages based on the CIPN formalism, formal verification of such control applications in the presence of adversarial activity is not supported. Consequently, in this paper we focus on security-aware modeling and verification challenges for CIPN-based sequential control applications. Specifically, we show how CIPN models of networked industrial IoT controllers can be transformed into Time Petri Net (TPN)-based models, and composed with plant and security-aware channel models in order to enable system-level verification of safety properties in the presence of network-based attacks. Additionally, we introduce realistic channel-specific attack models that capture adversarial behavior using nondeterminism. Moreover, we show how verification results can be utilized to introduce security patches and motivate design of attack detectors that improve overall system resiliency, and allow satisfaction of critical safety properties. Finally, we evaluate our framework on an industrial case study.

Deep brain stimulation (DBS) has shown great promise toward treating motor symptoms caused by Parkinson's disease (PD), by delivering electrical pulses to the Basal Ganglia (BG) region of the brain. However, DBS devices approved by the U.S. Food and Drug Administration (FDA) can only deliver continuous DBS (cDBS) stimuli at a fixed amplitude; this energy inefficient operation reduces battery lifetime of the device, cannot adapt treatment dynamically for activity, and may cause significant side-effects (e.g., gait impairment). In this work, we introduce an offline reinforcement learning (RL) framework, allowing the use of past clinical data to train an RL policy to adjust the stimulation amplitude in real time, with the goal of reducing energy use while maintaining the same level of treatment (i.e., control) efficacy as cDBS. Moreover, clinical protocols require the safety and performance of such RL controllers to be demonstrated ahead of deployments in patients. Thus, we also introduce an offline policy evaluation (OPE) method to estimate the performance of RL policies using historical data, before deploying them on patients. We evaluated our framework on four PD patients equipped with the RC+S DBS system, employing the RL controllers during monthly clinical visits, with the overall control efficacy evaluated by severity of symptoms (i.e., bradykinesia and tremor), changes in PD biomakers (i.e., local field potentials), and patient ratings. The results from clinical experiments show that our RL-based controller maintains the same level of control efficacy as cDBS, but with significantly reduced stimulation energy. Further, the OPE method is shown effective in accurately estimating and ranking the expected returns of RL controllers., Accepted to International Conference on Cyber Physical Systems (ICCPS) 2023

Pioneers of autonomous vehicles (AVs) promised to revolutionize the driving experience and driving safety. However, milestones in AVs have materialized slower than forecast. Two culprits are (1) the lack of verifiability of proposed state-of-the-art AV components, and (2) stagnation of pursuing next-level evaluations, e.g., vehicle-to-infrastructure (V2I) and multi-agent collaboration. In part, progress has been hampered by: the large volume of software in AVs, the multiple disparate conventions, the difficulty of testing across datasets and simulators, and the inflexibility of state-of-the-art AV components. To address these challenges, we present AVstack, an open-source, reconfigurable software platform for AV design, implementation, test, and analysis. AVstack solves the validation problem by enabling first-of-a-kind trade studies on datasets and physics-based simulators. AVstack solves the stagnation problem as a reconfigurable AV platform built on dozens of open-source AV components in a high-level programming language. We demonstrate the power of AVstack through longitudinal testing across multiple benchmark datasets and V2I-collaboration case studies that explore trade-offs of designing multi-sensor, multi-agent algorithms.

Sensing technology, as well as cloud communication, is enabling the development of closed-loop deep brain stimulation (DBS) for Parkinson's disease. The accelerometer is a practical sensor that can provide information about the disease/health state of the patient as well as physical activity levels, all of which in the long-term can provide feedback information to an adaptive closed-loop control algorithm for more effective and personalized DBS therapy. In this paper, we present for the first time, acceleration streamed from Medtronic's RC+S device in patients with Parkinson's disease while at home, and compare it to accel-eration acquired concurrently from the patient's Apple Watch. We examined correlation between the accelerometer signals at varying time scales. We also compared the spectral band power obtained from the two accelerometers. While there was an average correlation of 0.37 for subject 1 and 0.50 for subject 2 between the two acceleration signals on a time scale of 10 minutes, the correlation was lower for shorter time scales on the order of seconds. There was greater spectral power in the Parkinsonian tremor band of 4-7 Hz for the externally worn accelerometer than the internal accelerometer, but the internal accelerometer showed greater relative power distributed in the higher frequencies (7-30 Hz). Thus, based on this preliminary analysis, we expect that the internal accelerometer may be used to assess patient activity and state for closed loop DBS but tremor detection may require more sophisticated signal processing. Furthermore, the internal accelerometer may contain information in higher frequency bands that reveal information about the patient state. Clinical relevance - Closed-loop DBS is expected to improve patient outcomes for the tens of thousands of Parkinson's disease patients using DBS [1], [2]. Eliminating an additional external device in order to implement closed-loop adaptive deep brain stimulation would benefit DBS patients however an understanding of what information is lost by doing so is needed to justify the ultimate design of closed-loop DBS.

Multivariate time series (MTS) classification is a challenging and important task in various domains and real-world applications. Much of prior work on MTS can be roughly divided into neural network (NN)- and pattern-based methods. The former can lead to robust classification performance, but many of the generated patterns are challenging to interpret; while the latter often produce interpretable patterns that may not be helpful for the classification task. In this work, we propose a reinforcement learning (RL) informed PAttern Mining framework (RLPAM) to identify interpretable yet important patterns for MTS classification. Our framework has been validated by 30 benchmark datasets as well as real-world large-scale electronic health records (EHRs) for an extremely challenging task: sepsis shock early prediction. We show that RLPAM outperforms the state-of-the-art NN-based methods on 14 out of 30 datasets as well as on the EHRs. Finally, we show how RL informed patterns can be interpretable and can improve our understanding of septic shock progression.

Industrial Internet of Things (IIoT) represents a backbone of modern reconfigurable manufacturing systems (RMS), which enable manufacturing of a high product variety through rapid and easy reconfiguration of manufacturing equipment. In IIoT-enabled RMS, modular equipment is built from smart devices, each performing its own tasks, whereas the global functioning is achieved through their networking and intensive communication. Although device communication contributes to the system reconfigurability, it also opens up new security challenges due to potential vulnerability of communication links. In this article, we present security analysis for a major part of RMS in which manufacturing equipment is sequentially controlled and can be modeled as discrete event systems (DES). Control distribution within DES implies communication of certain events between smart modules. Specifically, in this work, we focus on attacks on communication of these events. In particular, we develop a method for modeling such attacks, including event insertion and removal attacks, in distributed sequential control; the method is based on the supervisory control theory framework. We show how the modeled attacks can be detected and provide a method for identification of communication links that require protection to avoid catastrophic damage of the system. Finally, we illustrate and experimentally validate applicability of our methodology on a real-world industrial case study with reconfigurable manufacturing equipment.

A digital microfluidic biochip (DMFB) enables miniaturization of immunoassays, point-of-care clinical diagnostics, and DNA sequencing. A recent generation of DMFBs uses a micro-electrode-dot-array (MEDA) architecture, which provides fine-grained control of droplets and real-time droplet sensing using the CMOS technology. However, microelectrodes in a MEDA biochip degrade when they are charged and discharged frequently during bioassay execution. In this article, we first make the key observation that the droplet-sensing operations contribute up to 94% of all microelectrode actuation in MEDA. Consequently, to reduce the number of droplet-sensing operations, we present a new microelectrode cell (MC) design as well as a selective-sensing method such that only a small fraction of microelectrodes perform droplet sensing during bioassay execution. The selection of microelectrodes that need to perform the droplet sensing is based on an analysis of experimental data. A comprehensive set of simulation results show that the total number of droplet-sensing operations is reduced to only 0.7%, which prolongs the lifespan of a MEDA biochip by $11\times $ without any impact on bioassay time-to-response.

Recent trends in manufacturing require the use of reconfigurable equipment that facilitates rapid and cost-effective change of functionality through modular design, which supports fast integration. Intelligent devices (e.g., sensors, actuators) with integrated computation and communication capabilities enable high-level modularity, not only with the respect to hardware components but also in terms of control functionality; this can be achieved by distributing control to different network-connected devices. Thus, to enable fast and reliable system reconfigurations, in this brief, we introduce a method for distribution of control tasks and generation of control code for the devices in the control network. Our approach is based on the control interpreted Petri nets (CIPNs) formalism. We start from a CIPN capturing the centralized (overall) control system, and the mapping of input and output signals to local controllers (LCs) (i.e., smart devices) that have direct physical access to system sensors and actuators. From these, our method automatically designs distributed control tasks for LCs in the network, as well as generates control code for each LC. The applicability of the proposed method is experimentally verified on two real-world case studies.

An increasingly relevant security issue for unmanned aerial vehicles (UAVs, also known as drones) is the possibility of a global positioning system (GPS) spoofing attack. Given the existing problems in current GPS spoofing detection techniques and human visual advantages in searching and localizing targets, we propose a human-autonomy collaborative approach of human geo-location to assist UAV control systems in detecting GPS spoofing attacks. An interactive testbed and experiment were designed and used to evaluate this approach, which demonstrated that human-autonomy collaborative hacking detection is a viable concept. Using the hidden Markov model (HMM) approach, operator behavior patterns and strategies from the experiment were modeled via hidden states and transitions among them. These models revealed two dominant hacking detection strategies. Statistical results and expert performer evaluations show no significant difference between different hacking detection strategies in terms of correct detection. The detection strategy model suggests areas of future research in decision support tool design for UAV hacking detection. Also, the development of HMMs presents the feasibility of quantitatively investigating operator behavior patterns and strategies in human supervisory control scenarios.

Many important properties of cyber-physical systems (CPS) are defined upon the relationship between multiple executions simultaneously in continuous time. Examples include probabilistic fairness and sensitivity to modeling errors (i.e., parameters changes) for real-valued signals. These requirements can only be specified by hyperproperties . In this article, we focus on verifying probabilistic hyperproperties for CPS. To cover a wide range of modeling formalisms, we first propose a general model of probabilistic uncertain systems (PUSs) that unify commonly studied CPS models such as continuous-time Markov chains (CTMCs) and probabilistically parametrized Hybrid I/O Automata (P 2 HIOA). To formally specify hyperproperties, we propose a new temporal logic, hyper probabilistic signal temporal logic (HyperPSTL) that serves as a hyper and probabilistic version of the conventional signal temporal logic (STL). Considering the complexity of real-world systems that can be captured as PUSs, we adopt a statistical model checking (SMC) approach for their verification. We develop a new SMC technique based on the direct computation of significance levels of statistical assertions for HyperPSTL specifications, which requires no a priori knowledge on the indifference margin. Then, we introduce SMC algorithms for HyperPSTL specifications on the joint probabilistic distribution of multiple paths, as well as specifications with nested probabilistic operators quantifying different paths, which cannot be handled by existing SMC algorithms. Finally, we show the effectiveness of our SMC algorithms on CPS benchmarks with varying levels of complexity, including the Toyota Powertrain Control System.

In system analysis, conformance indicates that two systems simultaneously satisfy the same set of specifications of interest; thus, the results from analyzing one system automatically transfer to the other, or one system can safely replace the other in practice. In this work, we study the probabilistic conformance of cyber-physical systems (CPS). We propose a notion of (approximate) probabilistic conformance for sets of complex specifications expressed by the Signal Temporal Logic (STL). Based on a novel statistical test, we develop the first statistical verification methods for the probabilistic conformance of a wide class of CPS. Using this method, we verify the conformance of the startup time of the widely-used full and simplified model of Toyota powertrain systems, the settling time of model-predictive-control-based and neural-network-based automotive lane-keeping controllers, as well as the maximal voltage deviation of full and simplified power grid systems.

A digital microfluidic biochip (DMFB) enables the miniaturization of immunoassays, point-of-care clinical diagnostics, and DNA sequencing. A recent generation of DMFBs uses a micro-electrode-dot-array (MEDA) architecture, which provides fine-grained control of droplets and real-time droplet sensing using CMOS technology. However, microelectrodes in a MEDA biochip can degrade due to charge trapping when they are repeatedly charged and discharged during bioassay execution; such degradation leads to the failure of microelectrodes and erroneous bioassay outcomes. To address this problem, we first introduce a new microelectrode-cell design such that we can obtain the health status of all the microelectrodes in a MEDA biochip by employing the inherent sensing mechanism. Next, we present a stochastic game-based model for droplet manipulation, and a formal synthesis method for droplet routing that can dynamically change droplet transportation routes. This adaptation is based on the real-time health information obtained from microelectrodes. Comprehensive simulation results for four real-life bioassays show that our method increases the likelihood of successful bioassay completion with negligible impact on time-to-results.

Network-based attacks on control systems may alter sensor data delivered to the controller, effectively causing degradation in control performance. As a result, having access to accurate state estimates, even in the presence of attacks on sensor measurements, is of critical importance. In this paper, we analyze performance of resilient state estimators (RSEs) when any subset of sensors may be compromised by a stealthy attacker. Specifically, we consider systems with the well-known l0-based RSE and two commonly used sound intrusion detectors (IDs). For linear time-invariant plants with bounded noise, we define the notion of perfect attackability (PA) when attacks may result in unbounded estimation errors while remaining undetected by the employed ID (i.e., stealthy). We derive necessary and sufficient PA conditions, showing that a system can be perfectly attackable even if the plant is stable. While PA can be prevented with the use the standard cryptographic mechanisms (e.g.,message authentication) that ensure data integrity under network-based attacks, their continuous use imposes significant communication and computational overhead. Consequently, we also study the impact that even intermittent use of data authentication has on RSE performance guarantees in the presence of stealthy attacks. We show that if messages from some of the sensors are even intermittently authenticated, stealthy attacks could not result in unbounded state estimation errors., 12 pages, 7 figures, submitted to Journal

In this paper, we propose a Deep Imitative Q-learning (DIQL) method to synthesize control policies for mobile robots that need to satisfy Linear Temporal Logic (LTL) specifications using noisy semantic observations of their surroundings. The robot sensing error is modeled using probabilistic labels defined over the states of a Labeled Transition System (LTS) and the robot mobility is modeled using a Labeled Markov Decision Process (LMDP) with unknown transition probabilities. We use existing product-based model checkers (PMCs) as experts to guide the Q-learning algorithm to convergence. To the best of our knowledge, this is the first approach that models noise in semantic observations using probabilistic labeling functions and employs existing model checkers to provide suboptimal instructions to the Q-learning agent.

The use of Neural Network (NN)-based controllers has attracted significant attention in recent years. Yet, due to the complexity and non-linearity of such NN-based cyber-physical systems (CPS), existing verification techniques that employ exhaustive state-space search, face significant scalability challenges; this effectively limits their use for analysis of real-world CPS. In this work, we focus on the use of Statistical Model Checking (SMC) for verifying complex NN-controlled CPS. Using an SMC approach based on Clopper-Pearson confidence levels, we verify from samples specifications that are captured by Signal Temporal Logic (STL) formulas. Specifically, we consider three CPS benchmarks with varying levels of plant and controller complexity, as well as the type of considered STL properties - reachability property for a mountain car, safety property for a bipedal robot, and control performance of the closed-loop magnet levitation system. On these benchmarks, we show that SMC methods can be successfully used to provide high-assurance for learning-based CPS.

Parkinson’s disease (PD) currently Influences around one million people in the US. Deep brain stimulation (DBS) is a surgical treatment for the motor symptoms of PD that delivers electrical stimulation to the basal ganglia (BG) region of the brain. Existing commercial DBS devices employ stimulation based only on fixed-frequency periodic pulses. While such periodic high-frequency DBS controllers provide effective relief of PD symptoms, they are very inefficient in terms of energy consumption, and the lifetime of these battery- operated devices is limited to 4 years. Furthermore, fixed high- frequency stimulation may have side effects, such as speech impairment. Consequently, there is a need to move beyond (1) fixed stimulation pulse controllers, and (2) ‘one-size-fits- all’ patient-agnostic treatments, to provide energy efficient and effective (in terms of relieving PD symptoms) DBS controllers. In this work, we introduce a deep reinforcement learning (RL)- based approach that can derive patient-specific DBS patterns that are both effective in reducing a model-based proxy for PD symptoms, as well as energy-efficient. Specifically, we model the BG regions as a Markov decision process (MDP), and define the state and action space as state of the neurons in the BG regions and the stimulation patterns, respectively. Thereafter, we define the reward functions over the state space, and the learning objective is set to maximize the accumulated reward over a finite horizon (i.e., the treatment duration), while bounding average stimulation frequency. We evaluate the performance of our methodology using a Brain-on-Chip (BoC) FPGA platform that implements the physiologically-relevant basal ganglia model (BGM). We show that our RL-based DBS controllers significantly outperform existing fixed frequency controllers in terms of energy efficiency (e.g., by using 70% less energy than common periodic controllers), while providing suitable reduction of model-based proxy for PD symptoms.

We study the problem of synthesizing control strategies for Linear Temporal Logic (LTL) objectives in unknown environments. We model this problem as a turn-based zero-sum stochastic game between the controller and the environment, where the transition probabilities and the model topology are fully unknown. The winning condition for the controller in this game is the satisfaction of the given LTL specification, which can be captured by the acceptance condition of a deterministic Rabin automaton (DRA) directly derived from the LTL specification. We introduce a model-free reinforcement learning (RL) methodology to find a strategy that maximizes the probability of satisfying a given LTL specification when the Rabin condition of the derived DRA has a single accepting pair. We then generalize this approach to LTL formulas for which the Rabin condition has a larger number of accepting pairs, providing a lower bound on the satisfaction probability. Finally, we illustrate applicability of our RL method on two motion planning case studies.

Feed-forward neural networks (FNNs) work as standard building blocks in applying artificial intelligence (AI) to the physical world. They allow learning the dynamics of unknown physical systems (e.g., biological and chemical) {to predict their future behavior}. However, they are likely to violate the physical constraints of those systems without proper treatment. This work focuses on imposing two important physical constraints: monotonicity (i.e., a partial order of system states is preserved over time) and stability (i.e., the system states converge over time) when using FNNs to learn physical dynamics. For monotonicity constraints, we propose to use nonnegative neural networks and batch normalization. For both monotonicity and stability constraints, we propose to learn the system dynamics and corresponding Lyapunov function simultaneously. As demonstrated by case studies, our methods can preserve the stability and monotonicity of FNNs and significantly reduce their prediction errors.

We consider the problem of security-aware planning in an unknown stochastic environment, in the presence of attacks on control signals (i.e., actuators) of the robot. We model the attacker as an agent who has the full knowledge of the controller as well as the employed intrusion-detection system and who wants to prevent the controller from performing tasks while staying stealthy. We formulate the problem as a stochastic game between the attacker and the controller and present an approach to express the objective of such an agent and the controller as a combined linear temporal logic (LTL) formula. We then show that the planning problem, described formally as the problem of satisfying an LTL formula in a stochastic game, can be solved via model-free reinforcement learning when the environment is completely unknown. Finally, we illustrate and evaluate our methods on two robotic planning case studies.

In this paper, we introduce the context-aware probabilistic temporal logic (CAPTL) that provides an intuitive way to formalize system requirements by a set of PCTL objectives with a context-based priority structure. We formally present the syntax and semantics of CAPTL and propose a synthesis algorithm for CAPTL requirements. We also implement the algorithm based on the PRISM-games model checker. Finally, we demonstrate the usage of CAPTL on two case studies: a robotic task planning problem, and synthesizing error-resilient scheduler for micro-electrode-dot-array digital microfluidic biochips.

In this work, we study supervisory control of discrete event systems in the presence of network-based attacks on information delivered to and from the supervisors. The attacks are modeled by finite state transducers (FSTs), having the ability to nondeterministically rewrite a word to any word of a regular language. A desired language is called controllable if there exists a security-aware supervisor that ensures that the restricted language executed by the plant for any possible attack behavior is the desired one – we refer to such supervisors as attack-resilient. First, we solve the problem of computing the maximal controllable sub-language (MCSL) of a desired language and propose the design algorithm for an attack-resilient supervisor, in scenarios where no security guarantees exists for communication between the plant and the supervisor. Then, we consider the case where the supervisor has active but intermittent access to a size-limited secure channel, which ensures integrity and availability of the data transmitted over it. Specifically, we propose the notion of accessibility as a measure of distance between a language and its sub-language, and show that a desired language is controllable with intermittently secure communication if and only if its difference from its MCSL without secure channel is bounded by the accessibility measure. Finally, we illustrate our approach on several examples.

This work focuses on control of discrete event systems (DES) in the presence of attacks on their inputs and outputs. We propose to model such attacks as nondeterministic finite state transducers (FSTs) and show how FSTs can be used to capture a very wide class of attacks including all previously considered attacks on DES, as well as additional attacks and attack features reported in recent security incidents. We study the supervisory control problem in cases when attacks occur: (i) only on the sensors, (ii) only on the actuators, and (iii) both on the actuators and sensors of the plant. For each case, we present new sets of controllability theorems and synthesizing algorithms for attack-resilient supervisors. On a series of examples, we illustrate the use of our approach for modeling and design of such security-aware supervisory control.

In this paper, we establish a zero-sum, hybrid state stochastic game model for designing defense policies for cyber-physical systems against different types of attacks. With the increasingly integrated properties of cyber-physical systems (CPS) today, security is a challenge for critical infrastructures. Though resilient control and detecting techniques for a specific model of attack have been proposed, to analyze and design detection and defense mechanisms against multiple types of attacks for CPSs requires new system frameworks. Besides security, other requirements such as optimal control cost also need to be considered. The hybrid game model we propose contains physical states that are described by the system dynamics, and a cyber state that represents the detection mode of the system composed by a set of subsystems. A strategy means selecting a subsystem by combining one controller, one estimator and one detector among a finite set of candidate components at each state. Based on the game model, we propose a suboptimal value iteration algorithm for a finite horizon game, and prove that the algorithm results an upper bound for the value of the finite horizon game. A moving-horizon approach is also developed in order to provide a scalable and real-time computation of the switching strategies. Both algorithms aim at obtaining a saddle-point equilibrium policy for balancing the system’s security overhead and control cost. The paper illustrates these concepts using numerical examples, and we compare the results with previously system designs that only equipped with one type of controller.

A digital microfluidic biochip (DMFB) is an attractive technology platform for automating laboratory procedures in biochemistry. In recent years, DMFBs based on a micro-electrode-dot-array (MEDA) architecture have been proposed. MEDA biochips can provide advantages of better capability of droplet manipulation and real-time sensing ability. However, errors are likely to occur due to defects, chip degradation, and the lack of precision inherent in biochemical experiments. Therefore, an efficient error-recovery strategy is essential to ensure the correctness of assays executed on MEDA biochips. By exploiting MEDA-specific advances in droplet sensing, we present a novel error-recovery technique to dynamically reconfigure the biochip using real-time data provided by on-chip sensors. Local recovery strategies based on probabilistic-timed-automata are presented for various types of errors. An online synthesis technique and a control flow are also proposed to connect local-recovery procedures with global error recovery for the complete bioassay. Moreover, an integer linear programming-based method is also proposed to select the optimal local-recovery time for each operation. Laboratory experiments using a fabricated MEDA chip are used to characterize the outcomes of key droplet operations. The PRISM model checker and three benchmarks are used for an extensive set of simulations. Our results highlight the effectiveness of the proposed error-recovery strategy.

In this work, we focus on securing cyber-physical systems (CPS) in the presence of network-based attacks, such as Man-in-the-Middle (MitM) attacks, where a stealthy attacker is able to compromise communication between system sensors and controllers. Standard methods for this type of attacks rely on the use of cryptographic mechanisms, such as Message Authentication Codes (MACs) to ensure data integrity. However, this approach incurs significant computation overhead, limiting its use in resource constrained systems. Consequently, we consider the problem of scheduling multiple control tasks on a shared processor while providing a suitable level of security guarantees. Specifically, by security guarantees we refer to control performance, i.e., Quality-of-Control (QoC), in the presence of attacks. We start by mapping requirements for QoC under attack into constraints for security-aware control tasks that, besides standard control operations, intermittently perform data authentication. This allows for the analysis of the impact that security-related computation overhead has on both schedulability of control tasks and QoC. Building on this analysis, we introduce a mixed-integer linear programming-based technique to obtain a schedulable task set with predefined QoC requirements. Also, to facilitate optimal resource allocation, we provide a method to analyze interplay between available computational resources and the overall QoC under attack, and show how to obtain a schedulable task set that maximizes the overall QoC guarantees. Finally, we prove usability of our approach on a case study with multiple automotive control components.

A digital microfluidic biochip (DMFB) is an attractive technology platform for various biomedical applications. However, a conventional DMFB is limited by: (i) the number of electrical connections that can be practically realized, (ii) constraints on droplet size and volume, and (iii) the need for special fabrication processes and the associated reliability/yield concerns. To overcome the above challenges, DMFBs based on a micro-electrode-dot-array (MEDA) architecture have been proposed and fabricated recently. Error recovery is of key interest for MEDA biochips due to the need for system reliability. Errors are likely to occur during droplet manipulation due to defects, chip degradation, and the uncertainty inherent in biochemical experiments. In this paper, we first formalize error-recovery objectives, and then synthesize optimal error-recovery protocols using a model based on Stochastic Multiplayer Games (SMGs). We also present a global error-recovery technique that can update the schedule of fluidic operations in an adaptive manner. Using three representative real-life bioassays, we show that the proposed approach can effectively reduce the bioassay completion time and increase the probability of success for error recovery.

This article is concerned with the security of modern Cyber-Physical Systems in the presence of transient sensor faults. We consider a system with multiple sensors measuring the same physical variable, where each sensor provides an interval with all possible values of the true state. We note that some sensors might output faulty readings and others may be controlled by a malicious attacker. Differing from previous works, in this article, we aim to distinguish between faults and attacks and develop an attack detection algorithm for the latter only. To do this, we note that there are two kinds of faults—transient and permanent; the former are benign and short-lived, whereas the latter may have dangerous consequences on system performance. We argue that sensors have an underlying transient fault model that quantifies the amount of time in which transient faults can occur. In addition, we provide a framework for developing such a model if it is not provided by manufacturers. Attacks can manifest as either transient or permanent faults depending on the attacker’s goal. We provide different techniques for handling each kind. For the former, we analyze the worst-case performance of sensor fusion over time given each sensor’s transient fault model and develop a filtered fusion interval that is guaranteed to contain the true value and is bounded in size. To deal with attacks that do not comply with sensors’ transient fault models, we propose a sound attack detection algorithm based on pairwise inconsistencies between sensor measurements. Finally, we provide a real-data case study on an unmanned ground vehicle to evaluate the various aspects of this article.

Recent years have witnessed a significant increase in the number of securityrelated incidents in control systems. These include high-profile attacks in a wide range of application domains, from attacks on critical infrastructure, as in the case of the Maroochy Water breach [1], and industrial systems (such as the StuxNet virus attack on an industrial supervisory control and data acquisition system [2], [3] and the German Steel Mill cyberattack [4], [5]), to attacks on modern vehicles [6]-[8]. Even high-assurance military systems were shown to be vulnerable to attacks, as illustrated in the highly publicized downing of the RQ-170 Sentinel U.S. drone [9]-[11]. These incidents have greatly raised awareness of the need for security in cyberphysical systems (CPSs), which feature tight coupling of computation and communication substrates with sensing and actuation components. However, the complexity and heterogeneity of this next generation of safety-critical, networked, and embedded control systems have challenged the existing design methods in which security is usually consider as an afterthought.

Several recent incidents have clearly illustrated the susceptibility of cyberphysical systems (CPS) to attacks, raising attention to security challenges in these systems. The tight interaction between information technology and the physical world has introduced new vulnerabilities that cannot be addressed with the use of standard cryptographic security techniques. Accordingly, the problem of state estimation in the presence of sensor and actuator attacks has attracted significant attention in the past. Unlike the existing work, in this paper, we consider the problem of attack-resilient state estimation in the presence of bounded-size noise. We focus on the most general model for sensor attacks where any signal can be injected via compromised sensors. Specifically, we present an $l_0$ -based state estimator that can be formulated as a mixed-integer linear program and its convex relaxation based on the $l_1$ norm. For both attack-resilient state estimators, we derive rigorous analytic bounds on the state-estimation errors caused by the presence of noise. Our analysis shows that the worst-case error is linear with the size of the noise and, thus, the attacker cannot exploit the noise to introduce unbounded state-estimation errors. Finally, we show how the $l_0$ and $l_1$ -based attack-resilient state estimators can be used for sound attack detection and identification; we provide conditions on the size of attack vectors that ensure correct identification of compromised sensors.

Concept of Industry 4.0 and implementation of Cyber Physical Systems (CPS) and Internet of Things (IoT) in industrial plants are changing the way we manufacture. Introduction of industrial IoT leads to ubiquitous communication (usually wireless) between devices in industrial control systems, thus introducing numerous security concerns and opening up wide space for potential malicious threats and attacks. As a consequence of various cyber-attacks, fatal failures can occur on system parts or the system as a whole. Therefore, security mechanisms must be developed to provide sufficient resilience to cyber-attacks and keep the system safe and protected. In this paper we present a method for detection of attacks on signals in continuous time controlled electro-pneumatic positioning system that is implemented using smart devices with wireless communication capabilities. The method is based on $\varepsilon$ insensitive support vector regression ($\varepsilon$-SVR); it is implemented on real-world system, and it successfully detected all considered attacks (without false positives) in real-time.

Due to misaligned clock sources, distributed control in Cyber-Physical Systems (CPS) requires not only synchronous execution of control algorithms on distributed system components, which we refer to as cyber-synchronization, but also appropriate generation of actuation signals—we refer to this as physical-synchronization. In this paper, we define general requirements for cyber-physical synchronization, as well as show their use on a specific real-world application—distributed motion control for reconfigurable manufacturing systems. We present synchronization challenges in such systems and investigate effects of synchronization errors on the overall system functionality (i.e., machining accuracy). Furthermore, we introduce a low-cost synchronization scheme that can be implemented with of-the-shelf components and validate it on standardized accuracy tests with 2D configurations of industry-grade single-axis robots. We show that our cyber-physical synchronization techniques ensure minimal accuracy impairment of distributed motion control without introducing significant cost/overhead to system design.

In this work, we synthesize collaboration protocols for human-unmanned aerial vehicle (H-UAV) command and control systems, where the human operator aids in securing the UAV by intermittently performing geolocation tasks to confirm its reported location. We first present a stochastic game-based model for the system that accounts for both the operator and an adversary capable of launching stealthy false-data injection attacks, causing the UAV to deviate from its path. We also describe a synthesis challenge due to the UAV’s hidden-information constraint. Next, we perform human experiments using a developed RESCHU-SA testbed to recognize the geolocation strategies that operators adopt. Furthermore, we deploy machine learning techniques on the collected experimental data to predict the correctness of a geolocation task at a given location based on its geographical features. By representing the model as a delayed-action game and formalizing the system objectives, we utilize off-the-shelf model checkers to synthesize protocols for the human-UAV coalition that satisfy these objectives. Finally, we demonstrate the usefulness of the H-UAV protocol synthesis through a case study where the protocols are experimentally analyzed and further evaluated by human operators.

Reconfigurable manufacturing systems supported by Industrial Internet-of-Things (IIoT) are modular and easily integrable, promoting efficient system/component reconfigurations with minimal downtime. Industrial systems are commonly based on sequential controllers described with Control Interpreted Petri Nets (CIPNs). Existing design methodologies to distribute centralized automation/control tasks focus on maintaining functional properties of the system during the process, while disregarding failures that may occur during execution (e.g., communication packet drops, sensing or actuation failures). Consequently, in this work, we provide a missing link for reliable IIoT-based distributed automation. We introduce a method to transform distributed control models based on CIPNs into Stochastic Reward Nets that enable integration of realistic fault models (e.g., probabilistic link models). We show how to specify desired system properties to enable verification under the adopted communication/fault models, both at design- and run-time; we also show feasibility of runtime verification on the edge, with a continuously updated system model. Our approach is used on real industrial systems, resulting in modifications of local controllers to guarantee reliable system operation in realistic IIoT environments.

Stochastic multiplayer games (SMGs) have gained attention in the field of strategy synthesis for multi-agent reactive systems. However, standard SMGs are limited to modeling systems where all agents have full knowledge of the state of the game. In this paper, we introduce delayed-action games (DAGs) formalism that simulates hidden-information games (HIGs) as SMGs, where hidden information is captured by delaying a player’s actions. The elimination of private variables enables the usage of SMG off-the-shelf model checkers to implement HIGs. Furthermore, we demonstrate how a DAG can be decomposed into subgames that can be independently explored, utilizing parallel computation to reduce the model checking time, while alleviating the state space explosion problem that SMGs are notorious for. In addition, we propose a DAG-based framework for strategy synthesis and analysis. Finally, we demonstrate applicability of the DAG-based synthesis framework on a case study of a human-on-the-loop unmanned-aerial vehicle system under stealthy attacks, where the proposed framework is used to formally model, analyze and synthesize security-aware strategies for the system.

This paper considers the problem of continuous state estimation from discrete context-based measurements. Context measurements provide binary information as obtained from the system's environment, e.g., a medical alarm indicating that a vital sign is above a certain threshold. Since they provide state information, these measurements can be used for estimation purposes, similar to standard continuous measurements, especially when standard sensors are biased or attacked. Context measurements are assumed to have a known probability of occurring given the state; in particular, we focus on the probit function to model threshold-based measurements, such as the medical-alarm scenario. We develop a recursive context-aware filter by approximating the posterior distribution with a Gaussian distribution with the same first two moments as the true posterior. We show that the filter's expected uncertainty is bounded when the probability of receiving context measurements is lower bounded by some positive number for all system states. Furthermore, we provide an observability-like result—all eigenvalues of the filter's covariance matrix converge to 0 after repeated updates if and only if a persistence of excitation condition holds for the context measurements. Finally, in addition to simulation evaluations, we applied the filter to the problem of estimating a patient's blood oxygen content during surgery using real-patient data.

Hyperproperties have shown to be a powerful tool for expressing and reasoning about information-flow security policies. In this paper, we investigate the problem of statistical model checking (SMC) for hyperproperties. Unlike exhaustive model checking, SMC works based on drawing samples from the system at hand and evaluate the specification with statistical confidence. The main benefit of applying SMC over exhaustive techniques is its efficiency and scalability. To reason about probabilistic hyperproperties, we first propose the temporal logic HyperPCLT* that extends PCTL* and HyperPCTL. We show that HyperPCLT* can express important probabilistic information-flow security policies that cannot be expressed with HyperPCTL. Then, we introduce SMC algorithms for verifying HyperPCLT* formulas on discrete-time Markov chains, based on sequential probability ratio tests (SPRT) with a new notion of multi-dimensional indifference region. Our SMC algorithms can handle both non-nested and nested probability operators for any desired significance level. To show the effectiveness of our technique, we evaluate our SMC algorithms on four case studies focused on information security: timing side-channel vulnerability in encryption, probabilistic anonymity in dining cryptographers, probabilistic noninterference of parallel programs, and the performance of a randomized cache replacement policy that acts as a countermeasure against cache flush attacks.

There is a growing interest on formal methods-based robotic planning for temporal logic objectives. In this work, we extend the scope of existing synthesis methods to hyper-temporal logics. We are motivated by the fact that important planning objectives, such as optimality, robustness, and privacy, (maybe implicitly) involve the interrelation between multiple paths. Such objectives are thus hyperproperties, and cannot be expressed with usual temporal logics like the linear temporal logic (LTL). We show that such hyperproperties can be expressed by HyperLTL, an extension of LTL to multiple paths. To handle the complexity of planning with HyperLTL specifications, we introduce a symbolic approach for synthesizing planning strategies on discrete transition systems. Our planning method is evaluated on several case studies.

We present a reinforcement learning (RL) framework to synthesize a control policy from a given linear temporal logic (LTL) specification in an unknown stochastic environment that can be modeled as a Markov Decision Process (MDP). Specifically, we learn a policy that maximizes the probability of satisfying the LTL formula without learning the transition probabilities. We introduce a novel rewarding and path-dependent discounting mechanism based on the LTL formula such that (i) an optimal policy maximizing the total discounted reward effectively maximizes the probabilities of satisfying LTL objectives, and (ii) a model-free RL algorithm using these rewards and discount factors is guaranteed to converge to such policy. Finally, we illustrate the applicability of our RL-based synthesis approach on two motion planning case studies.

With network-based attacks, such as Man-in-the-Middle (MitM) attacks, the attacker can inject false data to force a closed-loop system into any undesired state, unless even intermittently integrity of delivered sensor measurements is enforced. Yet, the use of standard cryptographic techniques that ensure data integrity, such as Message Authentication Codes (MACs), introduces significant communication and computation overhead. Thus, in this work we explore the use of cumulative MACs that significantly reduce network overhead. We consider systems with Kalman filter-based state estimators and sequential probability ratio test (SPRT) intrusion detectors. We show that strong estimation guarantees under MitM attacks can be obtained even with intermittent use of a single cumulative MAC that is added to appropriate sensor measurements transmitted over the network. We present a design-time methodology to evaluate the effects of any given cumulative integrity enforcement policy on reachable state-estimation errors for any type of stealthy attacks; this provides a base for design of cumulative enforcement policies with desired performance guarantees even in the presence of MitM attacks. Finally, we illustrate the effectiveness of our approach on an automated steering control.