Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “formal 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 451 records · Page 25

Understanding and Verifying Neural Networks

Deep Neural Networks (DNNs) have gained immense popularity in recent times and have widespread use in applications such as image classification, sentiment analysis, speech recognition and also in safety-critical applications such as autonomous driving. However, they suffer limitations such as lack of explainability and robustness which raise safety and security concerns in their usage. Further, the complex structure and large input spaces of DNNs act as an impediment to thorough verification and testing. The SafeDNN project at the Robust Software Engineering (RSE) group at NASA aims at exploring techniques to ensure that systems that use deep neural networks are safe, robust and interpretable. In this talk, I will be presenting our technique Prophecy that automatically infers formal properties of deep neural network models. The tool extracts patterns based on neuron activations as preconditions that imply certain desirable output properties of the model. I would be highlighting case studies that use Prophecy in obtaining explanations for network decisions, understanding correct and incorrect behavior, providing formal guarantees wrt safety and robustness, and debugging neural network models. We have applied the tool on image classification networks, neural network controllers providing turn advisories in unmanned aircrafts, regression models used for autonomous center-line tracking in aircrafts and neural network object detectors

Deep Neural Networks↗

Secure System Composition and Type Checking using Cryptographic Proofs [Slides]

We can use formal methods to verify that systems compose correctly without the possibility of incorrect behavior. This means exhaustively checking that System A’s postconditions agree with System B’s preconditions. If so, it is safe to compose. Normal Setting: Every computational path must be accounted for and checked. Verification cost (time) is multiplicative across systems.

97 MATHEMATICS AND COMPUTING↗

Formal Methods for Automated Diagnosis of Autosub 6000

This is a progress report on applying formal methods in the context of building an automated diagnosis and recovery system for Autosub 6000, an Autonomous Underwater Vehicle (AUV). The diagnosis task involves building abstract models of the control system of the AUV. The diagnosis engine is based on Livingstone 2, a model-based diagnoser originally built for aerospace applications. Large parts of the diagnosis model can be built without concrete knowledge about each mission, but actual mission scripts and configuration parameters that carry important information for diagnosis are changed for every mission. Thus we use formal methods for generating the mission control part of the diagnosis model automatically from the mission script and perform a number of invariant checks to validate the configuration. After the diagnosis model is augmented with the generated mission control component model, it needs to be validated using verification techniques.

Ernits, Juhan↗

Large project experiences with object-oriented methods and reuse

The SSVTF (Space Station Verification and Training Facility) project is completing the Preliminary Design Review of a large software development using object-oriented methods and systematic reuse. An incremental developmental lifecycle was tailored to provide early feedback and guidance on methods and products, with repeated attention to reuse. Object oriented methods were formally taught and supported by realistic examples. Reuse was readily accepted and planned by the developers. Schedule and budget issues were handled by agreements and work sharing arranged by the developers.

Wessale, William↗

A Mathematical Analysis of Conflict Prevention Information

In air traffic management, conflict prevention information refers to the guidance maneuvers, which if taken, ensure that an aircraft's path is conflict-free. These guidance maneuvers take the form of changes to track angle or ground speed. Conflict prevention information may be assembled into prevention bands that advise the crew on maneuvers that should not be taken. Unlike conflict resolution systems, which presume that the aircraft already has a conflict, conflict prevention systems show conflicts for any maneuver, giving the pilot confidence that if a maneuver is made, then no near-term conflicts will result. Because near-term conflicts can lead to safety concerns, strong verification of information correctness is required. This paper presents a mathematical framework to analyze the correctness of algorithms that produce conflict prevention information incorporating an arbitrary number of traffic aircraft and with both a near-term and intermediate-term lookahead times. The framework is illustrated with a formally verified algorithm for 2-dimensional track angle prevention bands.

Maddalon, Jeffrey M.↗

NASA's Space Launch System: Systems Engineering Approach for Affordability and Mission Success

NASA is working toward the first launch of the Space Launch System, a new, unmatched capability for deep space exploration with launch readiness planned for 2019. Since program start in 2011, SLS has passed several major formal design milestones, and every major element of the vehicle has produced test and flight hardware. The SLS approach to systems engineering has been key to the program's success. Key aspects of the SLS SE&I approach include: 1) minimizing the number of requirements, 2) elimination of explicit verification requirements, 3) use of certified models of subsystem capability in lieu of requirements when appropriate and 4) certification of capability beyond minimum required capability.

Hutt, John J.↗

Establishing the Assurance Efficacy of Automated Risk Mitigation Strategies

Verification and validation of increasingly autonomous aviation systems is a major challenge. Traditional techniques for the assurance of high-confidence, safety-critical systems are not equipped to handle the complexity, uncertainty, and lack of predictability inherent in non-deterministic systems. Techniques such as run time monitoring, formal methods, and testing and simulation have been applied to some effect, but it is difficult to properly assess the success of such measures. The authors propose the concept of Assurance Efficacy to address this gap. Assurance Efficacy is seen as a parameter, criteria, or perspective by which to evaluate, identify and explore safety risk mitigation strategies and operational assurance architectures. Validation of the utility of this concept through flight testing is a first step in determining its potential role in assessing the overall safety of complex, increasingly autonomous systems that cannot be fully assured in the design phase.

system safety↗

NASA's M and S Accreditation Process Plan and Specification for Space Exploration

NASA's Exploration Systems Mission Directorate (ESMD) is implementing a management approach for modeling and simulation (M&S) that will provide decision-makers information on the model's fidelity, credibility, and quality. This information will allow the decision-maker to understand the risks involved in using a model's results in the decision-making process. This presentation will discuss NASA's overall approach to achieving formal accreditation of its models or simulations supporting space exploration. The development of a formal Accreditation Plan is a key component in the preliminary activities for modeling and simulation (M&S) assessment. This presentation will describe NASA's process for identifying risks associated with M&S use and the associated M&S assessments that will dictate the level of data certification and M&S verification and validation (V&V) activities required to support the decision-making process. The M&S Accreditation Plan and Report templates for ESMD will also be illustrated.

O'Neil, David↗

MBSE Validation and Verification: Case Study for LADEE

The Lunar Atmosphere Dust Environment Explorer (LADEE) mission orbited the moon in order to measure the density, composition, and time variability of the lunar dust environment. The successful mission launched September 7, 2013 and was de-orbited and impacted the moon's surface on April 17, 2014. The ground-side and onboard flight software for the mission was developed using a “Model-Based Software Engineering” (MBSE) methodology combined with strong reuse of Government and Commercial Off-The Shelf (G/COTS) components. Models of the spacecraft and flight software were developed in a graphical dynamics modeling package. Flight Software requirements were prototyped and refined using the simulated models. After the model was shown to work as desired in the simulation framework, C-code software was automatically generated from the models. The auto-generated software was then tested in real-time Processor-in-the-Loop and Hardware-in-the-Loop test beds. “Traveling Road Show” test beds were used for early integration tests with payloads and other subsystems. Traditional techniques for verifying computational sciences models were used to characterize the spacecraft simulation. A lightweight set of formal methods analysis, static analysis, formal inspection, and code coverage analyses were utilized to further reduce defects in the onboard flight software artifacts. These techniques were applied early and often in the development process, iteratively increasing the capabilities of software and fidelity of vehicle models and test beds.

Model-Based Software Engineering, Validation and V↗

An error covariance model for sea surface topography and velocity derived from TOPEX/POSEIDON altimetry

In order to facilitate the use of satellite-derived sea surface topography and velocity oceanographic models, methodology is presented for deriving the total error covariance and its geographic distribution from TOPEX/POSEIDON measurements. The model is formulated using a parametric model fit to the altimeter range observations. The topography and velocity modeled with spherical harmonic expansions whose coefficients are found through optimal adjustment to the altimeter range residuals using Bayesian statistics. All other parameters, including the orbit, geoid, surface models, and range corrections are provided as unadjusted parameters. The maximum likelihood estimates and errors are derived from the probability density function of the altimeter range residuals conditioned with a priori information. Estimates of model errors for the unadjusted parameters are obtained from the TOPEX/POSEIDON postlaunch verification results and the error covariances for the orbit and the geoid, except for the ocean tides. The error in the ocean tides is modeled, first, as the difference between two global tide models and, second, as the correction to the present tide model, the correction derived from the TOPEX/POSEIDON data. A formal error covariance propagation scheme is used to derive the total error. Our global total error estimate for the TOPEX/POSEIDON topography relative to the geoid for one 10-day period is found tio be 11 cm RMS. When the error in the geoid is removed, thereby providing an estimate of the time dependent error, the uncertainty in the topography is 3.5 cm root mean square (RMS). This level of accuracy is consistent with direct comparisons of TOPEX/POSEIDON altimeter heights with tide gauge measurements at 28 stations. In addition, the error correlation length scales are derived globally in both east-west and north-south directions, which should prove useful for data assimilation. The largest error correlation length scales are found in the tropics. Errors in the velocity field are smallest in midlatitude regions. For both variables the largest errors caused by uncertainty in the geoid. More accurate representations of the geoid await a dedicated geopotential satellite mission. Substantial improvements in the accuracy of ocean tide models are expected in the very near future from research with TOPEX/POSEIDON data.

Tsaoussi, Lucia S.↗

What Sensing Tells Us: Towards a Formal Theory of Testing for Dynamical Systems

Just as actions can have indirect effects on the state of the world, so too can sensing actions have indirect effects on an agent's state of knowledge. In this paper, we investigate "what sensing actions tell us", i.e., what an agent comes to know indirectly from the outcome of a sensing action, given knowledge of its actions and state constraints that hold in the world. To this end, we propose a formalization of the notion of testing within a dialect of the situation calculus that includes knowledge and sensing actions. Realizing this formalization requires addressing the ramification problem for sensing actions. We formalize simple tests as sensing actions. Complex tests are expressed in the logic programming language Golog. We examine what it means to perform a test, and how the outcome of a test affects an agent's state of knowledge. Finally, we propose automated reasoning techniques for test generation and complex-test verification, under certain restrictions. The work presented in this paper is relevant to a number of application domains including diagnostic problem solving, natural language understanding, plan recognition, and active vision.

McIlraith, Sheila↗

A Test Generation Framework for Distributed Fault-Tolerant Algorithms

Heavyweight formal methods such as theorem proving have been successfully applied to the analysis of safety critical fault-tolerant systems. Typically, the models and proofs performed during such analysis do not inform the testing process of actual implementations. We propose a framework for generating test vectors from specifications written in the Prototype Verification System (PVS). The methodology uses a translator to produce a Java prototype from a PVS specification. Symbolic (Java) PathFinder is then employed to generate a collection of test cases. A small example is employed to illustrate how the framework can be used in practice.

Goodloe, Alwyn↗

Fusing Quantitative Requirements Analysis with Model-based Systems Engineering

A vision is presented for fusing quantitative requirements analysis with model-based systems engineering. This vision draws upon and combines emergent themes in the engineering milieu. "Requirements engineering" provides means to explicitly represent requirements (both functional and non-functional) as constraints and preferences on acceptable solutions, and emphasizes early-lifecycle review, analysis and verification of design and development plans. "Design by shopping" emphasizes revealing the space of options available from which to choose (without presuming that all selection criteria have previously been elicited), and provides means to make understandable the range of choices and their ramifications. "Model-based engineering" emphasizes the goal of utilizing a formal representation of all aspects of system design, from development through operations, and provides powerful tool suites that support the practical application of these principles. A first step prototype towards this vision is described, embodying the key capabilities. Illustrations, implications, further challenges and opportunities are outlined.

optimization↗

What FM can offer DFCS design

The results of aircrafts and spacecrafts flight tests are reported. It is shown that the problems of Digital Flight Control Systems (DFCS) are the problems of systems whose complexity has exceeded the reach of the intellectual tools employed. It is also shown that intuition, experience, and techniques derived from mechanical and analog systems are insufficient for complex, integrated, digital systems. Formal Methods (FM) of computer science can offer DFCS systematic techniques for the construction of trustworthy software, including: techniques for the precise specification of requirements and the development of designs; systematic approaches to the design and structuring of distributed and concurrent systems; fault tolerance algorithms; and systematic methods of testing and analytic methods of verification.

Rushby, John↗

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts

The NASA DAIDALUS library provides formal definitions for Detect-and-Avoid avionics concepts such as when an aircraft is well-clear with respect to the surrounding air traffic, i.e., it does not operate in such proximity to create a collision hazard. While several properties are proven correct for DAIDALUS assuming ideal real number arithmetic, an actual implementation that uses floating-point numbers may behave unexpectedly because of round-off errors and run-time exceptions. This paper presents an experience report on the application of a formal methods toolchain to extract and verify floating-point C code from a real-valued specification of the well-clear module of DAIDALUS. This toolchain comprises the PVS theorem prover, the PRECiSA floating-point analyzer and code generator, and the Frama-C analysis suite. The generated code is automatically instrumented to detect when the control flow of the floating-point program may diverge from the ideal real number specification, and it is annotated with contracts that state the maximum accumulated round-off error. The absence of overflows is also formally verified for the generated code. In order to apply the toolchain to an industrial case study such as DAIDALUS, a formally verified pre-processing of the input specification is performed, which includes a program slicing and several semantic-preserving simplifications.

Program verification↗

Closing the Certification Gaps in Adaptive Flight Control Software

Over the last five decades, extensive research has been performed to design and develop adaptive control systems for aerospace systems and other applications where the capability to change controller behavior at different operating conditions is highly desirable. Although adaptive flight control has been partially implemented through the use of gain-scheduled control, truly adaptive control systems using learning algorithms and on-line system identification methods have not seen commercial deployment. The reason is that the certification process for adaptive flight control software for use in national air space has not yet been decided. The purpose of this paper is to examine the gaps between the state-of-the-art methodologies used to certify conventional (i.e., non-adaptive) flight control system software and what will likely to be needed to satisfy FAA airworthiness requirements. These gaps include the lack of a certification plan or process guide, the need to develop verification and validation tools and methodologies to analyze adaptive controller stability and convergence, as well as the development of metrics to evaluate adaptive controller performance at off-nominal flight conditions. This paper presents the major certification gap areas, a description of the current state of the verification methodologies, and what further research efforts will likely be needed to close the gaps remaining in current certification practices. It is envisioned that closing the gap will require certain advances in simulation methods, comprehensive methods to determine learning algorithm stability and convergence rates, the development of performance metrics for adaptive controllers, the application of formal software assurance methods, the application of on-line software monitoring tools for adaptive controller health assessment, and the development of a certification case for adaptive system safety of flight.

Jacklin, Stephen A.↗

Parsing-based Approaches for Verification and Recognition of Hierarchical Plans

Hierarchical Task Networks were proposed as a method todescribe plans by decomposition of tasks to sub-tasks untilprimitive tasks, actions, are obtained. Plan verification assumesa complete plan as input, and the objective is findinga task that decomposes to this plan. In plan recognition, aprefix of the plan is given and the objective is finding a taskthat decomposes to the (shortest) plan with the given prefix.This paper describes how to verify and recognize plans usinga common method known from formal grammars, by parsing.

Bartak, Roman↗

A Game-Theoretic Quantum Algorithm for Solving Magic Squares

Variational quantum algorithms (VQAs) offer a promising near-term approach to finding optimal quantum strategies for playing non-local games. These games test quantum correlations beyond classical limits and enable entanglement verification. In this work, we present a variational framework for the Magic Square Game (MSG), a two-player non-local game with perfect quantum advantage. We construct a value Hamiltonian that encodes the game’s parity and consistency constraints, then optimize parameterize quantum circuits to minimize this cost. Our approach build on the stabilizer formalism, leverages commutation structure for circuit design, and is hardware-efficient. Compared to existing work, our contribution emphasizes algebraic structure an interpretability. We validate our method through numerical experiments and outline generalizations to larger games.

Chehade, Sarah [ORNL]↗