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 163 records · Page 9
All sourcesNASA NTRSDOE OSTI
NASA NTRS1991

Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems

The formal specification and mechanically checked verification for a model of fault-masking and transient-recovery among the replicated computers of digital flight-control systems are presented. The verification establishes, subject to certain carefully stated assumptions, that faults among the component computers are masked so that commands sent to the actuators are the same as those that would be sent by a single computer that suffers no failures.

Rushby, John↗
NASA NTRS1998

An Integrated Environment for Efficient Formal Design and Verification

The general goal of this project was to improve the practicality of formal methods by combining techniques from model checking and theorem proving. At the time the project was proposed, the model checking and theorem proving communities were applying different tools to similar problems, but there was not much cross-fertilization. This project involved a group from SRI that had substantial experience in the development and application of theorem-proving technology, and a group at Stanford that specialized in model checking techniques. Now, over five years after the proposal was submitted, there are many research groups working on combining theorem-proving and model checking techniques, and much more communication between the model checking and theorem proving research communities. This project contributed significantly to this research trend. The research work under this project covered a variety of topics: new theory and algorithms; prototype tools; verification methodology; and applications to problems in particular domains.

Source record↗
NASA NTRS1994

Using formal specification in the Guidance and Control Software (GCS) experiment. Formal design and verification technology for life critical systems

The goal of this task was to investigate how formal methods could be incorporated into a software engineering process for flight-control systems under DO-178B and to demonstrate that process by developing a formal specification for NASA's Guidance and Controls Software (GCS) Experiment. GCS is software to control the descent of a spacecraft onto a planet's surface. The GCS example is simplified from a real example spacecraft, but exhibits the characteristics of realistic spacecraft control software. The formal specification is written in Larch.

Weber, Doug↗
NASA NTRS1990

Formal design and verification of a reliable computing platform for real-time control. Phase 1: Results

A high-level design is presented for a reliable computing platform for real-time control applications. Design tradeoffs and analyses related to the development of the fault-tolerant computing platform are discussed. The architecture is formalized and shown to satisfy a key correctness property. The reliable computing platform uses replicated processors and majority voting to achieve fault tolerance. Under the assumption of a majority of processors working in each frame, it is shown that the replicated system computes the same results as a single processor system not subject to failures. Sufficient conditions are obtained to establish that the replicated system recovers from transient faults within a bounded amount of time. Three different voting schemes are examined and proved to satisfy the bounded recovery time conditions.

Divito, Ben L.↗
NASA NTRS1993

On verifying a high-level design

An overview of design verification techniques is presented, and some of the current research in high-level design verification is described. Formal hardware description languages that are capable of adequately expressing the design specifications have been developed, but some time will be required before they can have the expressive power needed to be used in real applications. Simulation-based approaches are more useful in finding errors in designs than they are in proving the correctness of a certain design. Hybrid approaches that combine simulation with other formal design verification techniques are argued to be the most promising over the short term.

Mathew, Ben↗
NASA NTRS1995

Formal Methods Specification and Verification Guidebook for Software and Computer Systems: Planning and Technology Insertion - Volume 1

The Formal Methods Specification and Verification Guidebook for Software and Computer Systems describes a set of techniques called Formal Methods (FM), and outlines their use in the specification and verification of computer systems and software. Development of increasingly complex systems has created a need for improved specification and verification techniques. NASA's Safety and Mission Quality Office has supported the investigation of techniques such as FM, which are now an accepted method for enhancing the quality of aerospace applications. The guidebook provides information for managers and practitioners who are interested in integrating FM into an existing systems development process. Information includes technical and administrative considerations that must be addressed when establishing the use of FM on a specific project. The guidebook is intended to aid decision makers in the successful application of FM to the development of high-quality systems at reasonable cost. This is the first volume of a planned two-volume set. The current volume focuses on administrative and planning considerations for the successful application of FM.

Source record↗
NASA NTRSDate not supplied

Matrix Theory for Data Association in PVS

Consider a collection of data generated by sensors from a set of aircraft. Data association is the process of connecting each sensor measurement with its corresponding aircraft. Furthermore once the data association has taken place, the state of the aircraft can be approximated using a Kalman filter. This talk aims to explore formal specification and verification of data association in the Prototype Verification System (PVS). Formal specification and verification of data association includes development of Kalman filters, Mahalanobis distance, and other topics of matrix analysis in PVS.

Linear Algebra↗
NASA NTRS2019

Bridging the Gap Between Requirements and Model Analysis: Evaluation on Cyber-Physical Challenge Problems

We present a framework for introducing high-level requirement specifications in the automated analysis of dataflow models. By integrating the FRET requirements elicitation tool with the CoCoSim analyzer, our framework enables the analysis of hierarchical Simulink models against requirements written in a restricted English language. More precisely, we support: automatic extraction of Simulink model information and association of high-level requirements with target model signals and components; translation of temporal logic formulas into synchronous dataflow CoCoSpec specifications as well as Simulink monitors; and interpretation of counterexamples produced by the analysis both at the requirement and model level. The features provided by our framework are generic and can be used to integrate other requirements elicitation and Simulink/Lustre analysis tools. We report on the lessons learned from the application of our approach to the Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems. For the analysis, we used the Kind2, Zustre, and Simulink Design Verifier (SLDV) tools.

Simulink↗
NASA NTRSDate not supplied

Formal Specification and Parametric Verification of the ICAROUS Distributed Merging Protocol for Autonomous Aircraft Systems

ICAROUS is a software architecture that provides highly assured core software modules for building safety-centric autonomous unmanned aircraft applications. One of its core components is the ICAROUS distributed merging (IDM) protocol, which allows for decentralized merging of autonomous aircrafts through a designated intersection. This report presents initial results on formal specification and parametric verification of the IDM protocol. We present the development of a formal, discrete-time specification of the ICAROUS distributed merging protocol in TLA+. The developed TLA+ specification includes an abstracted model of the physical aircraft dynamics, the consensus machinery for leader election and coordination, and the computation of merging schedules. In addition, we present details on a command line tool we developed verimerge, that utilizes the TLC model checker for doing bounded, parametric verification and allows for plotting of these results in 2D parameter spaces. The tool also provides functionality for visualization of concrete protocol behaviors, to aid debugging and understanding. We present preliminary, bounded time verification results for a finite number of aircraft. Limitations of the current techniques and possible future extensions of this work are also discussed.

ICAROUS↗
NASA NTRS1993

Formal methods for life-critical software

The use of computer software in life-critical applications, such as for civil air transports, demands the use of rigorous formal mathematical verification procedures. This paper demonstrates how to apply formal methods to the development and verification of software by leading the reader step-by-step through requirements analysis, design, implementation, and verification of an electronic phone book application. The current maturity and limitations of formal methods tools and techniques are then discussed, and a number of examples of the successful use of formal methods by industry are cited.

Butler, Ricky W.↗
NASA NTRS1993

Formal Methods for Life-Critical Software

The use of computer software in life-critical applications, such as for civil air transports, demands the use of rigorous formal mathematical verification procedures. This paper demonstrates how to apply formal methods to the development and verification of software by leading the reader step-by-step through requirements analysis, design, implementation, and verification of an electronic phone book application. The current maturity and limitations of formal methods tools and techniques are then discussed, and a number of examples of the successful use of formal methods by industry are cited.

Butler, Ricky W.↗
DOE OSTI2024

Multi-Rigor Agile Verification and Rapid Prototyping for Formally Verified Software

We propose a novel approach to developing formally verified systems through Multi-rigor Agile Verification. Multi-rigor Agile Verification is rooted in the hypothesis of Rigor Independence, that a system’s specification and verification architecture depend primarily on the system requirements to be verified, and they depend very little on the rigor level of the methods used to verify those requirements. Due to its iterative nature, Multi-rigor Agile Verification promises to mitigate many of the high upfront design costs experienced by formally verified systems and to deliver a better-architected, and thus better-trusted, system in the end. We then discuss the tooling needed to perform Multi-rigor Agile Verification and go in depth to build one of those tools, which directly generates executable prototype code from declarative formal specifications using the Maude rewrite-logic framework.

97 MATHEMATICS AND COMPUTING↗
NASA NTRS1982

Formal specification and mechanical verification of SIFT - A fault-tolerant flight control system

The paper describes the methodology being employed to demonstrate rigorously that the SIFT (software-implemented fault-tolerant) computer meets its requirements. The methodology uses a hierarchy of design specifications, expressed in the mathematical domain of multisorted first-order predicate calculus. The most abstract of these, from which almost all details of mechanization have been removed, represents the requirements on the system for reliability and intended functionality. Successive specifications in the hierarchy add design and implementation detail until the PASCAL programs implementing the SIFT executive are reached. A formal proof that a SIFT system in a 'safe' state operates correctly despite the presence of arbitrary faults has been completed all the way from the most abstract specifications to the PASCAL program.

Melliar-Smith, P. M.↗