Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “logic”

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.

At least 1,225 records · Page 68

Experimental Verification of Electric Drive Technologies Based on Artificial Intelligence Tools

In this report, a fully integrated prototype of a flight servo control system is successfully developed and implemented using brushless dc motors. The control system is developed by the fuzzy logic theory, and implemented with a multilayer neural network. First, a neural network-based architecture is introduced for fuzzy logic control. The characteristic rules and their membership functions of fuzzy systems are represented as the processing nodes in the neural network structure. The network structure and the parameter learning are performed simultaneously and online in the fuzzy-neural network system. The structure learning is based on the partition of input space. The parameter learning is based on the supervised gradient decent method, using a delta adaptation law. Using experimental setup, the performance of the proposed control system is evaluated under various operating conditions. Test results are presented and discussed in the report. The proposed learning control system has several advantages, namely, simple structure and learning capability, robustness and high tracking performance and few nodes at hidden layers. In comparison with the PI controller, the proposed fuzzy-neural network system can yield a better dynamic performance with shorter settling time, and without overshoot. Experimental results have shown that the proposed control system is adaptive and robust in responding to a wide range of operating conditions. In summary, the goal of this study is to design and implement-advanced servosystems to actuate control surfaces for flight vehicles, namely, aircraft and helicopters, missiles and interceptors, and mini- and micro-air vehicles.

Rubaai, Ahmed↗

Java Application Shell: A Framework for Piecing Together Java Applications

This session describes the architecture of Java Application Shell (JAS), a Swing-based framework for developing interactive Java applications. Java Application Shell is being developed by Commerce One, Inc. for NASA Goddard Space Flight Center Code 588. The purpose of JAS is to provide a framework for the development of Java applications, providing features that enable the development process to be more efficient, consistent and flexible. Fundamentally, JAS is based upon an architecture where an application is considered a collection of 'plugins'. In turn, a plug-in is a collection of Swing actions defined using XML and packaged in a jar file. Plug-ins may be local to the host platform or remotely-accessible through HTTP. Local and remote plugins are automatically discovered by JAS upon application startup; plugins may also be loaded dynamically without having to re-start the application. Using Extensible Markup Language (XML) to define actions, as opposed to hardcoding them in application logic, allows easier customization of application-specific operations by separating application logic from presentation. Through XML, a developer defines an action that may appear on any number of menus, toolbars, and buttons. Actions maintain and propagate enable/disable states and specify icons, tool-tips, titles, etc. Furthermore, JAS allows actions to be implemented using various scripting languages through the use of IBM's Bean Scripting Framework. Scripted action implementation is seamless to the end-user. In addition to action implementation, scripts may be used for application and unit-level testing. In the case of application-level testing, JAS has hooks to assist a script in simulating end-user input. JAS also provides property and user preference management, JavaHelp, Undo/Redo, Multi-Document Interface, Single-Document Interface, printing, and logging. Finally, Jini technology has also been included into the framework by means of a Jini services browser and the ability to associate services with actions. Several Java technologies have been incorporated into JAS, including Swing, Internal Frames, Java Beans, XML, JavaScript, JavaHelp, and Jini. Additional information is contained in the original extended abstract.

Miller, Philip↗

Self-Tuning of Design Variables for Generalized Predictive Control

Three techniques are introduced to determine the order and control weighting for the design of a generalized predictive controller. These techniques are based on the application of fuzzy logic, genetic algorithms, and simulated annealing to conduct an optimal search on specific performance indexes or objective functions. Fuzzy logic is found to be feasible for real-time and on-line implementation due to its smooth and quick convergence. On the other hand, genetic algorithms and simulated annealing are applicable for initial estimation of the model order and control weighting, and final fine-tuning within a small region of the solution space, Several numerical simulations for a multiple-input and multiple-output system are given to illustrate the techniques developed in this paper.

Lin, Chaung↗

Fundamentals of Digital Engineering: Designing for Reliability

The concept of designing for reliability will be introduced along with a brief overview of reliability, redundancy and traditional methods of fault tolerance is presented, as applied to current logic devices. The fundamentals of advanced circuit design and analysis techniques will be the primary focus. The introduction will cover the definitions of key device parameters and how analysis is used to prove circuit correctness. Basic design techniques such as synchronous vs asynchronous design, metastable state resolution time/arbiter design, and finite state machine structure/implementation will be reviewed. Advanced topics will be explored such as skew-tolerant circuit design, the use of triple-modular redundancy and circuit hazards, device transients and preventative circuit design, lock-up states in finite state machines generated by logic synthesizers, device transient characteristics, radiation mitigation techniques. worst-case analysis, the use of timing analyzer and simulators, and others. Case studies and lessons learned from spaceflight designs will be given as examples

Katz, R.↗

Institution Morphisms

Institutions formalize the intuitive notion of logical system, including both syntax and semantics. A surprising number of different notions of morphisim have been suggested for forming categories with institutions as objects, and a surprising variety of names have been proposed for them. One goal of this paper is to suggest a terminology that is both uniform and informative to replace the current rather chaotic nomenclature. Another goal is to investigate the properties and interrelations of these notions. Following brief expositions of indexed categories, twisted relations, and Kan extensions, we demonstrate and then exploit the duality between institution morphisms in the original sense of Goguen and Burstall, and the 'plain maps' of Meseguer, obtaining simple uniform proofs of completeness and cocompleteness for both resulting categories; because of this duality, we prefer the name 'comorphism' over 'plain map.' We next consider 'theoroidal' morphisms and comorphisims, which generalize signatures to theories, finding that the 'maps' of Meseguer are theoroidal comorphisms, while theoroidal morphisms are a new concept. We then introduce 'forward' and 'semi-natural' morphisms, and appendices discuss institutions for hidden algebra, universal algebra, partial equational logic, and a variant of order sorted algebra supporting partiality.

Goguen, Joseph↗

Robust Strategy for Rocket Engine Health Monitoring

Monitoring the health of rocket engine systems is essentially a two-phase process. The acquisition phase involves sensing physical conditions at selected locations, converting physical inputs to electrical signals, conditioning the signals as appropriate to establish scale or filter interference, and recording results in a form that is easy to interpret. The inference phase involves analysis of results from the acquisition phase, comparison of analysis results to established health measures, and assessment of health indications. A variety of analytical tools may be employed in the inference phase of health monitoring. These tools can be separated into three broad categories: statistical, rule based, and model based. Statistical methods can provide excellent comparative measures of engine operating health. They require well-characterized data from an ensemble of "typical" engines, or "golden" data from a specific test assumed to define the operating norm in order to establish reliable comparative measures. Statistical methods are generally suitable for real-time health monitoring because they do not deal with the physical complexities of engine operation. The utility of statistical methods in rocket engine health monitoring is hindered by practical limits on the quantity and quality of available data. This is due to the difficulty and high cost of data acquisition, the limited number of available test engines, and the problem of simulating flight conditions in ground test facilities. In addition, statistical methods incur a penalty for disregarding flow complexity and are therefore limited in their ability to define performance shift causality. Rule based methods infer the health state of the engine system based on comparison of individual measurements or combinations of measurements with defined health norms or rules. This does not mean that rule based methods are necessarily simple. Although binary yes-no health assessment can sometimes be established by relatively simple rules, the causality assignment needed for refined health monitoring often requires an exceptionally complex rule base involving complicated logical maps. Structuring the rule system to be clear and unambiguous can be difficult, and the expert input required to maintain a large logic network and associated rule base can be prohibitive.

Santi, L. Michael↗

Automata-Based Verification of Temporal Properties on Running Programs

This paper presents an approach to checking a running program against its Linear Temporal Logic (LTL) specifications. LTL is a widely used logic for expressing properties of programs viewed as sets of executions. Our approach consists of translating LTL formulae to finite-state automata, which are used as observers of the program behavior. The translation algorithm we propose modifies standard LTL to Buchi automata conversion techniques to generate automata that check finite program traces. The algorithm has been implemented in a tool, which has been integrated with the generic JPaX framework for runtime analysis of Java programs.

Giannakopoulou, Dimitra↗

Monitoring Programs Using Rewriting

We present a rewriting algorithm for efficiently testing future time Linear Temporal Logic (LTL) formulae on finite execution traces, The standard models of LTL are infinite traces, reflecting the behavior of reactive and concurrent systems which conceptually may be continuously alive in most past applications of LTL, theorem provers and model checkers have been used to formally prove that down-scaled models satisfy such LTL specifications. Our goal is instead to use LTL for up-scaled testing of real software applications, corresponding to analyzing the conformance of finite traces against LTL formulae. We first describe what it means for a finite trace to satisfy an LTL property end then suggest an optimized algorithm based on transforming LTL formulae. We use the Maude rewriting logic, which turns out to be a good notation and being supported by an efficient rewriting engine for performing these experiments. The work constitutes part of the Java PathExplorer (JPAX) project, the purpose of which is to develop a flexible tool for monitoring Java program executions.

Havelund, Klaus↗

Development of a Launch Vehicle Manufacturing Process

One of the goals of this chapter is to provide sufficient information so that you can develop a manufacturing process for a potential launch vehicle. With the variety of manufacturing options available, you might ask how this can possibly be done in the span of a single chapter. Actually, it will be quite simple because a basic manufacturing process is nothing more than a set of logical steps that are iterated until they produce a desired product. Although these statements seem simple and logical, don't let this simplicity fool you. Manufacturing problems with launch vehicles and their subassemblies have been the primary cause of project failures because the vehicle concept delivered to the manufacturing floor could not be built as designed.

Vickers, John↗

Free Flight and Self-Separation from the Flight Deck Perspective

The concept of "free flight", while still being developed, is intended to emphasize more, flexibility for operators in the National Airspace System (NAS) by providing more separation responsibility to pilots, New technologies, procedures, and concepts have been suggested by the aviation community to enable this task; however, much work needs to be accomplished to help define and evaluate the concept feasibility. The purpose of this simulation was to begin examining some of the communication and procedural issues associated with self-separation in the enroute environment. A simulation demonstration was conducted in the Boeing 747-400 simulator at NASA Ames Research Center. Commercial pilots (from a U.S. domestic carrier) current on the B747-400 aircraft were the participants. Ten flight crews (10 captains, 10 first officers) flew in the Denver enroute airspace environment. A new alerting logic designed to allow for airborne self-separation was created for this demonstration. This logic assumes automatic dependent surveillance broadcast (ADS-B) capability and represented aircraft up to 120 nautical miles on the display. The new flight deck display features were designed and incorporated on the existing navigational display in the simulator to allow for increased traffic and maneuvering information to the flight crew. New tools were also provided to allow the crews to assess conflicts and potential maneuvers before implementing them. Each of the flight crews flew eight different scenarios in the Denver enroute airspace. The scenarios included eight to ten other aircraft, and each scenario was created with the intent of having one of the other aircraft become an operational conflict for our simulator aircraft. Different types of conflict geometries were represented across the eight scenarios. Also, some scenarios allowed for more time to detect a potential clearance, while others allowed for less time for'detection. Additionally, the crews were asked to a ply the Visual Flight Rules (VFR) right of way rules when determining who should maneuver in a conflict situation; therefore, the scenarios were designed to test different applications of those recommendations, Data analyses include an evaluation of crew procedures and communication. The application of the VFR right-of-way rules are being explored. Timing variables are being examined to determine potential efficiency differences between scenarios and conflict types. Proximity of aircraft will be assessed as one indication of the operational safety. The intent of these evaluations is to help provide definitions and guidelines of negotiation procedures in a self-separation environment assuming automated data link technology (ADS-B). Also, definitions of likely flight crew maneuvers and application to current VFR right-of-way rules may be obtained, along with guidelines for negotiation procedures between flight crews.

Lozito, Sandra↗

Certifying Domain-Specific Policies

Proof-checking code for compliance to safety policies potentially enables a product-oriented approach to certain aspects of software certification. To date, previous research has focused on generic, low-level programming-language properties such as memory type safety. In this paper we consider proof-checking higher-level domain -specific properties for compliance to safety policies. The paper first describes a framework related to abstract interpretation in which compliance to a class of certification policies can be efficiently calculated Membership equational logic is shown to provide a rich logic for carrying out such calculations, including partiality, for certification. The architecture for a domain-specific certifier is described, followed by an implemented case study. The case study considers consistency of abstract variable attributes in code that performs geometric calculations in Aerospace systems.

Lowry, Michael↗

A Rewriting-Based Approach to Trace Analysis

We present a rewriting-based algorithm for efficiently evaluating future time Linear Temporal Logic (LTL) formulae on finite execution traces online. While the standard models of LTL are infinite traces, finite traces appear naturally when testing and/or monitoring red applications that only run for limited time periods. The presented algorithm is implemented in the Maude executable specification language and essentially consists of a set of equations establishing an executable semantics of LTL using a simple formula transforming approach. The algorithm is further improved to build automata on-the-fly from formulae, using memoization. The result is a very efficient and small Maude program that can be used to monitor program executions. We furthermore present an alternative algorithm for synthesizing probably minimal observer finite state machines (or automata) from LTL formulae, which can be used to analyze execution traces without the need for a rewriting system, and can hence be used by observers written in conventional programming languages. The presented work is part of an ambitious runtime verification and monitoring project at NASA Ames, called PATHEXPLORER, and demonstrates that rewriting can be a tractable and attractive means for experimenting and implementing program monitoring logics.

Havelund, Klaus↗

Tracking and Control of Gas Turbine Engine Component Damage/Life

This paper describes damage mechanisms and the methods of controlling damages to extend the on-wing life of critical gas turbine engine components. Particularly, two types of damage mechanisms are discussed: creep/rupture and thermo-mechanical fatigue. To control these damages and extend the life of engine hot-section components, we have investigated two methodologies to be implemented as additional control logic for the on-board electronic control unit. This new logic, the life-extending control (LEC), interacts with the engine control and monitoring unit and modifies the fuel flow to reduce component damages in a flight mission. The LEC methodologies were demonstrated in a real-time, hardware-in-the-loop simulation. The results show that LEC is not only a new paradigm for engine control design, but also a promising technology for extending the service life of engine components, hence reducing the life cycle cost of the engine.

Jaw, Link C.↗

Application of Artificial Intelligence Techniques in Unmanned Aerial Vehicle Flight

This paper describes the development of an application of Artificial Intelligence for Unmanned Aerial Vehicle (UAV) control. The project was done as part of the requirements for a class in Artificial Intelligence (AI) at Nova southeastern University and as an adjunct to a project at NASA Goddard Space Flight Center's Wallops Flight Facility for a resilient, robust, and intelligent UAV flight control system. A method is outlined which allows a base level application for applying an AI method, Fuzzy Logic, to aspects of Control Logic for UAV flight. One element of UAV flight, automated altitude hold, has been implemented and preliminary results displayed. A low cost approach was taken using freeware, gnu, software, and demo programs. The focus of this research has been to outline some of the AI techniques used for UAV flight control and discuss some of the tools used to apply AI techniques. The intent is to succeed with the implementation of applying AI techniques to actually control different aspects of the flight of an UAV.

Bauer, Frank H.↗

Flight Guidance System Requirements Specification

This report describes a requirements specification written in the RSML-e language for the mode logic of a Flight Guidance System of a typical regional jet aircraft. This model was created as one of the first steps in a five-year project sponsored by the NASA Langley Research Center, Rockwell Collins Inc., and the Critical Systems Research Group of the University of Minnesota to develop new methods and tools to improve the safety of avionics designs. This model will be used to demonstrate the application of a variety of methods and techniques, including safety analysis of system and subsystem requirements, verification of key properties using theorem provers and model checkers, identification of potential sources mode confusion in system designs, partitioning of applications based on the criticality of system hazards, and autogeneration of avionics quality code. While this model is representative of the mode logic of a typical regional jet aircraft, it does not describe an actual or planned product. Several aspects of a full Flight Guidance System, such as recovery from failed sensors, have been omitted, and no claims are made regarding the accuracy or completeness of this specification.

Miller, Steven P.↗

Questions Revisited: A Close Examination of Calculus of Inference and Inquiry

In this paper I examine more closely the way in which probability theory, the calculus of inference, is derived from the Boolean lattice structure of logical assertions ordered by implication. I demonstrate how the duality between the logical conjunction and disjunction in Boolean algebra is lost when deriving the probability calculus. In addition, I look more closely at the other lattice identities to verify that they are satisfied by the probability calculus. Last, I look towards developing the calculus of inquiry demonstrating that there is a sum and product rule for the relevance measure as well as a Bayes theorem. Current difficulties in deriving the complete inquiry calculus will also be discussed.

Knuth, Kevin H.↗

Deriving Laws from Ordering Relations

It took much effort in the early days of non-Euclidean geometry to break away from the mindset that all spaces are flat and that two distinct parallel lines do not cross. Up to that point, all that was known was Euclidean geometry, and it was difficult to imagine anything else. We have suffered a similar handicap brought on by the enormous relevance of Boolean algebra to the problems of our age-logic and set theory. Previously, I demonstrated that the algebra of questions is not Boolean, but rather is described by the free distributive algebra. To get to this stage took much effort, as many obstacles-most self-placed-had to be overcome. As Boolean algebras were all I had ever known, it was almost impossible for me to imagine working with an algebra where elements do not have complements. With this realization, it became very clear that the sum and product rules of probability theory at the most basic level had absolutely nothing to do with the Boolean algebra of logical statements. Instead, a measure of degree of inclusion can be invented for many different partially ordered sets, and the sum and product rules fall out of the associativity and distributivity of the algebra. To reinforce this very important idea, this paper will go over how these constructions are made, while focusing on the underlying assumptions. I will derive the sum and product rules for a distributive lattice in general and demonstrate how this leads to probability theory on the Boolean lattice and is related to the calculus of quantum mechanical amplitudes on the partially ordered set of experimental setups. I will also discuss the rules that can be derived from modular lattices and their relevance to the cross-ratio of projective geometry.

Knuth, Kevin H.↗

Discrete Abstractions of Hybrid Systems: Verification of Safety and Application to User-Interface Design

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.

Meeko Oishi↗