The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems; however, state-of-the-art theorem provers require manual intervention to handle complex systems. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assistance that a system designer is able to provide directly. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about performance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage forward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing automatic verification approaches using several examples, including one involving an automotive powertrain control system.

In model-based development, abstraction provides insight and tractability. Different formalisms are often used at different levels of abstraction to represent the variety of concerns that need to be addressed when designing complex cyber-physical systems. In this paper, we consider the problem of establishing abstraction across heterogeneous formalisms in a compositional manner. We use the framework of behavioral semantics to elucidate the general conditions that must be satisfied to assure that the composition of abstractions for individual components is an abstraction for the composition of the components. The theoretical concepts are illustrated using an example of a cooperative intersection collision avoidance system (CICAS).

Although a growing number of dynamical systems studied in various fields are hybrid in nature, the verification of properties, such as stability, safety, etc., is still a challenging problem. Reachability analysis is one of the promising methods for hybrid system verification, which together with all other verification techniques faces the challenge of making the analysis scale with respect to the number of continuous state variables. The bottleneck of many reachability analysis techniques for hybrid systems is the geometrically computed intersection with guard sets. In this work, we replace the intersection operation by a nonlinear mapping onto the guard, which is not only numerically stable, but also scalable, making it possible to verify systems which were previously out of reach. The approach can be applied to the fairly common class of hybrid systems with piecewise continuous solutions, guard sets modeled as halfspaces, and urgent semantics, i.e. discrete transitions are immediately taken when enabled by guard sets. We demonstrate the usefulness of the new approach by a mechanical system with backlash which has 101 continuous state variables.

Today's complex cyber-physical systems are being built increasingly using model-based development (MBD), where mathematical models for the system behavior are checked against design specifications using analysis tools. Different types of models and analysis tools are used to address different aspects of the system. While the use of heterogeneous formalisms supports a divide-and-conquer approach to complexity and allows engineers with different types of expertise to work on various aspects of the design, system integration problems can arise due to the lack of an underlying unifying formalism. In this paper, we introduce the notion of behavior relations to address the problem of heterogeneity and propose constraints over parameters as a mechanism to manage inter-model dependencies and ensure consistency. In addition, we present structured constructs of nested conjunctive and disjunctive analyses to enable multi-model heterogeneous verification. The theoretical concepts are illustrated using an example of a cooperative intersection collision avoidance system (CICAS).

This paper presents data centers from a cyber–physical system (CPS) perspective. Current methods for controlling information technology (IT) and cooling technology (CT) in data centers are classified according to the degree to which they take into account both cyber and physical considerations. To evaluate the potential impact of coordinated CPS strategies at the data center level, we introduce a control-oriented model that represents the data center as two coupled networks: a computational network representing the cyber dynamics and a thermal network representing the physical dynamics. These networks are coupled through the influence of the IT on both networks: servers affect both the quality of service (QoS) delivered by the computational network and the generation of heat in the thermal network. Using this model, three control strategies are evaluated with respect to their energy efficiency and computational performance: a baseline strategy that ignores CPS considerations, an uncoordinated strategy that manages the IT and CT independently, and a coordinated strategy that manages the IT and CT together to achieve optimal performance with respect to both QoS and energy efficiency. Simulation results show that the benefits to be realized from coordinating the control of IT and CT depend on the distribution and heterogeneity of the computational and cooling resources throughout the data center. A new cyber–physical index (CPI) is introduced as a measure of this combined distribution of cyber and physical effects in a given data center. We illustrate how the CPI indicates the potential impact of using coordinated CPS control strategies.

This paper presents a method for using set-based approximations to the Peano-Baker series to compute overapproximations of reachable sets for linear systems with uncertain, time-varying parameters and inputs. Alternative representations for sets of uncertain system matrices are considered, including matrix polytopes, matrix zonotopes, and interval matrices. For each representation, the computational efficiency and resulting approximation error for reachable set computations are evaluated analytically and empirically. As an application, reachable sets are computed for a truck with hybrid dynamics due to a gain-scheduled yaw controller. As an alternative to computing reachable sets for the hybrid model, for which switching introduces an additional overapproximation error, the gain-scheduled controller is approximated with uncertain time-varying parameters, which leads to more efficient and more accurate reachable set computations.

We present an approach for verifying locking of charge-pump phase-locked loops by performing reachability analysis on a behavioral model of the circuit. Bounded uncertain parameters in the behavioral model make it possible to represent all possible behaviors of more detailed models. The dynamics of the behavioral model is hybrid (i.e., discrete and continuous) due to the switching of charge pumps that drive the analog control circuits. A unique feature of phase-locked loops compared to most other hybrid systems is that they require thousands of switchings in the continuous dynamics to converge sufficiently close to a limit cycle. This makes reachability analysis a challenging task since switches in the dynamics are expensive to compute and result in conservative overapproximations. We solve this problem by overapproximating the effects of the switching conditions with uncertain parameters in linear continuous models, a method we call continuization. Using efficient reachability algorithms for discrete-time linear systems, locking is verified over the complete range of possible initial states of a charge-pump PLL designed in 32nm CMOS SOI technology in comparable time required for Monte Carlo simulations of the same behavioral model.

This paper surveys major technical challenges for power system operations in support of large-scale wind energy integration. The fundamental difficulties of integrating wind power arise from its high inter-temporal variation and limited predictability. The impact of wind power integration is manifested in, but not limited to, scheduling, frequency regulations, and system stabilization requirements. Possible alternatives are suggested for a more reliable and cost-effective power system operation. New computationally efficient methods for improving system performances by using prediction and operational interdependencies over different time horizons remain critical open research problems.

This paper concerns the use of large-scale wireless sensor networks to detect and locate leaks of specified gases in the presence of time-varying advection (air currents) and diffusion. We show that when leaks are rare but constant for long periods, Kalman filtering combined with binary hypothesis testing provides an effective alternative to full-scale hypothesis testing covering all possible combinations of leaks and leak intensities. To reduce energy consumption and use of communication bandwidth, a two-tiered strategy is proposed in which a reduced number of sensors (Tier 1) provides coarse-grid sensing. When a leak is detected by the Tier 1 strategy, fine-grained grids of sensors (Tier 2) are activated around the vicinities of the detected leak areas to provide more precise detection and localization. Energy consumption is further reduced by applying an information versus energy-based dynamic sensor selection technique. Details of a laboratory implementation are presented and simulation results illustrate the approach and demonstrate its effectiveness.

Properties of analog circuits can be verified formally by partitioning the continuous state space and applying hybrid system verification techniques to the resulting abstraction. To verify properties of oscillator circuits, cyclic invariants need to be computed. Methods based on forward reachability have proven to be inefficient and in some cases inadequate in constructing these invariant sets. In this paper, we propose a novel approach combining forward- and backward-reachability while iteratively refining partitions at each step. The technique can yield dramatic memory and runtime reductions. We illustrate the effectiveness by verifying, for the first time, the limit cycle oscillation behavior of a third-order model of a differential VCO circuit

In previous work, we presented a method for constructing dynamic input-output models for real-time state estimation in correlated dynamic fields using wireless sensor networks (WSNs). The input signals correspond to the sensors on the boundary of the physical space under study, reflecting the assumption there are no independent sources in the interior of the region. In this paper, we present a method to identify sensors not on the boundary that should be used as inputs in the dynamic models when there are inner sources, i.e., sources inside the physical space. We extend concepts from the behavioral model theory of Jan Willems to handle noisy time series. We construct a block-Hankel structured matrix based on the sensor data, and then calculate as an independence indicator the angle between each row of the matrix and the subspace determined by the span of the preceding rows. The inner sources are identified based on these angle values. Experimental results with real temperature data collected with a WSN, and including heat sources as inner sources, illustrate the proposed method.

This article describes one of the major efforts in the sensor network community to build an integrated sensor network system for surveillance missions. The focus of this effort is to acquire and verify information about enemy capabilities and positions of hostile targets. Such missions often involve a high element of risk for human personnel and require a high degree of stealthiness. Hence, the ability to deploy unmanned surveillance missions, by using wireless sensor networks, is of great practical importance for the military. Because of the energy constraints of sensor devices, such systems necessitate an energy-aware design to ensure the longevity of surveillance missions. Solutions proposed recently for this type of system show promising results through simulations. However, the simplified assumptions they make about the system in the simulator often do not hold well in practice, and energy consumption is narrowly accounted for within a single protocol. In this article, we describe the design and implementation of a complete running system, called VigilNet, for energy-efficient surveillance. The VigilNet allows a group of cooperating sensor devices to detect and track the positions of moving vehicles in an energy-efficient and stealthy manner. We evaluate VigilNet middleware components and integrated system extensively on a network of 70 MICA2 motes. Our results show that our surveillance strategy is adaptable and achieves a significant extension of network lifetime. Finally, we share lessons learned in building such an integrated sensor system.

In many sensor networks applications, sensors collect correlated measurements of a physical field, e.g., temperature field in a building or in a data center. However, the locations of the sensors are usually inconsistent with the application requirements. In this paper, we consider the problem of estimating the field at arbitrary positions of interest, where there are possibly no sensors, from the irregularly placed sensors. We map this sensor network on a graph, and, by introducing the concepts of interconnection matrices, system digraphs, and cut point sets, we can pose sensor network tradeoffs and derive real-time field estimation algorithms. The results of temperature field estimation, obtained from simulations and real world experiments, show that the methodology presented in this paper can successfully predict the field values at arbitrary locations, including others than the ones with sensors.

A wide variety of sensors have been incorporated into a spectrum of wireless sensor network (WSN) platforms, providing flexible sensing capability over a large number of low-power and inexpensive nodes. Traditional signal processing algorithms, however, often prove too complex for energy-and-cost-effective WSN nodes. This study explores how to design efficient sensing and classification algorithms that achieve reliable sensing performance on energy-and-cost effective hardware without special powerful nodes in a continuously changing physical environment. We present the detection and classification system in a cutting-edge surveillance sensor network, which classifies vehicles, persons, and persons carrying ferrous objects, and tracks these targets with a maximum error in velocity of 15%. Considering the demanding requirements and strict resource constraints, we design a hierarchical classification architecture that naturally distributes sensing and computation tasks at different levels of the system. Such a distribution allows multiple sensors to collaborate on a sensor node, and the detection and classification results to be continuously refined at different levels of the WSN. This design enables reliable detection and classification without involving high-complexity computation, reduces network traffic, and emphasizes resilience and adaptation to the realistic environment. We evaluate the system with performance data collected from outdoor experiments and field assessments. Based on the experience acquired and lessons learned when developing this system, we abstract common issues and introduce several guidelines which can direct future development of detection and classification solutions based on WSNs.

Dynamic power management aims at extending battery life by switching devices to lower-power modes when there is a reduced demand for service. Static power management strategies can lead to poor performance or unnecessary power consumption when there are wide variations in the rate of requests for service. This paper presents a hierarchical scheme for adaptive dynamic power management (DPM) under nonstationary service requests. As the main theoretical contribution, we model the nonstationary request process as a Markov-modulated process with a collection of modes, each corresponding to a particular stationary request process. Optimal DPM policies are precalculated offline for selected modes using standard algorithms available for stationary Markov decision processes (MDPs). The power manager then switches online among these policies to accommodate the stochastic mode-switching request dynamics using an adaptive algorithm to determine the optimal switching rule based on the observed sample path. As a target application, we present simulations of hierarchical DPM for hard disk drives where the read/write request arrivals are modeled as a Markov-modulated Poisson process. Simulation results show that the power consumption of our approach under highly nonstationary request arrivals is less than that of a previously proposed heuristic approach and is even comparable to that of the optimal policy under stationary Poisson request process with the same arrival rate as the average arrival rate of the nonstationary request process.

Embedded systems encompass a wide range of applications, technologies, and disciplines, necessitating a broad approach to education. We describe embedded system coursework during the first 4 years of university education (the U.S. undergraduate level). Embedded application curriculum areas include: small and single-microcontroller applications, control systems, distributed embedded control, system-on-chip, networking, embedded PCs, critical systems, robotics, computer peripherals, wireless data systems, signal processing, and command and control. Additional cross-cutting skills that are important to embedded system designers include: security, dependability, energy-aware computing, software/systems engineering, real-time computing, and human--computer interaction. We describe lessons learned from teaching courses in many of these areas, as well as general skills taught and approaches used, including a heavy emphasis on course projects to teach system skills.

The main contribution of this paper is a novel hierarchical scheme for adaptive dynamic power management (DPM) under nonstationary service requests. We model the nonstationary arrival process of service requests as a Markov-modulated stochastic process in which the stochastic process for each modulation state models a particular stationary mode of the arrival process. The bottom layer of our hierarchical architecture is a set of stationary optimal DPM policies, pre-calculated off-line for selected modes from policy optimization in Markov decision processes. The supervisory power manager at the top layer adaptively and optimally switches among these stationary policies on-line to accommodate the actual mode-switching arrival dynamics. Simulation results show that our approach, under highly nonstationary requests, can lead to significant power savings compared to previously proposed heuristic approaches.

We show how model checking methods developed for hybrid dynamic systems may be usefully applied for analog circuit verification. Finite-state abstractions of the continuous analog behavior are automatically constructed using polyhedral outer approximations to the flows of the underlying continuous differential and difference equations. In contrast to previous approaches, we do not discretize the entire continuous state space, and our abstraction captures the relevant behaviors for verification in terms of the transitions between "states" (regions of the continuous state space) as a finite state machine in the hybrid system model. The approach is illustrated for two circuits, a standard oscillator benchmark, and a much larger and more realistic delta-sigma (AI) modulator.

The focus of surveillance missions is to acquire and verify information about enemy capabilities and positions of hostile targets. Such missions often involve a high element of risk for human personnel and require a high degree of stealthiness. Hence, the ability to deploy unmanned surveillance missions, by using wireless sensor networks, is of great practical importance for the military. Because of the energy constraints of sensor devices, such systems necessitate an energy-aware design to ensure the longevity of surveillance missions. Solutions proposed recently for this type of system show promising results through simulations. However, the simplified assumptions they make about the system in the simulator often do not hold well in practice and energy consumption is narrowly accounted for within a single protocol. In this paper, we describe the design and implementation of a running system for energy-efficient surveillance. The system allows a group of cooperating sensor devices to detect and track the positions of moving vehicles in an energy-efficient and stealthy manner. We can trade off energy-awareness and surveillance performance by adaptively adjusting the sensitivity of the system. We evaluate the performance on a network of 70 MICA2 motes equipped with dual-axis magnetometers. Our results show that our surveillance strategy is adaptable and achieves a significant extension of network lifetime. Finally, we share lessons learned in building such a complete running system.

The planning problem for a mobile manipulator system that must perform a sequence of tasks defined by position, orientation, force, and moment vectors at the end-effector is considered. Each task can be performed in multiple configurations due to the redundancy introduced by mobility. The planning problem is formulated as an optimization problem in which the decision variables for mobility (base position) are separated from the manipulator joint angles in the cost function. The resulting numerical problem is nonlinear with nonconvex, unconnected feasible regions in the decision space. Simulated annealing is proposed as a general solution method for obtaining near-optimal results. The problem formulation and numerical solution by simulated annealing are illustrated for a manipulator system with three degrees of freedom mounted on a base with two degrees of freedom. The results are compared with results obtained by conventional nonlinear programming techniques customized for the particular example system.>

The planning problem is considered for a mobile manipulator system which must perform a sequence of tasks defined by position, orientation, force, and moment vectors at the end effector. Each task can be performed in multiple configurations due to the redundancy introduced by mobility. The planning problem is formulated as an optimization problem in which the decision variables for mobility (base position) are separated from the manipulator joint angles in the cost function. The resulting numerical problem is nonlinear with nonconvex, unconnected feasible regions in the decision space. Simulated annealing is proposed as a general solution method for obtaining near-optimal results. The problem formulation and numerical solution by simulated annealing are illustrated for a positioning system with five degrees of freedom. These results are compared with results obtained by conventional nonlinear programming techniques customized for the particular example system.>

An algorithm is presented for dynamically steering an autonomous mobile robot (AMR) along a collision-free path to a goal using local feedback information. A two-level navigation algorithm is presented in which a subgoal selection algorithm (SSA) generates visible subgoals to be pursued by the steering control algorithm (SCA). The authors focus on the SCA. In particular, a general feedback scheme is developed for dynamically steering an ARM to a visible goal in the local obstacle-free space identified by the SSA. The detailed implementation of the SCA for a conventionally steered AMR (CAMR) is presented. Simulation results are presented which demonstrate the effectiveness of the combined SSA-SCA feedback scheme.>

Production allocation in multicell manufacturing systems is considered. A model is developed for a hierarchical control scheme, where each cell consists of several failure-prone machines for which the time scale of the machine state transitions is comparable to the processing times. The production objective is to track a nonstationary demand as closely as possible when the demand is near or exceeds the capacity of the system. A series of approximations is proposed to obtain a model that is realistic while admitting a tractable solution. To solve the resulting stochastic control problem, a general result is derived on the second-order finite-time (transient) statistics of a continuous-time Markov chain. Simulation results are presented to illustrate the proposed model and control methodology. These results are compared with a myopic linear programming approach.>

The concurrent flow of multiple jobs through a FMS can lead to deadlock conditions due to competition for limited resources in the system. The authors develop a Petri net (PN) model of concurrent job flow and dynamic resource allocation in an FMS and define deadlock in terms of transition enabling in the PN model. The problem of deadlock avoidance is addressed by introducing the notion of a restriction policy, which is a feedback policy for excluding some enabled transitions from the current resource allocation alternatives. The authors then present their deadlock avoidance algorithm (DAA) and prove that restricted deadlock can never occur for any resource allocation policy implemented under the DAA restriction policy. The DAA can be implemented easily in real time and is much less restrictive for FMS applications than existing algorithms for deadlock avoidance in computer systems. Application of the DAA is illustrated for three FMS examples: allocation of finite buffer space in a multicell machining facility, collision avoidance in a multirobot assembly cell, and coordination of multiple AGVs on a shop floor.>

An approach is presented for the specification, modeling, and analysis of discrete-state systems and controllers. The approach features a rule-based state-variable-specification formalism that is translated into Petri net models composed of interconnected state machines. The concept of reduced reachability graphs is introduced as a means of reducing the computational effort required to isolate and analyze subcomponent behavior within the system. The target application is discrete manufacturing systems where the costs involved in writing, debugging, and maintaining of code for online process control can be significantly reduced through the use of automated modeling and analysis techniques. The approach is illustrated by an example of a simple discrete-state system.>

A general approach to the local navigation problem for autonomous mobile robots (AMRs) is presented and its application to omnidirectional and conventionally steered wheelbases is described. The problem of driving an AMR to a goal in an unknown environment is formulated as a dynamic feedback control problem in which local feedback information is used to make steering decisions while the AMR is moving. To obtain a computationally tractable algorithm, a class of satisficing feedback strategies that generate reasonable, collision-free trajectories to the goal using simplified representations of the AMR dynamics and constrains is proposed. Realizations of the feedback strategy are presented and illustrated by simulation under the assumptions of perfect feedback information and zero servo error. Straightforward extensions of the approach to handle uncertainties in real systems are briefly described.>

The authors describe the design and implementation of a motor drive control system for an omnidirectional wheelbase, the Ilonator platform, developed at the Robotics Institute at Carnegie Mellon University. The experimental mobile platform is mounted on four omnidirectional wheels which permit a full three degrees of freedom (3 DOF) in the plane. The distributed servo-control system is coordinated by onboard computer which converts 3-DOF acceleration commands into individual velocity commands for the four wheels. Four HCTL-1000 motor control chips close the velocity-control feedback loops for the wheels. Details of the platform kinematics and motion command structure, servo hardware design and implementation, software for command and joystick control, and the experimental tuning of the controller parameters are presented.>

The acceleration radius is defined as a global index for quantifying the dynamic capabilities of manipulator-positioning systems over a continuous operation region. It is generalization of previously proposed manipulability indices that are local measures of the acceleration capability. The problem of computing the acceleration radius is formulated as an optimization problem. A numerical algorithm for solving the resulting generalized semi-infinite program is presented, and the application of the acceleration radius concept to examples of manipulator design and workspace specification is illustrated. Several directions for future research are discussed.>

Recently, there has been substantial interest in multi-stage, multi-cell Flexible Assembly Systems for Electronic (Printed Circuit Board) Assembly. Previous work (Akella et.al 1984: Gershwin et.al. 1985; Akella and Kumar, 1986) has concerned real-time dispatch in single cells. There has also been related work on design and production allocation in multi-cell systems by Yao and Shanthikumar (1985, 1986). Here, we formulate and compute approximate solutions to a generic multi-cell, failure prone system with a hierarchical control system.

Qualitative properties of Petri nets (such as liveness and safeness) are useful in discrete manufacturing applications since they correspond to consistent, deadlock-free control logic. In this paper we introduce the qualitative property of essentially decision free (EDF) places in Petri nets (PNs) to represent the absence of unresolved (nonunique) resource allocation conditions. We show that a previously developed method for PN synthesis of on-line control logic may lead to ambiguous resource allocation conditions which are exhibited in the PN model us non-EDF places. Using the theory of place-invariants, we develop a procedure for identifying non-EDF places in the synthesized logic. The procedure is illustrated for an example of assigning robots to tasks in a flexible assembly cell. For this example, allocation ambiguities are systematically resolved by introducing logical NOT conditions in the PN model.

A methodology is presented for constructing models of manufacturing processes for simulation and design of the discrete control logic. The models represent the discrete event evolution of the system as well as features of the underlying continuous processes. For applications such as discrete parts manufacture and assembly, the process is decomposed into operations with specified precedence relations. For each operation the required resources and associated discrete resource states are identified. Also associated with each resource is a set of resource attributes which are modified by the processes underlying each operation. The structure of the discrete-level control is modeled by modified Petri nets which are synthesized from single resource activity cycles. Construction of the net provides discrete control logic for error recovery loops and other real-time decision structures with guaranteed properties based on extensions of previous results in Petri net theory. The modeling methodology is applied to a two-arm robotic assembly cell example.

A method is presented for combining two previously proposed algorithms for path-planning and dynamic steering control into a computationally feasible scheme for real-time feedback control of autonomous vehicles in uncertain environments. In the proposed approach to vehicle guidance and control, Path Relaxation is used to compute critical points along a globally desirable path using a priori information and sensor data. Generalized potential fields are then used for local feedback control to drive the vehicle along a collision-free path using the critical points as subgoals. Simulation results are presented to demonstrate the control scheme.

This paper describes the analysis and implementation of a motor drive control system for an intelligent wheelchair being developed at the Robotics Institute at Carnegie-Mellon University. The experimental mobile platform is mounted on four so-called Ilonators which permit motion in any direction without conventional steering of the wheel axes. The kinematics of the platform were determined analytically and a simulation program was developed to generate reference wheel velocity trajectories corresponding to several basic platform trajectories. These reference trajectories were used to drive the platform under open-loop control. The paper includes a description of the motor-drive hardware implementation, and experimental results. The results of this work provide the foundation for the implementation of feedback control of the wheels and higher-level supervisory control.