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.

SourceResearch connectionFrom yearThrough year

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 919 records · Page 51

All sources NASA NTRS DOE OSTI

NASA NTRS1987

Further Discussion: Parametric Study of Wind Generated Supermicron Particle Effects in Large Fires

In their reply (Porch et al., 1987) to our comments (Turco et al., 1987) on their smoke-scavenging-by-dust paper, Porch et al. attempt to justify a number of parameter assumptions in their original article, again revealing the extreme nature of those assumptions, particularly in the situation where all are taken simultaneously. In critiquing Porch et al.'s calculations, have not applied "opinion", but rather physical reality and common sense expressed through basic experimental results and logical physical bounds. A few examples of the unrealistic conditions required by the Porch et al. scavenging scheme, as described in their paper and comments, should suffice here. ) Porch et al. have fabricated a "fetch" region for dust particles in large fire plumes that logically must extend over an area up to 50 times greater than the fire area itself. Alternatively, they have invoked significant "necking down' of the fire plume, so that its cross-sectional area is at most a few percent of the fire area. Such severe constriction is seen only in very small fires with strong, organized vorticity, and then only over a limited plume rise region. No "fetch" has ever been noted in any large-scale fires we have observed, or for which accounts are available. Indeed, as we deduced in our original comments, complete dust scavenging even within the fire zone would probably occur less than 10% of the time for large urban fires.

Toon, O. B.↗

NASA NTRS2000

The Life Cycle Application of Intelligent Software Modeling for the First Materials Science Research Rack

Marshall Space Flight Center (MSFC) has been funding development of intelligent software models to benefit payload ground operations for nearly a decade. Experience gained from simulator development and real-time monitoring and control is being applied to engineering design, testing, and operation of the First Material Science Research Rack (MSRR-1). MSRR-1 is the first rack in a suite of three racks comprising the Materials Science Research Facility (MSRF) which will operate on the International Space Station (ISS). The MSRF will accommodate advanced microgravity investigations in areas such as the fields of solidification of metals and alloys, thermo-physical properties of polymers, crystal growth studies of semiconductor materials, and research in ceramics and glasses. The MSRR-1 is a joint venture between NASA and the European Space Agency (ESA) to study the behavior of different materials during high temperature processing in a low gravity environment. The planned MSRR-1 mission duration is five (5) years on-orbit and the total design life is ten (IO) years. The MSRR-1 launch is scheduled on the third Utilization Flight (UF-3) to ISS, currently in February of 2003). The objective of MSRR-1 is to provide an early capability on the ISS to conduct material science, materials technology, and space product research investigations in microgravity. It will provide a modular, multi-user facility for microgravity research in materials crystal growth and solidification. An intelligent software model of MSRR-1 is under development and will serve multiple purposes to support the engineering analysis, testing, training, and operational phases of the MSRR-1 life cycle development. The G2 real-time expert system software environment developed by Gensym Corporation was selected as the intelligent system shell for this development work based on past experience gained and the effectiveness of the programming environment. Our approach of multi- uses of the simulation model and its intuitive graphics capabilities is providing a concurrent engineering environment for rapid prototyping and development. Operational schematics of the MSRR-1 electrical, thermal control, vacuum access, and gas supply systems, and furnace inserts are represented graphically in the environment. Logic to represent first order engineering calculations is coded into the knowledge base to simulate the operational behavior of the MSRR-1 systems. An example of engineering data provided includes electrical currents, voltages, operational power, temperatures, thermal fluid flow rates. pressures, and component status indications. These type of data are calculated and displayed at appropriate instrumentation points, and the schematics are animated to reflect the simulated operational status of the MSRR-1. The software control functions are also simulated to represent appropriate operational behavior based on automated control and response to commands received by the crew or ground controllers. The first benefit of this simulation environment is being realized in the high fidelity engineering analysis results from the electrical power system G2 model. Secondly, the MSRR-1 simulation model will be embedded with a hardware mock-up of the MSRR-1 to provide crew training on MSRR-1 integrated payload operations. G2 gateway code will output the simulated instrumentation values, termed as telemetry, in a flight-like data stream so that the crew has realistic and accurate simulated MSRR-1 data on the flight displays which will be designed for crew use. The simulation will also respond appropriately to crew or ground initiated commands, which will be part of normal facility operations. A third use of the G2 model is being planned; the MSRR-1 simulation will be integrated with additional software code as part of the test configuration of the primary onboard computer, or Master Controller, for MSRR-1. We will take advantage of the G2 capability to simulate the flight like data stream to test flight software responses and behavior. A fourth use of the G2 model will be to train the Ground Support Personnel that will monitor the MSRR-1 systems and payloads while they are operating aboard the ISS. The intuitive, schematic based environment will provide an excellent foundation for personnel to understand the integrated configuration and operation of the MSRR-1, and the anticipated telemetry feedback based on operational modes of the equipment. Expert monitoring features will be enhanced to provide a smart monitoring environment for the operators. These features include: (1) Animated, intuitive schematic-based displays which reflect telemetry values, (1) Real-time plotting of simulated or incoming sensor values, (3) High/Low exception monitoring for analog data, (4) Expected state monitoring for discrete data, (5) Data trending, (6) Automated malfunction procedure execution to diagnose problems, (7) Look ahead capability to planned MSRR-1 activities in the onboard timeline. And finally, the logic to calculate telemetry values will be deactivated, and the same environment will interface to the incoming data for the real-time telemetry stream to schematically represent the onboard hardware configuration. G2 will be the foundation for the real-time monitoring and control environment. In summary, our MSRR-1 simulation model spans many elements of the life cycle development of this project: Engineering Analysis, Test and Checkout, Training of Crew and Ground Personnel, and Real-time monitoring and control. By utilizing the unique features afforded by an expert system development environment, we have been able to synergize a powerful tool capable of addressing our project needs at every phase of project development.

Rice, Amanda↗

NASA NTRS1998

A System for Managing Replenishment of a Nutrient Solution Using an Electrical Conductivity Controller

Control of nutrient solution parameters is very important for the growth and development of plants grown hydroponically. Protocols involving different nutrient solution replenishment times (e.g. one-week, two-week, or two-day replenishment) provide manual periodic control of the nutrient solution's electrical conductivity (EC). Since plants take-up nutrients as they grow, manual control has a drawback in that EC is not held constant between replenishments. In an effort to correct this problem the Center for Food and Environmental Systems for Human Exploration of Space at Tuskegee University has developed a system for managing and controlling levels of EC over a plant's entire growing cycle. A prototype system is being tested on sweetpotato production using the nutrient film technique (NFT), and it is being compared to a system in which sweetpotatoes are grown using NFT with manual control. NASA has played an important role in the development of environmental control systems. They have become a forerunner in growing plants hydroponically with some control systems through the use of networked data acquisition and control using environmental growth chambers. Data acquisition systems which involve the use of real-time, calibration, set points, user panel, and graphical representation programming provide a good method of controlling nutrient solution parameters such as EC and pH [Bledsoe, 19931]. In NASA's Biomass Production Chamber (BPC) at Kennedy Space Center, control is provided by a programmable logic controller (PLC). This is an industrial controller which combines ladder computer logic which has the ability to handle various levels of electrical power. The controller controls temperature, light and other parameters that affect the plant's environment, in the BPC, the Nutrient Delivery System (NIX), a sub-system of the PLC, controls nutrient solution parameters such as EC, pH, and solution levels. When the nutrient EC measurement goes outside a preset range (120-130 mS/m) a set amount of a stock solution of nutrients is automatically added by a metering pump to bring the EC back into operating range [Fortson, 1992]. This paper describes a system developed at Tuskegee University for controlling the EC of a nutrient solution used for growing sweetpotatoes with an EC controller and a computer with LabView data acquisition and instrumentation software. It also describes the preliminary data obtained from the growth of sweetpotatoes using this prototype control system.

Davis, D.↗

NASA NTRS1998

Fuzzy Control of Flexible-Link Manipulators: A Review

Several recent research efforts are reviewed here which have applied fuzzy logic in control of flexible-link manipulators. A flexible robot is a distributed parameter system represented by complex nonlinear dynamics, its actuator and the control parameters are non-colocated, and lastly, unstructured/unknown parameters play a significant role in model dynamics of a flexible robot operating in the real world. As a result, control of flexible robots is considered a promising area for application of intelligent control methodologies such as fuzzy logic, genetic algorithms, and neural networks.

Akbarzadeh-T, M.-R.↗

NASA NTRS1998

ELIPS: Toward a Sensor Fusion Processor on a Chip

The paper presents the concept and initial tests from the hardware implementation of a low-power, high-speed reconfigurable sensor fusion processor. The Extended Logic Intelligent Processing System (ELIPS) processor is developed to seamlessly combine rule-based systems, fuzzy logic, and neural networks to achieve parallel fusion of sensor in compact low power VLSI. The first demonstration of the ELIPS concept targets interceptor functionality; other applications, mainly in robotics and autonomous systems are considered for the future. The main assumption behind ELIPS is that fuzzy, rule-based and neural forms of computation can serve as the main primitives of an "intelligent" processor. Thus, in the same way classic processors are designed to optimize the hardware implementation of a set of fundamental operations, ELIPS is developed as an efficient implementation of computational intelligence primitives, and relies on a set of fuzzy set, fuzzy inference and neural modules, built in programmable analog hardware. The hardware programmability allows the processor to reconfigure into different machines, taking the most efficient hardware implementation during each phase of information processing. Following software demonstrations on several interceptor data, three important ELIPS building blocks (a fuzzy set preprocessor, a rule-based fuzzy system and a neural network) have been fabricated in analog VLSI hardware and demonstrated microsecond-processing times.

Daud, Taher↗

NASA NTRS2000

HTMT-class Latency Tolerant Parallel Architecture for Petaflops Scale Computation

Computational Aero Sciences and other numeric intensive computation disciplines demand computing throughputs substantially greater than the Teraflops scale systems only now becoming available. The related fields of fluids, structures, thermal, combustion, and dynamic controls are among the interdisciplinary areas that in combination with sufficient resolution and advanced adaptive techniques may force performance requirements towards Petaflops. This will be especially true for compute intensive models such as Navier-Stokes are or when such system models are only part of a larger design optimization computation involving many design points. Yet recent experience with conventional MPP configurations comprising commodity processing and memory components has shown that larger scale frequently results in higher programming difficulty and lower system efficiency. While important advances in system software and algorithms techniques have had some impact on efficiency and programmability for certain classes of problems, in general it is unlikely that software alone will resolve the challenges to higher scalability. As in the past, future generations of high-end computers may require a combination of hardware architecture and system software advances to enable efficient operation at a Petaflops level. The NASA led HTMT project has engaged the talents of a broad interdisciplinary team to develop a new strategy in high-end system architecture to deliver petaflops scale computing in the 2004/5 timeframe. The Hybrid-Technology, MultiThreaded parallel computer architecture incorporates several advanced technologies in combination with an innovative dynamic adaptive scheduling mechanism to provide unprecedented performance and efficiency within practical constraints of cost, complexity, and power consumption. The emerging superconductor Rapid Single Flux Quantum electronics can operate at 100 GHz (the record is 770 GHz) and one percent of the power required by convention semiconductor logic. Wave Division Multiplexing optical communications can approach a peak per fiber bandwidth of 1 Tbps and the new Data Vortex network topology employing this technology can connect tens of thousands of ports providing a bi-section bandwidth on the order of a Petabyte per second with latencies well below 100 nanoseconds, even under heavy loads. Processor-in-Memory (PIM) technology combines logic and memory on the same chip exposing the internal bandwidth of the memory row buffers at low latency. And holographic storage photorefractive storage technologies provide high-density memory with access a thousand times faster than conventional disk technologies. Together these technologies enable a new class of shared memory system architecture with a peak performance in the range of a Petaflops but size and power requirements comparable to today's largest Teraflops scale systems. To achieve high-sustained performance, HTMT combines an advanced multithreading processor architecture with a memory-driven coarse-grained latency management strategy called "percolation", yielding high efficiency while reducing the much of the parallel programming burden. This paper will present the basic system architecture characteristics made possible through this series of advanced technologies and then give a detailed description of the new percolation approach to runtime latency management.

Sterling, Thomas↗

NASA NTRS2000

Predictability of Gaseous Impact Ignition Sensitivity from Autoignition Temperature Data

An analysis of cumulative binomial probabilities for a quantal-type test like ASTM G74 indicates that for a probability of reaction in a single trial of 0.05, the probability of obtaining zero reactions in 20 trials is only approximately 36 percent, Because the lack of precision with the ASTM G74 test logic could be potentially misleading, an investigation was conducted to determine if pneumatic impact sensitivity could be predicted more reliably from other, more precise test methods. Pneumatic impact sensitivity tests were conducted following ASTM G74, but employing more rigorous test logics; autoignition temperature tests were conducted per ASTM G72. Polytetrafluoroethylene (PTFE), Viton A, polyethylene, polyoxymethylene polyamide, and silicone were the polymers used. After a fixed number of pneumatic impact tests was performed at set pressures, a plot of reaction frequency over a 3.4 to 24.1 MPa impact pressure range indicated that PTFE, Viton A, and silicone would outperform other polymers. The 50 percent pneumatic impact reactivity level was determined with the Bruceton test method. The data obtained resulted in a strong correlation between the 50 percent reactivity level and the autoignition temperature of polymers, indicating similar ignition mechanisms.

Hirsh, David↗

NASA NTRS2000

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↗

NASA NTRS2001

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↗

NASA NTRS2000

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↗

NASA NTRS2001

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.↗

NASA NTRS2001

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↗

NASA NTRS2001

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↗

NASA NTRS2001

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↗

NASA NTRS2001

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↗

NASA NTRS2002

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↗

NASA NTRS1997

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↗

NASA NTRS2001

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↗