SEARCH · Engineering Papers

Results for “language models”

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 343 records · Page 19

All sources NASA NTRS DOE OSTI

NASA NTRS2004

Software for Checking Statecharts

HiVy is a software tool set that enables verification through model checking of designs represented as finite-state machines or statecharts. HiVy provides automated translation of (1) statecharts created by use of the MathWorks Stateflow program to (2) Promela, the input language of the Spin model checker, which can then be used to verify, or trace logical errors in, distributed software systems. HiVy can operate directly on Stateflow models, or its abstract syntax of hierarchical sequential automata (HSA) can be used independently as an intermediate format for translation to Promela. In a typical design application, HiVy parses and reformats Stateflow model file data using the programs SfParse and sf2hsa, respectively. If the parsing effort is successful, an abstract syntax tree is delivered into a file named with the extension .hsa. If the design comprises several model files, they may be merged into one .hsa file before translation into Promela. Stateflow scope is preserved, and name clashes are avoided in the merge process. The HiVy program hsa2pr translates the model from the intermediate HSA format into Promela. Additionally, HiVy provides through translation a list of all statechart model propositions that are the means for formalizing linear temporal logic (LTL) properties about the model for Spin verification.

Pingree, Paula↗

NASA NTRS1986

ASSIST: User's manual

Semi-Markov models can be used to compute the reliability of virtually any fault-tolerant system. However, the process of delineating all of the states and transitions in a model of a complex system can be devastingly tedious and error-prone. The ASSIST program allows the user to describe the semi-Markov model in a high-level language. Instead of specifying the individual states of the model, the user specifies the rules governing the behavior of the system and these are used by ASSIST to automatically generate the model. The ASSIST program is described and illustrated by examples.

Johnson, S. C.↗

NASA NTRS1988

Improvement and extension of a radar forest backscattering model

Research to-date has focused on modeling development and programming based on model components proposed during the past several months and research progress made by the Simonett team. The model components and programs (in C language under UNIX) finished to date are summarized. These model components may help explain the contributions of various vegetation structural components to the attenuation and backscattering of vegetated surfaces to extract useful data concerning forest stands and their underlying surfaces for both the seawater-on and seawater-off.

Simonett, David S.↗

NASA NTRS1991

Computer Language For Optimization Of Design

SOL is computer language geared to solution of design problems. Includes mathematical modeling and logical capabilities of computer language like FORTRAN; also includes additional power of nonlinear mathematical programming methods at language level. SOL compiler takes SOL-language statements and generates equivalent FORTRAN code and system calls. Provides syntactic and semantic checking for recovery from errors and provides detailed reports containing cross-references to show where each variable used. Implemented on VAX/VMS computer systems. Requires VAX FORTRAN compiler to produce executable program.

Scotti, Stephen J.↗

NASA NTRS2005

Model Checking Artificial Intelligence Based Planners: Even the Best Laid Plans Must Be Verified

Automated planning systems (APS) are gaining acceptance for use on NASA missions as evidenced by APS flown On missions such as Orbiter and Deep Space 1 both of which were commanded by onboard planning systems. The planning system takes high level goals and expands them onboard into a detailed of action fiat the spacecraft executes. The system must be verified to ensure that the automatically generated plans achieve the goals as expected and do not generate actions that would harm the spacecraft or mission. These systems are typically tested using empirical methods. Formal methods, such as model checking, offer exhaustive or measurable test coverage which leads to much greater confidence in correctness. This paper describes a formal method based on the SPIN model checker. This method guarantees that possible plans meet certain desirable properties. We express the input model in Promela, the language of SPIN and express the properties of desirable plans formally.

model checking↗

NASA NTRS2014

Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior

A key challenge in operating remote spacecraft is that ground operators must rely on the limited visibility available through spacecraft telemetry in order to assess spacecraft health and operational status. We describe a tool for processing spacecraft telemetry that allows ground operators to impose structure on received telemetry in order to achieve a better comprehension of system state. A key element of our approach is the design of a domain-specific language that allows operators to express models of expected system behavior using partial specifications. The language allows behavior specifications with data fields, similar to other recent runtime verification systems. What is notable about our approach is the ability to develop hierarchical specifications of behavior. The language is implemented as an internal DSL in the Scala programming language that synthesizes rules from patterns of specification behavior. The rules are automatically applied to received telemetry and the inferred behaviors are available to ground operators using a visualization interface that makes it easier to understand and track spacecraft state. We describe initial results from applying our tool to telemetry received from the Curiosity rover currently roving the surface of Mars, where the visualizations are being used to trend subsystem behaviors, in order to identify potential problems before they happen. However, the technology is completely general and can be applied to any system that generates telemetry such as event logs.

Runtime monitoring↗

NASA NTRSDate not supplied

How ExMC Communicates a System Model to Non-Modelers

NASA’s Human Research Program (HRP) Exploration Medical Capability (ExMC) Element adopted Systems Engineering (SE) principles and Model Based Systems Engineering (MBSE) tools to capture the system functions, system architecture, requirements, interfaces, and clinical capabilities for a future exploration medical system. There are many different stakeholders who may use the information in the model: systems engineers, clinicians (physicians, nurses, and pharmacists), scientists, and mission planners. Many of these stakeholders have neither access to MBSE modeling tools nor experience with SE modeling techniques. The challenge faced by ExMC SE team was how to present the content in the model to non-modelers in a way they would understand the content with limited training in MBSE and without using the modeling tool. ExMC SE team created a Hypertext Markup Language (HTML) report that shows key model content and is accessible to anyone with a browser. When creating the HTML report, the ExMC SE received stakeholder feedback on what content they wanted and how to display this content. Incorporating this feedback, the report arranges the content in a way that directs readers through the SE process taken to derive the requirements and helps them to understand the fundamental steps in an SE approach. The report includes links to source information (e.g., NASA documentation that describes levels of care) and other SE products (e.g., Concept of Operations). These links were provided to aid in the understanding of how the team created this content through a methodical SE approach. This presentation outlines the process used to develop the model, the data chosen to share with stakeholders, many of the model elements used in the report, the review process stakeholders followed, the comments received from the stakeholders, and the lessons ExMC learned through producing this HTML report.

J. Cohen↗

NASA NTRS1985

Using a data base management system for modelling SSME test history data

The usefulness of a data base management system (DBMS) for modelling historical test data for the complete series of static test firings for the Space Shuttle Main Engine (SSME) was assessed. From an analysis of user data base query requirements, it became clear that a relational DMBS which included a relationally complete query language would permit a model satisfying the query requirements. Representative models and sample queries are discussed. A list of environment-particular evaluation criteria for the desired DBMS was constructed; these criteria include requirements in the areas of user-interface complexity, program independence, flexibility, modifiability, and output capability. The evaluation process included the construction of several prototype data bases for user assessement. The systems studied, representing the three major DBMS conceptual models, were: MIRADS, a hierarchical system; DMS-1100, a CODASYL-based network system; ORACLE, a relational system; and DATATRIEVE, a relational-type system.

Abernethy, K.↗

NASA NTRS2021

Architectural Modeling and Analysis for Safety Engineering

Model-based development tools are increasingly being used for system-level development of safety-critical systems. Architectural and behavioral models provide important information that can be leveraged to improve the system safety analysis process. Model-based design artifacts produced in early stage development activities can be used to perform system safety analysis, reducing costs and providing accurate results throughout the system life-cycle. In this report we describe an extension to the Architecture Analysis and Design Language (AADL) that supports modeling of system behavior under failure conditions. This Safety Annex enables the independent modeling of component failures and allows safety engineers to weave various types of fault behavior into the nominal system model. The accompanying tool support uses model checking to propagate errors from their source to their effect on safety properties without the need to add separate propagation specifications. The tool also captures all minimal set of fault combinations that can cause violation of the safety properties, that can be compared to qualitative and quantitative objectives as part of the safety assessment process. We describe the Safety Annex, illustrate its use with a representative example, and discuss and demonstrate the tool support enabling an analyst to investigate the system behavior under failure conditions.

FTA↗

NASA NTRS2018

The SPASE Data Model: A Metadata Standard for Registering, Finding, Accessing, and Using Heliophysics Data Obtained from Observations and Modeling

The Space Physics Archive Search and Extract Consortium has developed and implemented the SPASE Data Model that provides a common language for registering a wide range of Heliophysics data and other products. The Data Model enables discovery and access tools such that any researcher can obtain data easily, thereby facilitating research, including on space weather. The Data Model includes descriptions of Simulation Models and Numerical Output, pioneered by the Integrated Medium for Planetary Exploration (IMPEx) group in Europe, and subsequently adopted by the Community Coordinated Modeling Center (CCMC). The SPASE group intends to register all relevant Heliophysics data resources, including space-, ground-, and model-based. Substantial progress has been made, especially for space-based observational data and associated observatories, instruments, and display data. Legacy product registrations and access go back more than 50 years. Real-time data will be included. The National Aeronautics and Space Administration (NASA) portion of the SPASE group has funding that assures continuity in the upkeep of the Data Model and aids with adding new products. Tools are being developed for making and editing data descriptions. Digital Object Identifiers (DOIs) for Data Products can now be included in the descriptions. The data access that SPASE facilitates is becoming more uniform, and work is progressing on Web Service access via a standard Application Programming Interface. The SPASE Data Model is stable; changes over the past 9 years were additions of terms and capabilities that are backward compatible. This paper provides a summary of the history, structure, use, and future of the SPASE Data Model.

Roberts, D. Aaron↗

NASA NTRS2007

Blurring the Inputs: A Natural Language Approach to Sensitivity Analysis

To document model parameter uncertainties and to automate sensitivity analyses for numerical simulation codes, a natural-language-based method to specify tolerances has been developed. With this new method, uncertainties are expressed in a natural manner, i.e., as one would on an engineering drawing, namely, 5.25 +/- 0.01. This approach is robust and readily adapted to various application domains because it does not rely on parsing the particular structure of input file formats. Instead, tolerances of a standard format are added to existing fields within an input file. As a demonstration of the power of this simple, natural language approach, a Monte Carlo sensitivity analysis is performed for three disparate simulation codes: fluid dynamics (LAURA), radiation (HARA), and ablation (FIAT). Effort required to harness each code for sensitivity analysis was recorded to demonstrate the generality and flexibility of this new approach.

Kleb, William L.↗

NASA NTRS1972

Development of a model of machine hand eye coordination and program specifications for a topological machine vision system

A unified approach to computer vision and manipulation is developed which is called choreographic vision. In the model, objects to be viewed by a projected robot in the Viking missions to Mars are seen as objects to be manipulated within choreographic contexts controlled by a multimoded remote, supervisory control system on Earth. A new theory of context relations is introduced as a basis for choreographic programming languages. A topological vision model is developed for recognizing objects by shape and contour. This model is integrated with a projected vision system consisting of a multiaperture image dissector TV camera and a ranging laser system. System program specifications integrate eye-hand coordination and topological vision functions and an aerospace multiprocessor implementation is described.

Source record↗

NASA NTRS2016

Topic Modeling of NASA Space System Problem Reports: Research in Practice

Problem reports at NASA are similar to bug reports: they capture defects found during test, post-launch operational anomalies, and document the investigation and corrective action of the issue. These artifacts are a rich source of lessons learned for NASA, but are expensive to analyze since problem reports are comprised primarily of natural language text. We apply topic modeling to a corpus of NASA problem reports to extract trends in testing and operational failures. We collected 16,669 problem reports from six NASA space flight missions and applied Latent Dirichlet Allocation topic modeling to the document corpus. We analyze the most popular topics within and across missions, and how popular topics changed over the lifetime of a mission. We find that hardware material and flight software issues are common during the integration and testing phase, while ground station software and equipment issues are more common during the operations phase. We identify a number of challenges in topic modeling for trend analysis: 1) that the process of selecting the topic modeling parameters lacks definitive guidance, 2) defining semantically-meaningful topic labels requires nontrivial effort and domain expertise, 3) topic models derived from the combined corpus of the six missions were biased toward the larger missions, and 4) topics must be semantically distinct as well as cohesive to be useful. Nonetheless,topic modeling can identify problem themes within missions and across mission lifetimes, providing useful feedback to engineers and project managers.

Data Mining↗

NASA NTRS2014

Spot: A Programming Language for Verified Flight Software

The C programming language is widely used for programming space flight software and other safety-critical real time systems. C, however, is far from ideal for this purpose: as is well known, it is both low-level and unsafe. This paper describes Spot, a language derived from C for programming space flight systems. Spot aims to maintain compatibility with existing C code while improving the language and supporting verification with the SPIN model checker. The major features of Spot include actor-based concurrency, distributed state with message passing and transactional updates, and annotations for testing and verification. Spot also supports domain-specific annotations for managing spacecraft state, e.g., communicating telemetry information to the ground. We describe the motivation and design rationale for Spot, give an overview of the design, provide examples of Spot's capabilities, and discuss the current status of the implementation.

validation↗

NASA NTRS1994

A Modular, Portable Model of Image Fidelity

There is a persistent need for a trustworthy model of perceptual image fidelity, especially in applications such as image compression and display design. A fidelity model provides a measure of the visual discriminability of two images. Ahumada has previously shown that the existing fidelity models may be categorized according to their inclusion of various canonical properties, such as a contrast sensitivity function, spatial frequency channels, etc. This suggests that research would be aided by the availability of a modular model, in which these components could be easily inserted or removed. A further impediment to research in this area has been that most models are written in low-level languages and are consequently large, non-portable, and difficult to understand, modify, and maintain. We therefore believe research would also be aided by models written in high-level languages. To serve both of these purposes, and to honor our conference host for his lifetime dedication to the problem of image quality. Global brightness and its effect on perceptual image quality. We offer a modular model written in the high-level language Mathematica. We will demonstrate this model and show how it may be modified.

Watson, Andrew B.↗

NASA NTRS2000

A Flexible Statechart-to-Model-Checker Translator

Many current-day software design tools offer some variant of statechart notation for system specification. We, like others, have built an automatic translator from (a subset of) statecharts to a model checker, for use to validate behavioral requirements. Our translator is designed to be flexible. This allows us to quickly adjust the translator to variants of statechart semantics, including problem-specific notational conventions that designers employ. Our system demonstration will be of interest to the following two communities: (1) Potential end-users: Our demonstration will show translation from statecharts created in a commercial UML tool (Rational Rose) to Promela, the input language of Holzmann's model checker SPIN. The translation is accomplished automatically. To accommodate the major variants of statechart semantics, our tool offers user-selectable choices among semantic alternatives. Options for customized semantic variants are also made available. The net result is an easy-to-use tool that operates on a wide range of statechart diagrams to automate the pathway to model-checking input. (2) Other researchers: Our translator embodies, in one tool, ideas and approaches drawn from several sources. Solutions to the major challenges of statechart-to-model-checker translation (e.g., determining which transition(s) will fire, handling of concurrent activities) are retired in a uniform, fully mechanized, setting. The way in which the underlying architecture of the translator itself facilitates flexible and customizable translation will also be evident.

Rouquette, Nicolas↗

NASA NTRS1999

Java PathFinder User Guide

The JAVA PATHFINDER, JPF, is a translator from a subset of JAVA 1.0 to PROMELA, the programming language of the SPIN model checker. The purpose of JPF is to establish a framework for verification and debugging of JAVA programming based on model checking. The main goal is to automate program verification such that a programmer can apply it in the daily work without the need for a specialist to manually reformulate a program into a different notation in order to analyze the program. The system is especially suited for analyzing multi-threaded JAVA applications, where normal testing usually falls short. The system can find deadlocks and violations of boolean assertions stated by the programmer in a special assertion language. This document explains how to Use JPF.

Havelund, Klaus↗

NASA NTRS2010

The Graphical Representation of the Digital Astronaut Physiology Backbone

This report summarizes my internship project with the NASA Digital Astronaut Project to analyze the Digital Astronaut (DA) physiology backbone model. The Digital Astronaut Project (DAP) applies integrated physiology models to support space biomedical operations, and to assist NASA researchers in closing knowledge gaps related to human physiologic responses to space flight. The DA physiology backbone is a set of integrated physiological equations and functions that model the interacting systems of the human body. The current release of the model is HumMod (Human Model) version 1.5 and was developed over forty years at the University of Mississippi Medical Center (UMMC). The physiology equations and functions are scripted in an XML schema specifically designed for physiology modeling by Dr. Thomas G. Coleman at UMMC. Currently it is difficult to examine the physiology backbone without being knowledgeable of the XML schema. While investigating and documenting the tags and algorithms used in the XML schema, I proposed a standard methodology for a graphical representation. This standard methodology may be used to transcribe graphical representations from the DA physiology backbone. In turn, the graphical representations can allow examination of the physiological functions and equations without the need to be familiar with the computer programming languages or markup languages used by DA modeling software.

Briers, Demarcus↗