Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “automated verification”

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 37 records · Page 2
All sourcesNASA NTRSDOE OSTI
NASA NTRS2007

AIRSAR Web-Based Data Processing

The AIRSAR automated, Web-based data processing and distribution system is an integrated, end-to-end synthetic aperture radar (SAR) processing system. Designed to function under limited resources and rigorous demands, AIRSAR eliminates operational errors and provides for paperless archiving. Also, it provides a yearly tune-up of the processor on flight missions, as well as quality assurance with new radar modes and anomalous data compensation. The software fully integrates a Web-based SAR data-user request subsystem, a data processing system to automatically generate co-registered multi-frequency images from both polarimetric and interferometric data collection modes in 80/40/20 MHz bandwidth, an automated verification quality assurance subsystem, and an automatic data distribution system for use in the remote-sensor community. Features include Survey Automation Processing in which the software can automatically generate a quick-look image from an entire 90-GB SAR raw data 32-MB/s tape overnight without operator intervention. Also, the software allows product ordering and distribution via a Web-based user request system. To make AIRSAR more user friendly, it has been designed to let users search by entering the desired mission flight line (Missions Searching), or to search for any mission flight line by entering the desired latitude and longitude (Map Searching). For precision image automation processing, the software generates the products according to each data processing request stored in the database via a Queue management system. Users are able to have automatic generation of coregistered multi-frequency images as the software generates polarimetric and/or interferometric SAR data processing in ground and/or slant projection according to user processing requests for one of the 12 radar modes.

Chu, Anhua↗
NASA NTRS1999

A Practical Approach to Implementing Real-Time Semantics

This paper investigates implementations of process algebras which are suitable for modeling concurrent real-time systems. It suggests an approach for efficiently implementing real-time semantics using dynamic priorities. For this purpose a proces algebra with dynamic priority is defined, whose semantics corresponds one-to-one to traditional real-time semantics. The advantage of the dynamic-priority approach is that it drastically reduces the state-space sizes of the systems in question while preserving all properties of their functional and real-time behavior. The utility of the technique is demonstrated by a case study which deals with the formal modeling and verification of the SCSI-2 bus-protocol. The case study is carried out in the Concurrency Workbench of North Carolina, an automated verification tool in which the process algebra with dynamic priority is implemented. It turns out that the state space of the bus-protocol model is about an order of magnitude smaller than the one resulting from real-time semantics. The accuracy of the model is proved by applying model checking for verifying several mandatory properties of the bus protocol.

Luettgen, Gerald↗
NASA NTRS2015

Verification of Functional Fault Models and the Use of Resource Efficient Verification Tools

Functional fault models (FFMs) are a directed graph representation of the failure effect propagation paths within a system's physical architecture and are used to support development and real-time diagnostics of complex systems. Verification of these models is required to confirm that the FFMs are correctly built and accurately represent the underlying physical system. However, a manual, comprehensive verification process applied to the FFMs was found to be error prone due to the intensive and customized process necessary to verify each individual component model and to require a burdensome level of resources. To address this problem, automated verification tools have been developed and utilized to mitigate these key pitfalls. This paper discusses the verification of the FFMs and presents the tools that were developed to make the verification process more efficient and effective.

reliability↗
NASA NTRS2009

Proceedings of the First NASA Formal Methods Symposium

Topics covered include: Model Checking - My 27-Year Quest to Overcome the State Explosion Problem; Applying Formal Methods to NASA Projects: Transition from Research to Practice; TLA+: Whence, Wherefore, and Whither; Formal Methods Applications in Air Transportation; Theorem Proving in Intel Hardware Design; Building a Formal Model of a Human-Interactive System: Insights into the Integration of Formal Methods and Human Factors Engineering; Model Checking for Autonomic Systems Specified with ASSL; A Game-Theoretic Approach to Branching Time Abstract-Check-Refine Process; Software Model Checking Without Source Code; Generalized Abstract Symbolic Summaries; A Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing; Component-Oriented Behavior Extraction for Autonomic System Design; Automated Verification of Design Patterns with LePUS3; A Module Language for Typing by Contracts; From Goal-Oriented Requirements to Event-B Specifications; Introduction of Virtualization Technology to Multi-Process Model Checking; Comparing Techniques for Certified Static Analysis; Towards a Framework for Generating Tests to Satisfy Complex Code Coverage in Java Pathfinder; jFuzz: A Concolic Whitebox Fuzzer for Java; Machine-Checkable Timed CSP; Stochastic Formal Correctness of Numerical Algorithms; Deductive Verification of Cryptographic Software; Coloured Petri Net Refinement Specification and Correctness Proof with Coq; Modeling Guidelines for Code Generation in the Railway Signaling Context; Tactical Synthesis Of Efficient Global Search Algorithms; Towards Co-Engineering Communicating Autonomous Cyber-Physical Systems; and Formal Methods for Automated Diagnosis of Autosub 6000.

Denney, Ewen↗
NASA NTRSDate not supplied

The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained

Capturing and analyzing requirements of Cyber-Physical Systems (CPS) can be challenging, since CPS models typically involve time-varying and real-valued variables, physical system dynamics, or even adaptive behavior. MATLAB/Simulinkis a development and simulation framework that is widely used in industry to capture such systems. In this paper, we report on the application of NASA Ames tools to perform end-to-end analysis of the Ten Lockheed Martin Challenge Problems (LMCPS). LMCPS is a set of industrial Simulink model benchmarks and natural language requirements developed by domain experts. Our framework, which integrates the tools FRET and COCOSIM, is used to: 1) elicit, explain, and formalize the semantics of the given natural language requirements; 2) generate verification code and monitors that can be automatically attached to the Simulink models; 3) perform verification by using SMT-based model checkers. FRET and COCOSIM are open source, and can be used by other researchers and practitioners to replicate our case study. We provide a categorization of recurring patterns in the formalization of the requirements and discuss the strengths and weaknesses of our automated verification approach.

Anastasia Mavridou↗
NASA NTRS2016

Challenges in High-Assurance Runtime Verification

Safety-critical systems are growing more complex and becoming increasingly autonomous. Runtime Verification (RV) has the potential to provide protections when a system cannot be assured by conventional means, but only if the RV itself can be trusted. In this paper, we proffer a number of challenges to realizing high-assurance RV and illustrate how we have addressed them in our research. We argue that high-assurance RV provides a rich target for automated verification tools in hope of fostering closer collaboration among the communities.

Goodloe, Alwyn E.↗
NASA NTRS1976

A methodology for producing reliable software, volume 1

An investigation into the areas having an impact on producing reliable software including automated verification tools, software modeling, testing techniques, structured programming, and management techniques is presented. This final report contains the results of this investigation, analysis of each technique, and the definition of a methodology for producing reliable software.

Stucki, L. G.↗
NASA NTRS1989

Initial Ada components evaluation

The SAIC has the responsibility for independent test and validation of the SSE. They have been using a mathematical functions library package implemented in Ada to test the SSE IV and V process. The library package consists of elementary mathematical functions and is both machine and accuracy independent. The SSE Ada components evaluation includes code complexity metrics based on Halstead's software science metrics and McCabe's measure of cyclomatic complexity. Halstead's metrics are based on the number of operators and operands on a logical unit of code and are compiled from the number of distinct operators, distinct operands, and total number of occurrences of operators and operands. These metrics give an indication of the physical size of a program in terms of operators and operands and are used diagnostically to point to potential problems. McCabe's Cyclomatic Complexity Metrics (CCM) are compiled from flow charts transformed to equivalent directed graphs. The CCM is a measure of the total number of linearly independent paths through the code's control structure. These metrics were computed for the Ada mathematical functions library using Software Automated Verification and Validation (SAVVAS), the SSE IV and V tool. A table with selected results was shown, indicating that most of these routines are of good quality. Thresholds for the Halstead measures indicate poor quality if the length metric exceeds 260 or difficulty is greater than 190. The McCabe CCM indicated a high quality of software products.

Moebes, Travis↗
NASA NTRS1995

The specification-based validation of reliable multicast protocol: Problem Report

Reliable Multicast Protocol (RMP) is a communication protocol that provides an atomic, totally ordered, reliable multicast service on top of unreliable IP multicasting. In this report, we develop formal models for RMP using existing automated verification systems, and perform validation on the formal RMP specifications. The validation analysis help identifies some minor specification and design problems. We also use the formal models of RMP to generate a test suite for conformance testing of the implementation. Throughout the process of RMP development, we follow an iterative, interactive approach that emphasizes concurrent and parallel progress of implementation and verification processes. Through this approach, we incorporate formal techniques into our development process, promote a common understanding for the protocol, increase the reliability of our software, and maintain high fidelity between the specifications of RMP and its implementation.

Wu, Yunqing↗
NASA NTRS1995

The Specification-Based Validation of Reliable Multicast Protocol

Reliable Multicast Protocol (RMP) is a communication protocol that provides an atomic, totally ordered, reliable multicast service on top of unreliable IP multicasting. In this report, we develop formal models for RMP using existing automated verification systems, and perform validation on the formal RMP specifications. The validation analysis help identifies some minor specification and design problems. We also use the formal models of RMP to generate a test suite for conformance testing of the implementation. Throughout the process of RMP development, we follow an iterative, interactive approach that emphasizes concurrent and parallel progress of the implementation and verification processes. Through this approach, we incorporate formal techniques into our development process, promote a common understanding for the protocol, increase the reliability of our software, and maintain high fidelity between the specifications of RMP and its implementation.

Wu, Yunqing↗
NASA NTRS2009

Software Model Checking Without Source Code

We present a framework, called AIR, for verifying safety properties of assembly language programs via software model checking. AIR extends the applicability of predicate abstraction and counterexample guided abstraction refinement to the automated verification of low-level software. By working at the assembly level, AIR allows verification of programs for which source code is unavailable-such as legacy and COTS software-and programs that use features-such as pointers, structures, and object-orientation-that are problematic for source-level software verification tools. In addition, AIR makes no assumptions about the underlying compiler technology. We have implemented a prototype of AIR and present encouraging results on several non-trivial examples.

Chaki, Sagar↗
NASA NTRS2011

NASA Tech Briefs, July 2011

Topics covered include: 1) Collaborative Clustering for Sensor Networks; 2) Teleoperated Marsupial Mobile Sensor Platform Pair for Telepresence Insertion Into Challenging Structures; 3) Automated Verification of Spatial Resolution in Remotely Sensed Imagery; 4) Electrical Connector Mechanical Seating Sensor; 5) In Situ Aerosol Detector; 6) Multi-Parameter Aerosol Scattering Sensor; 7) MOSFET Switching Circuit Protects Shape Memory Alloy Actuators; 8) Optimized FPGA Implementation of Multi-Rate FIR Filters Through Thread Decomposition; 9) Circuit for Communication Over Power Lines; 10) High-Efficiency Ka-Band Waveguide Two-Way Asymmetric Power Combiner; 11) 10-100 Gbps Offload NIC for WAN, NLR, and Grid Computing; 12) Pulsed Laser System to Simulate Effects of Cosmic Rays in Semiconductor Devices; 13) Flight Planning in the Cloud; 14) MPS Editor; 15) Object-Oriented Multi Disciplinary Design, Analysis, and Optimization Tool; 16) Cryogenic-Compatible Winchester Connector Mount and Retaining System for Composite Tubes; 17) Development of Position-Sensitive Magnetic Calorimeters for X-Ray Astronomy; 18) Planar Rotary Piezoelectric Motor Using Ultrasonic Horns; 19) Self-Rupturing Hermetic Valve; 20) Explosive Bolt Dual-Initiated from One Side; 21) Dampers for Stationary Labyrinth Seals; 22) Two-Arm Flexible Thermal Strap; 23) Carbon Dioxide Removal via Passive Thermal Approaches; 24) Polymer Electrolyte-Based Ambient Temperature Oxygen Microsensors for Environmental Monitoring; 25) Pressure Shell Approach to Integrated Environmental Protection; 26) Image Quality Indicator for Infrared Inspections; 27) Micro-Slit Collimators for X-Ray/Gamma-Ray Imaging; 28) Scatterometer-Calibrated Stability Verification Method; 29) Test Port for Fiber-Optic-Coupled Laser Altimeter; 30) Phase Retrieval System for Assessing Diamond Turning and Optical Surface Defects; 31) Laser Oscillator Incorporating a Wedged Polarization Rotator and a Porro Prism as Cavity Mirror; 32) Generic, Extensible, Configurable Push-Pull Framework for Large-Scale Science Missions; 33) Dynamic Loads Generation for Multi-Point Vibration Excitation Problems; 34) Optimal Control via Self-Generated Stochasticity; 35) Space-Time Localization of Plasma Turbulence Using Multiple Spacecraft Radio Links; 36) Surface Contact Model for Comets and Asteroids; 37) Dust Mitigation Vehicle; 38) Optical Coating Performance for Heat Reflectors of the JWST-ISIM Electronic Component; 39) SpaceCube Demonstration Platform; 40) Aperture Mask for Unambiguous Parity Determination in Long Wavelength Imagers; 41) Spaceflight Ka-Band High-Rate Radiation-Hard Modulator; 42) Enabling Disabled Persons to Gain Access to Digital Media; 43) Cytometer on a Chip; 44) Principles, Techniques, and Applications of Tissue Microfluidics; and 45) Two-Stage Winch for Kites and Tethered Balloons or Blimps.

Source record↗
NASA NTRS2002

Formal verification of human-automation interaction

This paper discusses a formal and rigorous approach to the analysis of operator interaction with machines. It addresses the acute problem of detecting design errors in human-machine interaction and focuses on verifying the correctness of the interaction in complex and automated control systems. The paper describes a systematic methodology for evaluating whether the interface provides the necessary information about the machine to enable the operator to perform a specified task successfully and unambiguously. It also addresses the adequacy of information provided to the user via training material (e.g., user manual) about the machine's behavior. The essentials of the methodology, which can be automated and applied to the verification of large systems, are illustrated by several examples and through a case study of pilot interaction with an autopilot aboard a modern commercial aircraft. The expected application of this methodology is an augmentation and enhancement, by formal verification, of human-automation interfaces.

Aviation↗
NASA NTRS1993

Development and verification testing of automation and robotics for assembly of space structures

A program was initiated within the past several years to develop operational procedures for automated assembly of truss structures suitable for large-aperture antennas. The assembly operations require the use of a robotic manipulator and are based on the principle of supervised autonomy to minimize crew resources. A hardware testbed was established to support development and evaluation testing. A brute-force automation approach was used to develop the baseline assembly hardware and software techniques. As the system matured and an operation was proven, upgrades were incorprated and assessed against the baseline test results. This paper summarizes the developmental phases of the program, the results of several assembly tests, the current status, and a series of proposed developments for additional hardware and software control capability. No problems that would preclude automated in-space assembly of truss structures have been encountered. The current system was developed at a breadboard level and continued development at an enhanced level is warranted.

Rhodes, Marvin D.↗
NASA NTRS1995

Verification Test of Automated Robotic Assembly of Space Truss Structures

A multidisciplinary program has been conducted at the Langley Research Center to develop operational procedures for supervised autonomous assembly of truss structures suitable for large-aperture antennas. The hardware and operations required to assemble a 102-member tetrahedral truss and attach 12 hexagonal panels were developed and evaluated. A brute-force automation approach was used to develop baseline assembly hardware and software techniques. However, as the system matured and operations were proven, upgrades were incorporated and assessed against the baseline test results. These upgrades included the use of distributed microprocessors to control dedicated end-effector operations, machine vision guidance for strut installation, and the use of an expert system-based executive-control program. This paper summarizes the developmental phases of the program, the results of several assembly tests, and a series of proposed enhancements. No problems that would preclude automated in-space assembly or truss structures have been encountered. The test system was developed at a breadboard level and continued development at an enhanced level is warranted.

Rhodes, Marvin D.↗
NASA NTRS2020

Design for Manufacturing Tool for Automated Fiber Placement Structures - Verification and Validation

A tool has been developed to address the growing Design for Manufacturing needs for composite structures, specifically those manufactured with automated fiber placement. This manufacturing approach presents unique challenges associated with puckers and wrinkling, tow overlaps and gaps, fiber deviation, and laminate strength. Achieving a satisfactory laminate design usually requires finding compromises between those four areas. The developed tool, dubbed the Central Optimizer, assists with the process of balancing competing design metrics in automated fiber placement. This tool was developed under the NASA Advanced Composites Consortium with input from industry partners. Under this program, the Central Optimizer has been exercised on three different structures to verify its functionality and validate ability to improve the design process for automated fiber placement structures.

August T Noevere↗
NASA NTRS1980

Evaluation of verification and testing tools for FORTRAN programs

Two automated software verification and testing systems were developed for use in the analysis of computer programs. An evaluation of the static analyzer DAVE and the dynamic analyzer PET, which are used in the analysis of FORTRAN programs on Control Data (CDC) computers, are described. Both systems were found to be effective and complementary, and are recommended for use in testing FORTRAN programs.

Smith, K. A.↗
NASA NTRS1987

Digital-flight-control-system software written in automated-engineering-design language: A user's guide of verification and validation tools

The user guide of verification and validation (V&V) tools for the Automated Engineering Design (AED) language is specifically written to update the information found in several documents pertaining to the automated verification of flight software tools. The intent is to provide, in one document, all the information necessary to adequately prepare a run to use the AED V&V tools. No attempt is made to discuss the FORTRAN V&V tools since they were not updated and are not currently active. Additionally, the current descriptions of the AED V&V tools are contained and provides information to augment the NASA TM 84276. The AED V&V tools are accessed from the digital flight control systems verification laboratory (DFCSVL) via a PDP-11/60 digital computer. The AED V&V tool interface handlers on the PDP-11/60 generate a Univac run stream which is transmitted to the Univac via a Remote Job Entry (RJE) link. Job execution takes place on the Univac 1100 and the job output is transmitted back to the DFCSVL and stored as a PDP-11/60 printfile.

Saito, Jim↗