Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Formal Methods”

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 271 records · Page 15
All sourcesNASA NTRSDOE OSTI
NASA NTRS2006

Simulated Data for High Temperature Composite Design

The paper describes an effective formal method that can be used to simulate design properties for composites that is inclusive of all the effects that influence those properties. This effective simulation method is integrated computer codes that include composite micromechanics, composite macromechanics, laminate theory, structural analysis, and multi-factor interaction model. Demonstration of the method includes sample examples for static, thermal, and fracture reliability for a unidirectional metal matrix composite as well as rupture strength and fatigue strength for a high temperature super alloy. Typical results obtained for a unidirectional composite show that the thermal properties are more sensitive to internal local damage, the longitudinal properties degrade slowly with temperature, the transverse and shear properties degrade rapidly with temperature as do rupture strength and fatigue strength for super alloys.

Chamis, Christos C.↗
NASA NTRS2008

Challenges and Demands on Automated Software Revision

In the past three decades, automated program verification has undoubtedly been one of the most successful contributions of formal methods to software development. However, when verification of a program against a logical specification discovers bugs in the program, manual manipulation of the program is needed in order to repair it. Thus, in the face of existence of numerous unverified and un- certified legacy software in virtually any organization, tools that enable engineers to automatically verify and subsequently fix existing programs are highly desirable. In addition, since requirements of software systems often evolve during the software life cycle, the issue of incomplete specification has become a customary fact in many design and development teams. Thus, automated techniques that revise existing programs according to new specifications are of great assistance to designers, developers, and maintenance engineers. As a result, incorporating program synthesis techniques where an algorithm generates a program, that is correct-by-construction, seems to be a necessity. The notion of manual program repair described above turns out to be even more complex when programs are integrated with large collections of sensors and actuators in hostile physical environments in the so-called cyber-physical systems. When such systems are safety/mission- critical (e.g., in avionics systems), it is essential that the system reacts to physical events such as faults, delays, signals, attacks, etc, so that the system specification is not violated. In fact, since it is impossible to anticipate all possible such physical events at design time, it is highly desirable to have automated techniques that revise programs with respect to newly identified physical events according to the system specification.

Bonakdarpour, Borzoo↗
NASA NTRS2009

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↗
NASA NTRS2009

A Reference Model for Software and System Inspections. White Paper

Software Quality Assurance (SQA) is an important component of the software development process. SQA processes provide assurance that the software products and processes in the project life cycle conform to their specified requirements by planning, enacting, and performing a set of activities to provide adequate confidence that quality is being built into the software. Typical techniques include: (1) Testing (2) Simulation (3) Model checking (4) Symbolic execution (5) Management reviews (6) Technical reviews (7) Inspections (8) Walk-throughs (9) Audits (10) Analysis (complexity analysis, control flow analysis, algorithmic analysis) (11) Formal method Our work over the last few years has resulted in substantial knowledge about SQA techniques, especially the areas of technical reviews and inspections. But can we apply the same QA techniques to the system development process? If yes, what kind of tailoring do we need before applying them in the system engineering context? If not, what types of QA techniques are actually used at system level? And, is there any room for improvement.) After a brief examination of the system engineering literature (especially focused on NASA and DoD guidance) we found that: (1) System and software development process interact with each other at different phases through development life cycle (2) Reviews are emphasized in both system and software development. (Figl.3). For some reviews (e.g. SRR, PDR, CDR), there are both system versions and software versions. (3) Analysis techniques are emphasized (e.g. Fault Tree Analysis, Preliminary Hazard Analysis) and some details are given about how to apply them. (4) Reviews are expected to use the outputs of the analysis techniques. In other words, these particular analyses are usually conducted in preparation for (before) reviews. The goal of our work is to explore the interaction between the Quality Assurance (QA) techniques at the system level and the software level.

He, Lulu↗
NASA NTRS2010

A Technique for the Assessment of Flight Operability Characteristics of Human Rated Spacecraft

In support of new human rated spacecraft development programs, the Mission Operations Directorate at NASA Johnson Space Center has implemented a formal method for the assessment of spacecraft operability. This "Spacecraft Flight Operability Assessment Scale" defines six key themes of flight operability, with guiding principles and goals stated for each factor. A standardized rating technique provides feedback that is useful to the operations, design and program management communities. Applicability of this concept across the program structure and life cycle is addressed. Examples of operationally desirable and undesirable spacecraft design characteristics are provided, as is a sample of the assessment scale product.

Crocker, Alan↗
NASA NTRS2010

Verification and Validation of Flight-Critical Systems

For the first time in many years, the NASA budget presented to congress calls for a focused effort on the verification and validation (V&V) of complex systems. This is mostly motivated by the results of the VVFCS (V&V of Flight-Critical Systems) study, which should materialize as a a concrete effort under the Aviation Safety program. This talk will present the results of the study, from requirements coming out of discussions with the FAA and the Joint Planning and Development Office (JPDO) to technical plan addressing the issue, and its proposed current and future V&V research agenda, which will be addressed by NASA Ames, Langley, and Dryden as well as external partners through NASA Research Announcements (NRA) calls. This agenda calls for pushing V&V earlier in the life cycle and take advantage of formal methods to increase safety and reduce cost of V&V. I will present the on-going research work (especially the four main technical areas: Safety Assurance, Distributed Systems, Authority and Autonomy, and Software-Intensive Systems), possible extensions, and how VVFCS plans on grounding the research in realistic examples, including an intended V&V test-bench based on an Integrated Modular Avionics (IMA) architecture and hosted by Dryden.

Brat, Guillaume↗
NASA NTRS2009

Modeling Guidelines for Code Generation in the Railway Signaling Context

Modeling guidelines constitute one of the fundamental cornerstones for Model Based Development. Their relevance is essential when dealing with code generation in the safety-critical domain. This article presents the experience of a railway signaling systems manufacturer on this issue. Introduction of Model-Based Development (MBD) and code generation in the industrial safety-critical sector created a crucial paradigm shift in the development process of dependable systems. While traditional software development focuses on the code, with MBD practices the focus shifts to model abstractions. The change has fundamental implications for safety-critical systems, which still need to guarantee a high degree of confidence also at code level. Usage of the Simulink/Stateflow platform for modeling, which is a de facto standard in control software development, does not ensure by itself production of high-quality dependable code. This issue has been addressed by companies through the definition of modeling rules imposing restrictions on the usage of design tools components, in order to enable production of qualified code. The MAAB Control Algorithm Modeling Guidelines (MathWorks Automotive Advisory Board)[3] is a well established set of publicly available rules for modeling with Simulink/Stateflow. This set of recommendations has been developed by a group of OEMs and suppliers of the automotive sector with the objective of enforcing and easing the usage of the MathWorks tools within the automotive industry. The guidelines have been published in 2001 and afterwords revisited in 2007 in order to integrate some additional rules developed by the Japanese division of MAAB [5]. The scope of the current edition of the guidelines ranges from model maintainability and readability to code generation issues. The rules are conceived as a reference baseline and therefore they need to be tailored to comply with the characteristics of each industrial context. Customization of these recommendations has been performed for the automotive control systems domain in order to enforce code generation [7]. The MAAB guidelines have been found profitable also in the aerospace/avionics sector [1] and they have been adopted by the MathWorks Aerospace Leadership Council (MALC). General Electric Transportation Systems (GETS) is a well known railway signaling systems manufacturer leading in Automatic Train Protection (ATP) systems technology. Inside an effort of adopting formal methods within its own development process, GETS decided to introduce system modeling by means of the MathWorks tools [2], and in 2008 chose to move to code generation. This article reports the experience performed by GETS in developing its own modeling standard through customizing the MAAB rules for the railway signaling domain and shows the result of this experience with a successful product development story.

Ferrari, Alessio↗
NASA NTRS2010

Hybrid Decompositional Verification for Discovering Failures in Adaptive Flight Control Systems

Adaptive flight control systems hold tremendous promise for maintaining the safety of a damaged aircraft and its passengers. However, most currently proposed adaptive control methodologies rely on online learning neural networks (OLNNs), which necessarily have the property that the controller is changing during the flight. These changes tend to be highly nonlinear, and difficult or impossible to analyze using standard techniques. In this paper, we approach the problem with a variant of compositional verification. The overall system is broken into components. Undesirable behavior is fed backwards through the system. Components which can be solved using formal methods techniques explicitly for the ranges of safe and unsafe input bounds are treated as white box components. The remaining black box components are analyzed with heuristic techniques that try to predict a range of component inputs that may lead to unsafe behavior. The composition of these component inputs throughout the system leads to overall system test vectors that may elucidate the undesirable behavior

Thompson, Sarah↗
NASA NTRS2011

Making Human Spaceflight Practical and Affordable: Spacecraft Designs and their Degree of Operability

As we push toward new and diverse space transportation capabilities, reduction in operations cost becomes increasingly important. Achieving affordable and safe human spaceflight capabilities will be the mark of success for new programs and new providers. The ability to perceive the operational implications of design decisions is crucial in developing safe yet cost competitive space transportation systems. Any human spaceflight program - government or commercial - must make countless decisions either to implement spacecraft system capabilities or adopt operational constraints or workarounds to account for the lack of such spacecraft capabilities. These decisions can benefit from the collective experience that NASA has accumulated in building and operating crewed spacecraft over the last five decades. This paper reviews NASA s history in developing and operating human rated spacecraft, reviewing the key aspects of spacecraft design and their resultant impacts on operations phase complexity and cost. Specific examples from current and past programs - including the Space Shuttle and International Space Station - are provided to illustrate design traits that either increase or increase cost and complexity associated with spacecraft operations. These examples address factors such as overall design performance margins, levels of redundancy, degree of automated failure response, type and quantity of command and telemetry interfaces, and the definition of reference scenarios for analysis and test. Each example - from early program requirements, design implementation and resulting real-time operations experience - to tell the end-to-end "story" Based on these experiences, specific techniques are recommended to enable earlier and more effective assessment of operations concerns during the design process. A formal method for the assessment of spacecraft operability is defined and results of such operability assessments for recent spacecraft designs are provided. Recent experience in applying these techniques to Orion spacecraft development is reviewed to highlight the direct benefits of early operational assessment and collaborative development efforts.

Crocker, Alan R.↗
NASA NTRS2011

Resolution of an Orbital Issue: A Designed Experiment

Design of Experiments (DOE) is a systematic approach to investigation of a system or process. A series of structured tests are designed in which planned changes are made to the input variables of a process or system. The effects of these changes on a pre-defined output are then assessed. DOE is a formal method of maximizing information gained while minimizing resources required.

Huddleston, Lisa L.↗
NASA NTRS2011

NASA's Advanced Multimission Operations System: A Case Study in Formalizing Software Architecture Evolution

All software systems of significant size and longevity eventually undergo changes to their basic architectural structure. Such changes may be prompted by evolving requirements, changing technology, or other reasons. Whatever the cause, software architecture evolution is commonplace in real world software projects. Recently, software architecture researchers have begun to study this phenomenon in depth. However, this work has suffered from problems of validation; research in this area has tended to make heavy use of toy examples and hypothetical scenarios and has not been well supported by real world examples. To help address this problem, I describe an ongoing effort at the Jet Propulsion Laboratory to re-architect the Advanced Multimission Operations System (AMMOS), which is used to operate NASA's deep-space and astrophysics missions. Based on examination of project documents and interviews with project personnel, I describe the goals and approach of this evolution effort and then present models that capture some of the key architectural changes. Finally, I demonstrate how approaches and formal methods from my previous research in architecture evolution may be applied to this evolution, while using languages and tools already in place at the Jet Propulsion Laboratory.

software architecture evolution↗
NASA NTRS2012

Certification of Safety-Critical Software Under DO-178C and DO-278A

The RTCA has recently released DO-178C and DO-278A as new certification guidance for the production of airborne and ground-based air traffic management software, respectively. Additionally, RTCA special committee SC-205 has also produced, at the same time, five other companion documents. These documents are RTCA DO-248C, DO-330, DO-331, DO- 332, and DO-333. These supplements address frequently asked questions about software certification, provide guidance on tool qualification requirements, and illustrate the modifications recommended to DO-178C when using model-based software design, object oriented programming, and formal methods. The objective of this paper is to first explain the relationship of DO-178C to the former DO-178B in order to give those familiar with DO- 178B an indication of what has been changed and what has not been changed. With this background, the relationship of DO-178C and DO-278 to the new DO-278A document for ground-based software development is shown. Last, an overview of the new guidance contained in the tool qualification document and the three new supplements to DO-178C and DO-278A is presented. For those unfamiliar with DO-178B, this paper serves to provide an entry point to this new certification guidance for airborne and ground-based CNS/ATM software certification.

Jacklin, Stephen A.↗
NASA NTRS2016

ICAROUS: Integrated Configurable Architecture for Unmanned Systems

NASA's Unmanned Aerial System (UAS) Traffic Management (UTM) project aims at enabling near-term, safe operations of small UAS vehicles in uncontrolled airspace, i.e., Class G airspace. A far-term goal of UTM research and development is to accommodate the expected rise in small UAS traffic density throughout the National Airspace System (NAS) at low altitudes for beyond visual line-of-sight operations. This video describes a new capability referred to as ICAROUS (Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems), which is being developed under the auspices of the UTM project. ICAROUS is a software architecture comprised of highly assured algorithms for building safety-centric, autonomous, unmanned aircraft applications. Central to the development of the ICAROUS algorithms is the use of well-established formal methods to guarantee higher levels of safety assurance by monitoring and bounding the behavior of autonomous systems. The core autonomy-enabling capabilities in ICAROUS include constraint conformance monitoring and autonomous detect and avoid functions. ICAROUS also provides a highly configurable user interface that enables the modular integration of mission-specific software components.

Consiglio, Maria C.↗
NASA NTRS2016

ICAROUS - Integrated Configurable Algorithms for Reliable Operations Of Unmanned Systems

NASA's Unmanned Aerial System (UAS) Traffic Management (UTM) project aims at enabling near-term, safe operations of small UAS vehicles in uncontrolled airspace, i.e., Class G airspace. A far-term goal of UTM research and development is to accommodate the expected rise in small UAS traffic density throughout the National Airspace System (NAS) at low altitudes for beyond visual line-of-sight operations. This paper describes a new capability referred to as ICAROUS (Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems), which is being developed under the UTM project. ICAROUS is a software architecture comprised of highly assured algorithms for building safety-centric, autonomous, unmanned aircraft applications. Central to the development of the ICAROUS algorithms is the use of well-established formal methods to guarantee higher levels of safety assurance by monitoring and bounding the behavior of autonomous systems. The core autonomy-enabling capabilities in ICAROUS include constraint conformance monitoring and contingency control functions. ICAROUS also provides a highly configurable user interface that enables the modular integration of mission-specific software components.

Consiglio, María↗
NASA NTRS2017

Advanced Software V&V for Civil Aviation and Autonomy

With the advances in high-computing platform (e.g., advanced graphical processing units or multi-core processors), computationally-intensive software techniques such as the ones used in artificial intelligence or formal methods have provided us with an opportunity to further increase safety in the aviation industry. Some of these techniques have facilitated building safety at design time, like in aircraft engines or software verification and validation, and others can introduce safety benefits during operations as long as we adapt our processes. In this talk, I will present how NASA is taking advantage of these new software techniques to build in safety at design time through advanced software verification and validation, which can be applied earlier and earlier in the design life cycle and thus help also reduce the cost of aviation assurance. I will then show how run-time techniques (such as runtime assurance or data analytics) offer us a chance to catch even more complex problems, even in the face of changing and unpredictable environments. These new techniques will be extremely useful as our aviation systems become more complex and more autonomous.

software assurance↗
NASA NTRS2017

A Fuzzy Logic Approach for Separation Assurance and Collision Avoidance for Unmanned Aerial Systems

In the coming years, operations in low altitude airspace will vastly increase as the capabilities and applications of small Unmanned Aerial Systems (sUAS) continue to multiply. Therefore, solutions to managing sUAS in highly congested airspace must be explored. In this study, a Fuzzy Logic based approach was used to help mitigate the risk of collisions between aircraft using separation assurance and collision avoidance techniques. The system was evaluated for its effectiveness to mitigate the risk of mid-air collisions between aircraft. This system utilizes only current state information and can resolve potential conflicts without knowledge of intruder intent. The avoidance logic was verified using formal methods and shown to select the correct action in all instances. Additionally, the Fuzzy Logic Controllers were shown to always turn the vehicles in the correct direction. Numerical testing demonstrated that the avoidance system was able to prevent a mid-air collision between two sUAS in all tested cases. Simulations were also performed in a three-dimensional environment with a heterogenous fleet of sUAS performing a variety of realistic missions. Simulations showed that the system was 99.98 effective at preventing mid-air collisions when separation assurance was disabled (unmitigated case) and 100 effective when enabled (mitigated case).

Verification & Validation of a Fuzzy Logic Control↗
NASA NTRS2019

Static Analysis Using Abstract Interpretation

Lecture about abstract interpretation. This lecture starts with a brief introduction to validation and verification using formal methods. It then demonstrates IKOS (Inference Kernel for Open Static Analyzers), a static analyzer for C/C++ based on Abstract Interpretation. Then, it describes in details the theory of Abstract Interpretation, a mathematical framework to over-approximate the reachable states of a program.

Arthaud, Maxime↗
NASA NTRS2020

Formal Verification of a Solution to the n-Queens Problem

This report describes a formal verification of a concise algorithm that computes a solution to the n-Queens problem for all natural numbers n, such that n > 3. The formal proof of the algorithm is completed in the Prototype Verification System (PVS) theorem prover. This verification effort serves two purposes. First, it is presented as a pedagogical example for learning a theorem prover, such as PVS, and second, as a candidate benchmark for comparing other formal methods tools to PVS.

Mahyar R Malekpour↗