Reward design is a key component of deep reinforcement learning (DRL), yet some tasks and designer’s objectives may be unnatural to define as a scalar cost function. Among the various techniques, formal methods integrated with DRL have garnered considerable attention due to their expressiveness and flexibility in defining the reward and requirements for different states and actions of the agent. Nevertheless, the exploration of leveraging Signal Temporal Logic (STL) for guiding multi-agent reinforcement learning (MARL) reward design is still limited. The presence of complex interactions, heterogeneous goals, and critical safety requirements in multi-agent systems exacerbates this challenge. In this paper, we propose a novel STL-guided multi-agent reinforcement learning framework. The STL requirements are designed to include both task specifications according to the objective of each agent and safety specifications. The robustness values from checking the states against STL specifications are leveraged to generate rewards. We validate our approach by conducting experiments across various testbeds. The experimental results demonstrate significant performance improvements compared to MARL without STL guidance, along with a remarkable increase in the overall safety rate of the multi-agent systems.

Ensuring safety in dynamic multi-agent systems is challenging due to limited information about the other agents. Control Barrier Functions (CBFs) are showing promise for safety assurance but current methods make strong assumptions about other agents and often rely on manual tuning to balance safety, feasibility, and performance. In this work, we delve into the problem of adaptive safe learning for multi-agent systems with CBF. We show how emergent behaviour can be profoundly influenced by the CBF configuration, highlighting the necessity for a responsive and dynamic approach to CBF design. We present ASRL, a novel adaptive safe RL framework, to fully automate the optimization of policy and CBF coefficients, to enhance safety and long-term performance through reinforcement learning. By directly interacting with the other agents, ASRL learns to cope with diverse agent behaviours and maintains the cost violations below a desired limit. We evaluate ASRL in a multi-robot system and competitive multi-agent racing, against learning-based and control-theoretic approaches. We empirically demonstrate the efficacy of ASRL, and assess generalization and scalability to out-of-distribution scenarios.

When academic researchers develop and validate autonomous driving algorithms, there is a challenge in balancing high-performance capabilities with the cost and complexity of the vehicle platform. Much of today’s research on autonomous vehicles (AV) is limited to experimentation on expensive commercial vehicles that require large skilled teams to retrofit the vehicles and test them in dedicated facilities. On the other hand, 1/10th-1/16th scaled-down vehicle platforms are more affordable but have limited similitude in performance and drivability. To address this issue, we present the design of a one-third-scale autonomous electric go-kart platform with open-source mechatronics design along with fully functional autonomous driving software. The platform’s multi-modal driving system is capable of manual, autonomous, and teleoperation driving modes. It also features a flexible sensing suite for the algorithm deployment across perception, localization, planning, and control. This development serves as a bridge between full-scale vehicles and reduced-scale cars while accelerating cost-effective algorithmic advancements. Our experimental results demonstrate the AV4EV platform’s capabilities and ease of use for developing new AV algorithms. All materials are available at AV4EV.org to stimulate collaborative efforts within the AV and electric vehicle (EV) communities.

Robot localization is an inverse problem of finding a robot's pose using a map and sensor measurements. In recent years, Invertible Neural Networks (INN s) have successfully solved ambiguous inverse problems in various fields. This paper proposes a framework that approaches the localization problem with INN. We design a network that provides implicit map representation in the forward path and localization in the inverse path. By sampling the latent space in evaluation, Local_INN outputs robot poses with covariance, which can be used to estimate the uncertainty. We show that the localization performance of Local_INN is on par with current methods with much lower latency. We show detailed 2D and 3D map reconstruction from Local_INN using poses exterior to the training set. We also provide a global localization algorithm using Local_INN to tackle the kidnapping problem.

Autonomous vehicles are increasingly introduced into our lives. Yet, people’s misunderstanding and mistrust have become the major obstacles to the use of these technologies. In response to this problem, proper work must be done to increase public’s understanding and awareness and help drivers rationally evaluate the system. The method proposed in this paper is a virtual reality driving simulator which serves as a low-cost platform for autonomous vehicle demonstration and education. To test the validity of the platform, we recruited 36 participants and conducted a test training drive using three different scenarios. The results show that our simulator successfully increased participants’ understanding while favorably changing their attitude towards the autonomous system. The methodology and findings presented in this paper can be further explored by driving schools, auto manufacturers, and policy makers, to improve training for autonomous vehicles.

Autonomous racing with scaled race cars has gained increasing attention as an effective approach for developing perception, planning and control algorithms for safe autonomous driving at the limits of the vehicle’s handling. To train agile control policies for autonomous racing, learning-based approaches largely utilize reinforcement learning, albeit with mixed results. In this study, we benchmark a variety of imitation learning policies for racing vehicles that are applied directly or for bootstrapping reinforcement learning both in simulation and on scaled real-world environments. We show that interactive imitation learning techniques outperform traditional imitation learning methods and can greatly improve the performance of reinforcement learning policies by bootstrapping thanks to its better sample efficiency. Our benchmarks provide a foundation for future research on autonomous racing using Imitation Learning and Reinforcement Learning.

Predicting the motion of dynamic agents is a critical task for guaranteeing the safety of autonomous systems. A particular challenge is that motion prediction algorithms should obey dynamics constraints and quantify prediction uncertainty as a measure of confidence. We present a physics-constrained approach for motion prediction which uses a surrogate dynamical model to ensure that predicted trajectories are dynamically feasible. We propose a two-step integration consisting of intent and trajectory prediction subject to dynamics constraints. We also construct prediction regions that quantify uncertainty and are tailored for autonomous driving by using conformal prediction, a popular statistical tool. Physics Constrained Motion Prediction achieves a 41% better ADE, 56% better FDE, and 19% better IoU over a baseline in experiments using an autonomous racing dataset.

Safety-critical Autonomous Systems require trustworthy and transparent decision-making process to be deployable in the real world. The advancement of Machine Learning introduces high performance but largely through black-box algorithms. In this position paper, we focus the discussion of explainability specifically with Autonomous Vehicles (AVs). As a safety-critical system, AVs provide the unique opportunity to utilize cutting-edge Machine Learning techniques while requiring transparency in decision making. Interpretability in every action the AV takes becomes crucial in post-hoc analysis where blame assignment might be necessary. In this paper, we provide positioning on how researchers could consider incorporating explainability and interpretability into design and optimization of separate Autonomous Vehicle modules including Perception, Planning, and Control.

High-performance autonomy often must operate at the boundaries of safety. When external agents are present in a system, the process of ensuring safety without sacrificing performance becomes extremely difficult. In this paper we present an approach to stress test such systems based on the rapidly exploring random tree (RRT) algorithm.We propose to find faults in such systems through adversarial agent perturbations, where the behaviors of other agents in an otherwise fixed scenario are modified. This creates a large search space of possibilities, which we explore both randomly and with a focused strategy that runs RRT in a bounded projection of the observable states that we call the objective space. The approach is applied to generate tests for evaluating overtaking logic and path planning algorithms in autonomous racing, where the vehicles are driving at high speed in an adversarial environment. We evaluate several autonomous racing path planners, finding numerous collisions during overtake maneuvers in all planners. The focused RRT search finds several times more crashes than the random strategy, and, for certain planners, tens to hundreds of times more crashes in the second half of the track.

The 3rd Japan Automotive AI Challenge was an international online autonomous racing challenge where 164 teams competed in December 2021. This paper outlines the winning strategy to this competition, and the advantages and challenges of using the Autoware.Auto open source autonomous driving platform for multi-agent racing. Our winning approach includes a lane-switching opponent overtaking strategy, a global raceline optimization, and the integration of various tools from Autoware.Auto including a Model-Predictive Controller. We describe the use of perception, planning and control modules for high-speed racing applications and provide experience-based insights on working with Autoware.Auto. While our approach is a rule-based strategy that is suitable for non-interactive opponents, it provides a good reference and benchmark for learning-enabled approaches.

Urban Air Mobility, the scenario where hundreds of manned and Unmanned Aircraft Systems (UASs) carry out a wide variety of missions (e.g., moving humans and goods within the city), is gaining acceptance as a transportation solution of the future. One of the key requirements for this to happen is safely managing the air traffic in these urban airspaces. Due to the expected density of the airspace, this requires fast autonomous solutions that can be deployed online. We propose Learning-‘N-Flying (LNF), a multi-UAS Collision Avoidance (CA) framework. It is decentralized, works on the fly, and allows autonomous Unmanned Aircraft System (UAS)s managed by different operators to safely carry out complex missions, represented using Signal Temporal Logic, in a shared airspace. We initially formulate the problem of predictive collision avoidance for two UASs as a mixed-integer linear program, and show that it is intractable to solve online. Instead, we first develop Learning-to-Fly (L2F) by combining (1) learning-based decision-making and (2) decentralized convex optimization-based control. LNF extends L2F to cases where there are more than two UASs on a collision path. Through extensive simulations, we show that our method can run online (computation time in the order of milliseconds) and under certain assumptions has failure rates of less than 1% in the worst case, improving to near 0% in more relaxed operations. We show the applicability of our scheme to a wide variety of settings through multiple case studies.

Balancing performance and safety is crucial to deploying autonomous vehicles in multi-agent environments. In particular, autonomous racing is a domain that penalizes safe but conservative policies, highlighting the need for robust, adaptive strategies. Current approaches either make simplifying assumptions about other agents or lack robust mechanisms for online adaptation. This work makes algorithmic contributions to both challenges. First, to generate a realistic, diverse set of opponents, we develop a novel method for self-play based on replica-exchange Markov chain Monte Carlo. Second, we propose a distributionally robust bandit optimization procedure that adaptively adjusts risk aversion relative to uncertainty in beliefs about opponents’ behaviors. We rigorously quantify the tradeoffs in performance and robustness when approximating these computations in real-time motion-planning, and we demonstrate our methods experimentally on autonomous vehicles that achieve scaled speeds comparable to Formula One racecars.

TUNERCAR is a toolchain that jointly optimizes racing strategy, planning methods, control algorithms, and vehicle parameters for an autonomous racecar. In this paper, we detail the target hardware, software, simulators, and systems infrastructure for this toolchain. Our methodology employs a parallel implementation of CMA-ES which enables simulations to proceed 6 times faster than real-world rollouts. We show our approach can reduce the lap times in autonomous racing, given a fixed computational budget. For all tested tracks, our method provides the lowest lap time, and relative improvements in lap time between 7-21%. We demonstrate improvements over a naive random search method with equivalent computational budget of over 15 seconds/lap, and improvements over expert solutions of over 2 seconds/lap. We further compare the performance of our method against hand-tuned solutions submitted by over 30 international teams, comprised of graduate students working in the field of autonomous vehicles. Finally, we discuss the effectiveness of utilizing an online planning mechanism to reduce the reality gap between our simulation and actual tests.

The determination of safety assurances for automated driving vehicles is one of the most critical challenges in the industry today. Several behavioral safety models for automated driving have been proposed recently and standards discussions are on the way. In this paper we present a method to automatically explore the performance of automated vehicle (AV) safety models utilizing robustness of Metric Temporal Logic (MTL) specifications as a continuous metric of safety. We present a case study of the Responsibility Sensitive Safety model (RSS), introducing a safety evaluation pipeline based on the CARLA driving simulator, RSS and a set of safety-critical driving scenarios. Our method automatically extracts safety relevant profiles for these scenarios providing practical parametric boundaries for implementation. Furthermore, we evaluate the trade-offs between safety and utility within the safe RSS parameter space through a proposed naturalistic benchmark challenge that we open-sourced. We analyze different RSS parameter configurations including assertive and more conservative settings, extracted by our specification-driven framework. Our results show that while maintaining the safety boundaries, the extracted RSS configuration for assertive driving behavior achieves the highest utility.

In multi-agent systems, robots transmit their planned trajectories to each other or to a central controller, and each receiver plans its own actions by maximizing a measure of mission satisfaction. For missions expressed in temporal logic, the robustness function plays the role of satisfaction measure. Currently, a Piece-Wise Linear (PWL) or piece-wise constant reconstruction is used at the receiver. This allows an efficient robustness computation algorithm - a.k.a. monitoring - but is not adaptive to the signal class of interest, and does not leverage the compression properties of more general representations. When communication capacity is at a premium, this is a serious bottleneck. In this paper we first show that the robustness computation is significantly affected by how the continuous-time signal is reconstructed from the received samples, which can mean the difference between a successful control and a crash. We show that monitoring general spline-based reconstructions yields a smaller robustness error, and that it can be done with the same time complexity as monitoring the simpler PWL reconstructions. Thus robustness computation can now be adapted to the signal class of interest. We further show that the monitoring error is tightly upper-bounded by the L∞ signal reconstruction error. We present a (non-linear) L∞-based scheme which yields even lower monitoring error than the spline-based schemes (which have the advantage of being faster to compute), and illustrate all results on two case studies. As an application of these results, we show how time-frequency specifications can be efficiently monitored online.

As methods and tools for cyber-physical systems (CPS) grow in capabilities and use, one-size-fits-all solutions start to show their limitations. In particular, tools and languages for programming an algorithm or modeling a CPS that are specific to the application domain are typically more usable, and yield better performance, than general-purpose languages and tools. In the domain of cardiac arrhythmia monitoring, a small, implantable medical device continuously monitors the patient's cardiac rhythm and delivers electrical therapy when needed. The algorithms executed by these devices are streaming algorithms, so they are best programmed in a streaming language that allows the programmer to reason about the incoming data stream as the basic object, rather than force her to think about lower-level details like state maintenance and minimization. Because these devices are resource-constrained, it is useful if the programming language allowed predictable performance in terms of processing runtime and energy consumption, or more general costs. StreamQRE is a declarative streaming programming language, with an efficient and portable implementation and strong theoretical guarantees. In particular, its evaluation algorithm guarantees constant cost (runtime, memory, energy) per data item and also calculates upper bounds on the per-item cost. Such an estimate of the cost allows early exploration of the algorithmic possibilities, while maintaining a handle on worst case performance, on the basis of which hardware can be designed and algorithms can be tuned.

Model Predictive Control (MPC) plays an important role in optimizing operations of complex cyber-physical systems because of its ability to forecast system’s behavior and act under system level constraints. However, MPC requires reasonably accurate underlying models of the system. In many applications, such as building control for energy management, Demand Response, or peak power reduction, obtaining a high-fidelity physics-based model is cost and time prohibitive, thus limiting the widespread adoption of MPC. To this end, we propose a data-driven control algorithm for MPC that relies only on the historical data. We use multi-output regression trees to represent the system’s dynamics over multiple future time steps and formulate a finite receding horizon control problem that can be solved in real-time in closed-loop with the physical plant. We apply this algorithm to peak power reduction in buildings to optimally trade-off peak power reduction against thermal comfort without having to learn white/grey box models of the systems dynamics.

Relaxed notions of decidability widen the scope of automatic verification of hybrid systems. In quasi-decidability and delta-decidability, the fundamental compromise is that if we are willing to accept a slight error in the algorithm's answer, or a slight restriction on the class of problems we verify, then it is possible to obtain practically useful answers. This paper explores the connections between relaxed decidability and the robust semantics of Metric Temporal Logic formulas. It establishes a formal equivalence between the robustness degree of MTL specifications, and the imprecision parameter delta used in delta-decidability when it is used to verify MTL properties. We present an application of this result in the form of an algorithm that generates new constraints to the delta-decision procedure from falsification runs, which can speed up the verification run. We then establish new conditions under which robust testing, based on the robust semantics of MTL, is in fact a quasi-semidecision procedure. These results allow us to delimit what is possible with fast, robustness-based methods, accelerate (near-)exhaustive verification, and further bridge the gap between verification and simulation.

In this paper, we survey recent progress in CyberCardia project, a CPS Frontier project funded by the National Science Foundation. The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The acceleration in medical-device innovation achievable as a result of the CyberCardia research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly.

Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It usually ends in death within a minute. A common way to treat the symptoms of fibrillation is to implant a medical device, known as an Implantable Cardioverter Defibrillator (ICD), in the patient's body. Model-based verification can supply rigorous proofs of safety and efficacy. In this paper, we build a hybrid system model of the human heart+ICD closed loop, and show it to be a STORMED system, a class of o-minimal hybrid systems that admit finite bisimulations. In general, it may not be possible to compute the bisimulation. We show that approximate reachability can yield a finite simulation for STORMED systems, and that certain compositions respect the STORMED property. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.

Peak power consumption is a universal problem across energy control systems in electrical grids, buildings, and industrial automation where the uncoordinated operation of multiple controllers result in temporally correlated electricity demand surges (or peaks). While there exist several diferent approaches to balance power consumption by load shifting and load shedding, they operate on coarse grained time scales and do not help in de-correlating energy sinks. The Energy System Scheduling Problem is particularly hard due to its binary control variables. Its complexity grows exponentially with the scale of the system, making it impossible to handle systems with more than a few variables. We developed a scalable approach for fine-grained scheduling of energy control systems that novelly combines techniques from control theory and computer science. The original system with binary control variables are approximated by an averaged system whose inputs are the utilization values of the binary inputs within a given period. The error between the two systems can be bounded, which allows us to derive a safety constraint for the averaged system so that the original system's safety is guaranteed. To further reduce the complexity of the scheduling problem, we abstract the averaged system by a simple single-state single-input dynamical system whose control input is the upper-bound of the total demand of the system. This model abstraction is achieved by extending the concept of simulation relations between transition systems to allow for input constraints between the systems. We developed conditions to test for simulation relations as well as algorithms to compute such a model abstraction. As a consequence, we only need to solve a small linear program to compute an optimal bound of the total demand. The total demand is then broken down, by solving a linear program much smaller than the original program, to individual utilization values of the subsystems, whose actual schedule is then obtained by a low-level scheduling algorithm. Numerical simulations in Matlab show the e ectiveness and scalability of our approach.

Autonomous vehicles promise significant benefits to society, from reduced accident rates to greater mobility for the elderly. The biggest challenge in the design of autonomous vehicles comes from the uncertainty of the environment in which they will operate. Their control algorithms must be able to cope with driving events that occur on widely ranging time scales. For example, relaxed rural driving can accommodate planning actions every few seconds, while imminent collision avoidance requires planning and actuation on the order of a few milliseconds. Thus 'real-time' performance will imply different things depending on the context.

Control software of autonomous robots has stringent real-time requirements that must be met to achieve the control objectives. One source of variability in the performance of a control system is the execution time and accuracy of the state estimator that provides the controller with state information. This estimator is typically perception-based (e.g., Computer Vision-based) and is computationally expensive. When the computational resources of the hardware platform become overloaded, the estimation delay can compromise control performance and even stability. In this paper, we define a framework for co-designing anytime estimation and control algorithms, in a manner that accounts for implementation issues like delays and inaccuracies. We construct an anytime perception-based estimator from standard off-the-shelf Computer Vision algorithms, and show how to obtain a trade-off curve for its delay vs estimate error behaviour. We use this anytime estimator in a controller that can use this trade-off curve at runtime to achieve its control objectives at a reduced energy cost. When the estimation delay is too large for correct operation, we provide an optimal manner in which the controller can use this curve to reduce estimation delay at the cost of higher inaccuracy, all the while guaranteeing basic objectives are met. We illustrate our approach on an autonomous hexrotor and demonstrate its advantage over a system that does not exploit co-design.

No abstract available.

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in the model-driven design of a pacemaker whose model is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems.

In modern hospitals, patients are treated using a wide array of medical devices that are increasingly interacting with each other over the network, thus offering a perfect example of a cyber-physical system. We study the safety of a medical device system for the physiologic closed-loop control of drug infusion. The main contribution of the paper is the verification approach for the safety properties of closed-loop medical device systems. We demonstrate, using a case study, that the approach can be applied to a system of clinical importance. Our method combines simulation-based analysis of a detailed model of the system that contains continuous patient dynamics with model checking of a more abstract timed automata model. We show that the relationship between the two models preserves the crucial aspect of the timing behavior that ensures the conservativeness of the safety analysis. We also describe system design that can provide open-loop safety under network failure.

A building testbed for design and evaluation of energy efficient control and demand response strategies for real buildings is presented. The testbed is a scaled down model of a centralized Heating, Ventilation and Air Conditioning (HVAC) and lighting system. Sensing and control in the tesbed is achieved using the standard Building Automation and Control Network protocol. A MATLAB based front-end can be used to run and observe experiments.

We study the problem of stabilizing a linear system over a wireless network using a simple in-network computation method. Specifically, we study an architecture called the "Wireless Control Network" (WCN), where each wireless node maintains a state, and periodically updates it as a linear combination of neighboring plant outputs and node states. This architecture has previously been shown to have low computational overhead and beneficial scheduling and compositionality properties. In this paper we characterize fundamental topological conditions to allow stabilization using such a scheme. To achieve this, we exploit the fact that the WCN scheme causes the network to act as a linear dynamical system, and analyze the coupling between the plant's dynamics and the dynamics of the network. We show that stabilizing control inputs can be computed in-network if the vertex connectivity of the network is larger than the geometric multiplicity of any unstable eigenvalue of the plant. This condition is analogous to the typical min-cut condition required in classical information dissemination problems. Furthermore, we specify equivalent topological conditions for stabilization over a wired (or point-to-point) network that employs network coding in a traditional way - as a communication mechanism between the plant's sensors and decentralized controllers at the actuators.

We present a distributed scheme used for control over a network of wireless nodes. As opposed to traditional networked control schemes where the nodes simply route information to and from a dedicated controller (perhaps performing some encoding along the way), our approach, Wireless Control Network (WCN), treats the network itself as the controller. In other words, the computation of the control law is done in a fully distributed way inside the network. We extend the basic WCN strategy, where at each time-step, each node updates its internal state to be a linear combination of the states of the nodes in its neighborhood. This causes the entire network to behave as a linear dynamical system, with sparsity constraints imposed by the network topology. We demonstrate that with observer style updates, the WCN's robustness to link failures is substantially improved. Furthermore, we show how to design a WCN that can maintain stability even in cases of node failures. We also address the problem of WCN synthesis with guaranteed optimal performance of the plant, with respect to standard cost functions. We extend the synthesis procedure to deal with continuous-time plants and demonstrate how the WCN can be used on a practical, industrial application, using a process-in-the-loop setup with real hardware.

Model-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling of the real-time system, followed by the model's verification at an early stage. The verified model must then be translated to a more detailed model for simulation-based testing and finally translated into executable code in a physical implementation. As later stages build on the same core model, it is essential that models used earlier in the pipeline are valid approximations of the more detailed models developed downstream. The focus of this effort is on the design and development of a model translation tool, UPP2SF, and how it integrates system modeling, verification, model-based WCET analysis, simulation, code generation and testing into an MDD based framework. UPP2SF facilitates automatic conversion of verified timed automata-based models (in UPPAAL) to models that may be simulated and tested (in Simulink/State flow). We describe the design rules to ensure the conversion is correct, efficient and applicable to a large class of models. We show how the tool enables MDD of an implantable cardiac pacemaker. We demonstrate that UPP2SF preserves behaviors of the pacemaker model from UPPAAL to State flow. The resultant State flow chart is automatically converted into C and tested on a hardware platform for a set of requirements.

In large building systems, such as a university campus, the air-conditioning systems are commonly served by chiller plants, which contribute a large fraction of the total electricity consumption of the campuses. The power consumption of a chiller is highly affected by its Coefficient of Performance (COP), which is optimal when the chiller is operated at or near full load. For a chiller plant, its overall COP can be optimized by utilizing a Thermal Energy Storage (TES) and switching its operation between COP-optimal charging and discharging modes. However, uncoordinated mode switchings of chiller plants may cause temporally-correlated high electricity demand when multiple plants are charging their TES concurrently. In this paper, a GS approach, proposed in our previous work, is used to schedule the chiller plants to reduce their peak aggregate power demand while ensuring safe operation of the TES. We present a scheduling algorithm based on backward reach set computation of the TES dynamics. The proposed algorithm is demonstrated in a numerical simulation in Mat lab to be effective for reducing the peak power demand and the overall electricity cost.

The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600 000 devices. Of these, 200 000 or 41% were due to firmware issues and their effect continues to increase in frequency. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. To this effect, a real-time virtual heart model (VHM) has been developed to model the electrophysiological operation of the functioning and malfunctioning (i.e., during arrhythmia) heart. By extracting the timing properties of the heart and pacemaker device, we present a methodology to construct a timed-automata model for functional and formal testing and verification of the closed-loop system. The VHM's capability of generating clinically relevant response has been validated for a variety of common arrhythmias. Based on a set of requirements, we describe a closed-loop testing environment that allows for interactive and physiologically relevant model-based test generation for basic pacemaker device operations such as maintaining the heart rate, atrial-ventricle synchrony, and complex conditions such as pacemaker-mediated tachycardia. This system is a step toward a testing and verification approach for medical cyber-physical systems with the patient in the loop.

Networked cyber-physical systems are fundamentally constrained by the tight coupling and closed-loop control of physical processes. To address actuation in such closed-loop wireless control systems there is a strong need to rethink the communication architectures and protocols for reliability, coordination, and control. We introduce the Embedded Virtual Machine (EVM), a programming abstraction where controller tasks with their control and timing properties are maintained across physical node boundaries and functionality is capable of migrating to the most competent set of physical controllers. In the context of process and discrete control, an EVM is the distributed runtime system that dynamically selects primary-backup sets of controllers given spatial and temporal constraints of the underlying wireless network. EVM-based algorithms allow network control algorithms to operate seamlessly over less reliable wireless networks with topological changes. They introduce new capabilities such as predictable outcomes during sensor/actuator failure, adaptation to mode changes, and runtime optimization of resource consumption. An automated design flow from Simulink to platform-independent domain-specific languages, and subsequently, to platform-dependent code generation is presented. Through case studies in discrete and process control we demonstrate the capabilities of EVM-based wireless network control systems.

Peak power consumption of buildings in large facilities like hospitals and universities becomes a big issue because peak prices are much higher than normal rates. During a power demand surge an automated power controller of a building may need to schedule ON and OFF different environment actuators such as heaters and air quality control while maintaining the state variables such as temperature or air quality of any room within comfortable ranges. The green scheduling problem asks whether a scheduling policy is possible for a system and what is the necessary and sufficient condition for systems to be feasible. In this paper we study the feasibility of the green scheduling problem for HVAC(Heating, Ventilating, and Air Conditioning) systems which are approximated by a discrete-time model with constant increasing and decreasing rates of the state variables. We first investigate the systems consisting of two tasks and find the analytical form of the necessary and sufficient conditions for such systems to be feasible under certain assumptions. Then we present our algorithmic solution for general systems of more than 2 tasks. Given the increasing and decreasing rates of the tasks, our algorithm returns a subset of the state space such that the system is feasible if and only if the initial state is in this subset. With the knowledge of that subset, a scheduling policy can be computed on the fly as the system runs, with the flexibility to add power-saving, priority-based or fair sub-policies.

Most algorithms are run-to-completion and provide one answer upon completion and no answer if interrupted before completion. On the other hand, anytime algorithms have a monotonic increasing utility with the length of execution time. Our investigation focuses on the development of time-bounded anytime algorithms on Graphics Processing Units (GPUs) to trade-off the quality of output with execution time. Given a time-varying workload, the algorithm continually measures its progress and the remaining contract time to decide its execution pathway and select system resources required to maximize the quality of the result. To exploit the quality-time tradeoff, the focus is on the construction, instrumentation, on-line measurement and decision making of algorithms capable of efficiently managing GPU resources. We demonstrate this with a Parallel A* routing algorithm on a CUDA-enabled GPU. The algorithm execution time and resource usage is described in terms of CUDA kernels constructed at design-time. At runtime, the algorithm selects a subset of kernels and composes them to maximize the quality for the remaining contract time. We demonstrate the feedback-control between the GPU-CPU to achieve controllable computation tardiness by throttling request admissions and the processing precision. As a case study, we have implemented AutoMatrix, a GPU-based vehicle traffic simulator for real-time congestion management which scales up to 16 million vehicles on a US street map. This is an early effort to enable imprecise and approximate real-time computation on parallel architectures for stream-based time-bounded applications such as traffic congestion prediction and route allocation for large transportation networks.

Designing bug-free medical device software is challenging, especially in complex implantable devices that may be used in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems between 1990 and 2000 affected over 200, 000 devices. This encompasses 41% of the devices recalled and continues to increase in frequency. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to construct a timed-automata model by extracting timing properties of the heart. The platform employs functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has also been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. This integrated functional and formal device design approach has potential to help expedite medical device certification for safe operation.

Designing bug-free medical device software is difficult, especially in complex implantable devices that may be used in unanticipated contexts. In the 20-year period from 1985 to 2005, the US Food and Drug Administration's (FDA) Maude database records almost 30,000 deaths and almost 600,000 injuries from device failures [8]. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to extract timing properties of the heart to construct a timed-automata model. The platform exposes functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. The VHM allows for exploratory electrophysiology studies for physicians to evaluate their diagnosis and determine the appropriate device therapy. This integrated functional and formal device design approach will potentially help expedite medical device certification for safer operation.

Embedded wireless networks have largely focused on open-loop sensing and monitoring. To address actuation in closed-loop wireless control systems there is a strong need to re-think the communication architectures and protocols for reliability, coordination and control. As the links, nodes and topology of wireless systems are inherently unreliable, such time-critical and safety-critical applications require programming abstractions and runtime systems where the tasks are assigned to the sensors, actuators and controllers as a single component rather than statically mapping a set of tasks to a specific physical node at design time. To this end, we introduce the Embedded Virtual Machine (EVM), a powerful and flexible programming abstraction where virtual components and their properties are maintained across node boundaries. In the context of process and discrete control, an EVM is the distributed runtime system that dynamically selects primary-backup sets of controllers to guarantee QoS given spatial and temporal constraints of the underlying wireless network. The EVM architecture defines explicit mechanisms for control, data and fault communication within the virtual component. EVM-based algorithms introduce new capabilities such as predictable outcomes and provably minimal graceful degradation during sensor/actuator failure, adaptation to mode changes and runtime optimization of resource consumption. Through case studies in process control we demonstrate the preliminary capabilities of EVM-based wireless networks.

In many portable devices, wireless network interfaces consume upwards of 30% of scarce system energy. Reducing the transceiver's power consumption to extend the system lifetime has therefore become a design goal. Our work is targeted at this goal and is based on the following two observations. First, conventional energy management approaches have focused independently on minimizing the fixed energy cost (by shutdown) and on scalable energy costs (by leveraging, for example, the modulation, code-rate and transmission power). These two energy management approaches present a tradeoff. For example, lower modulation rates and transmission power minimize the variable energy component, but this shortens the sleep duration thereby increasing fixed energy consumption. Second, in order to meet the quality of service (QoS) timeliness requirements for multiple users, we need to determine to what extent each system in the network may sleep and scale. Therefore, we propose a two-phase methodology that resolves the sleep-scaling tradeoff across the physical, communications and link layers at design time and schedules nodes at runtime with near optimal energy-efficient configurations in the solution space. As a result, we are able to achieve very low run-time overheads. Our methodology is applied to a case study on delivering a guaranteed QoS for multiple users with MPEG-4 video over a slow-fading channel. By exploiting runtime controllable parameters of actual RF components and a modified 802.11 medium access controller, system lifetime is increased by a factor of 3-to-10 in comparison with conventional techniques.

Vehicular Ad hoc NETworks (VANETs) is a subclass of Mobile Ad hoc NETworks (MANETs). However, automotive ad hoc networks will behave in fundamentally different ways than the predominated models in MANET research. Driver behaviour, mobility constraints and high speeds create unique characteristics in the network. All of these constraints have implications on the VANET architecture at the physical, link, network, and application layers. To facilitate the cross-layer designs for VANETs, understanding of the relationship between mobility and network connectivity is of paramount importance. In this paper, we focus on studying transport systems with structured mobility (e.g., bus systems), which have unique characteristics on the road such as fixed routes that have never been explored in previous work. The main contributions of this paper are three-fold: 1) we provide an analytical framework including the design requirements of the mobility model for realistic vehicular network studies, and metrics for evaluating node connectivity in vehicular networks; 2) we demonstrate, through simulation, the impacts of marco- and micro-mobility models, and various transport elements on network connectivity; and 3) we show that multi-hop paths perform dramatically poorer than single-hop links in vehicular networks. Specifically, two- hop and three-hop (communication) paths can only respectively achieve less than 27% and 13% of the average duration of single-hop links. Such kind of knowledge of the performance of multi-hop transmission will be significant for the studies of routing algorithm and other networking functions in vehicular networks.

In many portable devices, wireless network interfaces consume upwards of 30% of scarce system energy. Reducing the transceiver's power consumption to extend the system lifetime has therefore become a design goal. Our work is targeted at this goal and is based on the following two observations. First, conventional energy management approaches have focused independently on minimizing the fixed energy cost (by shutdown) and on scalable energy costs (by leveraging, for example, the modulation, code-rate and transmission power). These two energy management approaches present a tradeoff. For example, lower modulation rates and transmission power minimize the variable energy component, but this shortens the sleep duration thereby increasing fixed energy consumption. Second, in order to meet the quality of service (QoS) timeliness requirements for multiple users, we need to determine to what extent each system in the network may sleep and scale. Therefore, we propose a two-phase methodology that resolves the sleep-scaling tradeoff across the physical, communications and link layers at design time and schedules nodes at runtime with near optimal energy-efficient configurations in the solution space. As a result, we are able to achieve very low run-time overheads. Our methodology is applied to a case study on delivering a guaranteed QoS for multiple users with MPEG-4 video over a slow-fading channel. By exploiting runtime controllable parameters of actual RF components and a modified 802.11 medium access controller, system lifetime is increased by a factor of 3-to-10 in comparison with conventional techniques

Multi-hop wireless networks facilitate applications in metropolitan area broadband, home multimedia, surveillance and industrial control networks. Many of these applications require high end-to- end throughput and/or bounded delay. Random access link-layer protocols such as carrier sense multiple access (CSMA) which are widely used in single-hop networks perform poorly in the multi-hop regime and provide no end-to-end QoS guarantees. The primary causes for their poor performance are uncoordinated interference and unfairness in exclusive access of the shared wireless medium. Furthermore, random access schemes do not leverage spatial reuse effectively and require routes to be link- aware. In this paper, we propose and study MAX, a time-division- multiplexed resource allocation framework for multi-hop networks with regular topologies. MAX tiling delivers optimal end-to-end throughput across arbitrarily large regularly structured networks while providing bounded delay. It outperforms CSMA-based random access protocols by a factor of 5 to 8. The MAX approach also supports network services including flexible uplink and downlink bandwidth management, deterministic route admission control, and optimal gateway placement. MAX has been implemented on IEEE 802.15.3 embedded nodes and a test-bed of 50 nodes has been deployed both indoors and outdoors.

Vehicular networks are being developed for efficient broadcast of safety alerts, real-time traffic congestion probing and for distribution of on-road multimedia content. In order to investigate vehicular networking protocols and evaluate the effects of incremental deployment it is essential to have a topology-aware simulation and test-bed infrastructure. While several traffic simulators have been developed under the intelligent transport system initiative, their primary motivation has been to model and forecast vehicle traffic flow and congestion from a queuing perspective. GrooveNet is a hybrid simulator which enables communication between simulated vehicles, real vehicles and between real and simulated vehicles. By modeling inter-vehicular communication within a real street map-based topography it facilitates protocol design and also in-vehicle deployment. GrooveNet's modular architecture incorporates mobility, trip and message broadcast models over a variety of link and physical layer communication models. It is easy to run simulations of thousands of vehicles in any US city and to add new models for networking, security, applications and vehicle interaction. GrooveNet supports multiple network interfaces, GPS and events triggered from the vehicle's on-board computer. Through simulation, we are able to study the message latency, and coverage under various traffic conditions. On-road tests over 400 miles lend insight to required market penetration

Wireless sensor networks have traditionally focused on low duty-cycle applications where sensor data are reported periodically in the order of seconds or even longer. This is due to typically slow changes in physical variables, the need to keep node costs low and the goal of extending battery lifetime. However, there is a growing need to support real-time streaming of audio and/or low-rate video even in wireless sensor networks for use in emergency situations and short-term intruder detection. In this paper, we present FireFly, a time-synchronized sensor network platform for real-time data streaming across multiple hops. FireFly is composed of several integrated layers including specialized low-cost hardware, a sensor network operating system, a real-time link layer and network scheduling which together provide efficient support for applications with timing constraints. In order to achieve high end-to-end throughput, bounded latency and predictable lifetime, we employ hardware-based time synchronization. Multiple tasks including audio sampling, networking and sensor reading are scheduled using the nano-RK RTOS. We have implemented RT-Link, a TDMA-based link layer protocol for message exchange on well-defined time slots and pipelining along multiple hops. We use this platform to support 2-way audio streaming concurrently with sensing tasks. For interactive voice, we investigate TDMA-based slot scheduling with balanced bi-directional latency while meeting audio timeliness requirements. Finally, we describe our experimental deployment of 42 nodes in a coal mine, and present measurements of the end-to-end throughput, jitter, packet loss and voice quality

We propose RT-link, a time-synchronized link protocol for real-time wireless communication in industrial control, surveillance and inventory tracking. RT-link provides predictable lifetime for battery-operated embedded nodes, bounded end-to-end delay across multiple hops, and collision-free operation. We investigate the use of hardware-based time-synchronization for infrastructure nodes by using an AM carrier-current radio for indoors and atomic clock receivers for outdoors. Mobile nodes are synchronized via in-band software synchronization within the same framework. We identify three key observations in the design and deployment of RT-link: (a) hardware-based global-time synchronization is a robust and scalable option to in-band software-based techniques, (b) achieving global time-synchronization is both economical and convenient for indoor and outdoor deployments, (c) RT-link achieves a practical lifetime of over 2 years. Through analysis and simulation, we show that RT-link outperforms energy-efficient link protocols such as B-MAC in terms of node lifetime and end-to-end latency. The protocol supports flexible services such as on-demand end-to-end rate control and logical topology control. We implemented RT-link on the CMU FireFly sensor platform and have integrated it within the nano-RK real-time sensor OS. A 42-node network with sub-20 mus synchronization accuracy has been deployed for 3 weeks in the NIOSH Mining Research Laboratory and within two 5-story campus buildings

In many devices, wireless network interfaces consume upwards of 30% of scarce portable system energy. Extending the system lifetime by minimizing communication power consumption has therefore become a priority. Conventional energy management techniques focus independently on minimizing the fixed energy consumption of the transceiver circuit or on scalable transmission control. Fixed energy consumption is reduced by maximizing the transceiver shutdown interval. In contrast, variable transmission rate, coding and power can be leveraged to minimize energy costs. These two energy management approaches present a tradeoff in minimizing the overall system energy. For example, variable energy costs are minimized by transmitting at a lower modulation rate and transmission power, but this also shortens the sleep duration thereby increasing fixed energy consumption. We present a methodology for energy-efficient resource allocation across the physical layer, communications layer and link layer. Our methodology is aimed at providing QoS for multiple users with bursty MPEG-4 video over a time-varying channel. We evaluate our scheme by exploiting control knobs of actual RF components over a modified IEEE 802.11 MAC. Our results indicate that the system lifetime is increased by a factor of 2 to 5 compared to the gains of conventional techniques.