SEARCH · Engineering Papers
Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.
Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.
The authors describe how to construct a hybrid control system using a specific set of data and conditions specified within the paper. Furthermore, they give examples of how to create continuous systems, discrete systems, and simple hybrid systems. Finally, they touch upon Heisenberg and state space representation.
Human interaction with a complex control system involves the user, the automation’s discrete mode logic, and the underlying continuous dynamics of the physical system. The user-interface of such systems always displays a reduced set of information about the entire system. Designing interfaces such that all the pertinent information is available and assuring that this information is correct is important for any user-interface, but especially so for safety-critical systems such as automotive systems and autopilots. Here we describe a methodology for the analysis of hybrid control systems that incorporate user interaction, with the goal of assuring that the information provided to the user is correct. That is, the user-interface must contain all information necessary to safely complete a desired procedure or task. We begin with a hybrid system model which incorporates discrete mode logic as well as nonlinear continuous dynamics. Using a hybrid computational tool for reachability, we find the largest region of the state-space in which we can guarantee the state of the system can always remain – this is the safe region of operation. By implementing a controller for safety which arises from this computation, we mathematically guarantee that this safe region is invariant, meaning that the system will always remain within the safe region if the determined controller is used on the boundary of the safe region. Verification within a hybrid framework allows us to account for the continuous dynamics underlying the discrete representations displayed to the user. Using the computed invariant regions as discrete states, we can abstract a discrete event system from this hybrid system with safety restrictions. This abstraction can be used to determine what information must be provided on the display. Furthermore, in cases in which an interface already exists, the abstraction provides the necessary input into existing interface verification methods. We provide two examples: a car traveling through a yellow light at an intersection and an aircraft autopilot in an automatic landing/go-around maneuver. The examples demonstrate the applicability of this methodology to hybrid systems that have operational constraints we can pose in terms of safety. This methodology differs from existing work in hybrid system verification in that we directly account for the user’s interactions with the system.
Savannah State University (SSU) and the Florida Solar Energy Center (FSEC) have been participating in the NASA Advanced Communications Technology Satellite (ACTS) program for the last five years. This program was designed by NASA to help maintain U.S. leadership in commercial space communications by funding high-risk research, and to flight-test next-generation digital satellite components. Launched in 1993, ACTS is an U.S. government funded technology test-bed that incorporates high power Ka-band transponders, small spot beams, and on-board digital storage and switching technology. Associated with the spacecraft, is a prototype satellite control center that supports various application experiments. The SSU/FSEC application experiment is to developing a Photovoltaic-Diesel Hybrid Power system complete with satellite Supervisory Control and Data Acquisition (SCADA). The hybrid system was design to demonstrate the feasibility of using SCADA to maintain and operate remote village power systems. This configuration would enable experts at a central location to provide technical assistance to local technicians while they acquire a measure of proficiency with the hybrid system operation and maintenance. Upon full mastery of the technology, similar SCADA arrangement are planned to remotely monitor and control constellation of hybrid systems scattered overlarge rural areas. Two Orion Energy APEX-1000 hybrid systems were delivered in 1998, one was installed at SSU in eastern Georgia and the other was installed at FSEC in Central Florida. The project was designed to: (1) evaluate the performance of ACTS in a SCADA arrangement, (2) monitor the health and performance of all major hybrid subsystems, (3) investigate load control and battery charging strategies to maximize battery capacity and lifetime, and (4) develop satellite communication protocol. Preliminary results indicate that the hybrid design is suitable for satellite Supervisory Control and Data Acquisition. A modification to the controller software has produced a robust communication link capable of real time control and long term data collection.
We examine a class of hybrid systems which we call Composite Hybrid Machines (CHM's) that consists of the concurrent (and partially synchronized) operation of Elementary Hybrid Machines (EHM's). Legal behavior, specified by a set of illegal configurations that the CHM may not enter, is to be achieved by the concurrent operation of the CHM with a suitably designed legal controller. In the present paper we focus on the problem of synthesizing a legal controller, whenever such a controller exists. More specifically, we address the problem of synthesizing the minimally restrictive legal controller. A controller is minimally restrictive if, when composed to operate concurrently with another legal controller, it will never interfere with the operation of the other controller and, therefore, can be composed to operate concurrently with any other controller that may be designed to achieve liveness specifications or optimality requirements without the need to reinvestigate or reverify legality of the composite controller. We confine our attention to a special class of CHM's where system dynamics is rate-limited and legal guards are conjunctions or disjunctions of atomic formulas in the dynamic variables (of the type x less than or equal to x(sub 0), or x greater than or equal to x(sub 0)). We present an algorithm for synthesis of the minimally restrictive legal controller. We demonstrate our approach by synthesizing a minimally restrictive controller for a steam boiler (the verification of which recently received a great deal of attention).
The behavior of a general hybrid system in discrete time can be represented by a non-linear difference equation x(k+1) = Fk(x(k), theta(k)), where theta(k) is assumed to be a finite state Markov chain. An important step in the stability analysis of these systems is to establish the Markov property of (x(k), theta(k)). There are, however, no complete proofs of this property which are simple to understand. This paper aims to correct this problem by presenting a complete and explicit proof, which uses only basic measure-theoretical concepts.
Fifty operational segments from the U.S.S.R., 40 test segments from Canada, and 24 test segments from the United States were used to provide a wide range of geographic conditions for USDA analysts during a test to determine the effectiveness of labeling single pixel training fields (dots) using Procedure 1 on the 1-100 hybrid system, and clustering and classifying on the Earth Resources Interactive Processing System. The analysts had additional on-line capabilities such as interactive dot labeling, class or cluster map overlay flickers, and flashing of all dots of equal spectral value. Results on the 1-100 hybrid system are described and analyst problems and recommendations are discussed.
This research is directed towards the implementation of a comprehensive deductive-algorithmic environment (toolkit) for the development and verification of high assurance reactive systems, especially concurrent, real-time, and hybrid systems. For this, we have designed and implemented the STCP (Stanford Temporal Prover) verification system. Reactive systems have an ongoing interaction with their environment, and their computations are infinite sequences of states. A large number of systems can be seen as reactive systems, including hardware, concurrent programs, network protocols, and embedded systems. Temporal logic provides a convenient language for expressing properties of reactive systems. A temporal verification methodology provides procedures for proving that a given system satisfies a given temporal property. The research covered necessary theoretical foundations as well as implementation and application issues.
The design and the performance of an electrostatic-acoustic hybrid system and its application to a charge drop rotation experiment are presented. This system can levitate a charged drop electrostatically and induce drop rotation or oscillation by imposing an acoustic torque or an oscillating acoustic pressure. Using this system, the equilibrium shapes and stability of a rotating charged drop were experimentally investigated. A 3 mm size water drop was rotated as a rigid body and its gyrostatic equilibrium shapes were observed. Families of axisymmetric shapes, two-lobed shapes, and eventual fissioning have been observed. With the assumption of 'effective surface tension' in which the surface charge simply modified the surface tension of neutral liquid, the results agree exceptionally well with the Brown and Scriven's (1980) prediction for uncharged drops.
We demonstrate spin pumping driven by a strongly coupled magnon-photon system using a ferromagnet-coplanar superconducting resonator hybrid system at 1.4 K. Electrical readout via the inverse spin-Hall effect reveals characteristic coupling features, including mode splitting and linewidth broadening, demonstrating the electrical detection of strongly coupled microwave photons and magnons. The microwave magnon-photon coupling strength obtained by combined spin pumping and inverse spin-Hall effect measurements is compared to microwave transmission experiments. Here, microwave power-dependent measurements reveal a decrease in the coupling strength with increasing microwave power alongside the onset of nonlinearities of the superconducting resonator above a critical microwave power threshold.
The research is directed towards the design and implementation of a comprehensive deductive environment for the development of high-assurance systems, especially reactive (concurrent, real-time, and hybrid) systems. Reactive systems maintain an ongoing interaction with their environment, and are among the most difficult to design and verify. The project aims to provide engineers with a wide variety of tools within a single, general, formal framework in which the tools will be most effective. The entire development process is considered, including the construction, transformation, validation, verification, debugging, and maintenance of computer systems. The goal is to automate the process as much as possible and reduce the errors that pervade hardware and software development.
Hybrid electric powertrains are a growing market in medium- and heavy-duty applications. There is a lack of available information to understand the challenges in the integration of engine platforms into electrified powertrains, such as cold-start, restart, and load-reduction effects on emissions and emission control devices. Results from the Heavy Heavy-Duty Diesel Truck (HHDDT) cycle using a conventional medium-duty diesel engine were compared with those of a parallel hybrid architecture. Oak Ridge National Laboratory in collaboration with the US Department of Energy and Odyne Systems, LLC developed a powertrain in a hardware-in-the-loop environment, integrating the Odyne Systems, LLC medium-duty parallel hybrid system, which was used for the hybrid portion of this study. Experiments under the HHDDT cycle showed increasing improvements in fuel consumption and engine-out emissions with the integration of stop/start, hybrid, and hybrid with stop/start. However, the effects of load reduction and exhaust temperature on the thermal management strategy have shown an increase in fueling in the second part of the HHDDT cycle. Four configurations of medium-duty electrification were studied and contributed to building a unique data set containing combustion, emissions, and system integration data. Each electrification level was compared with the conventional baseline. The calibration of the conventional engine was not altered for this study. Opportunities to tailor the combustion process were identified with the stop/start strategy.
This study proposes a method of predicting the influence of random load behavior on the dynamics of dc microgrids and distribution systems. This is accomplished by combining stochastic load models and deterministic microgrid models. Together, these elements constitute a stochastic hybrid system. The resulting model enables straightforward calculation of dynamic state moments, which are used to assess the probability of desirable operating conditions. Specific consideration is given to systems based on the dual active bridge (DAB) topology. Bounds are derived for the probability of zero voltage switching (ZVS) in DAB converters. A simple example is presented to demonstrate how these bounds may be used to improve ZVS performance as an optimization problem. In conclusion, predictions of state moment dynamics and ZVS probability assessments are verified through comparisons to Monte Carlo simulations.
In the present work we model multi-lane traffic flow in presence of two population of vehicles: cars and trucks. We first develop a finite-dimensional hybrid system which rely on continuous Bando-Follow-the-Leader dynamics coupled with discrete events motivated by the lane-change maneuvers. Then we rigorously prove that the mean-field limit is given by a system of Vlasov-type PDE with source terms generated by the lane-change maneuvers of the human-driven vehicles.
Compositional verification techniques in the assume- guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata.
The aim of this research is to develop new mathematical methodology for the analysis of hybrid systems of the type involved in Air Traffic Control (ATC) problems. Two directions of investigation were initiated. The first used the methodology of nonlinear generalized functions, whose mathematical foundations were initiated by Colombeau and developed further by Oberguggenberger; it has been extended to apply to ordinary differential. Systems of the type encountered in control in joint work with the PI and M. Oberguggenberger. This involved a 'mixture' of 'continuous' and 'discrete' methodology. ATC clearly involves mixtures of two sorts of mathematical problems: (1) The 'continuous' dynamics of a standard control type described by ordinary differential equations (ODE) of the form: {dx/dt = f(x, u)} and (2) the discrete lattice dynamics involved of cellular automata. Most of the CA literature involves a discretization of a partial differential equation system of the type encountered in physics problems (e.g. fluid and gas problems). Both of these directions requires much thinking and new development of mathematical fundamentals before they may be utilized in the ATC work. Rather than consider CA as 'discretization' of PDE systems, I believe that the ATC applications will require a completely different and new mathematical methodology, a sort of discrete analogue of jet bundles and/or the sheaf-theoretic techniques to topologists. Here too, I have begun work on virtually 'virgin' mathematical ground (at least from an 'applied' point of view) which will require considerable preliminary work.
Low thrust reaction control for space missions, summarizing range and specific impulse characteristics for solid and hybrid systems
An approximation scheme is developed for the identification of hybrid systems describing the transverse vibrations of flexible beams with attached tip bodies. In particular, problems involving the estimation of functional parameters are considered. The identification problem is formulated as a least squares fit to data subject to the coupled system of partial and ordinary differential equations describing the transverse displacement of the beam and the motion of the tip bodies respectively. A cubic spline-based Galerkin method applied to the state equations in weak form and the discretization of the admissible parameter space yield a sequence of approximating finite dimensional identification problems. It is shown that each of the approximating problems admits a solution and that from the resulting sequence of optimal solutions a convergent subsequence can be extracted, the limit of which is a solution to the original identification problem. The approximating identification problems can be solved using standard techniques and readily available software.
This paper is concerned with the design, simulation, and implementation of a hybrid system using the GMSK type of signal format for phase modulation and demodulation. The performance of the designed transceiver structure is evaluated using the bit error rate (BER) curves. The simulated system was also successfully implemented in real time.