SEARCH · Engineering Papers
Results for “Semantic 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.
Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.
The scheme machine: A case study in progress in design derivation at system levels
The Scheme Machine is one of several design projects of the Digital Design Derivation group at Indiana University. It differs from the other projects in its focus on issues of system design and its connection to surrounding research in programming language semantics, compiler construction, and programming methodology underway at Indiana and elsewhere. The genesis of the project dates to the early 1980's, when digital design derivation research branched from the surrounding research effort in programming languages. Both branches have continued to develop in parallel, with this particular project serving as a bridge. However, by 1990 there remained little real interaction between the branches and recently we have undertaken to reintegrate them. On the software side, researchers have refined a mathematically rigorous (but not mechanized) treatment starting with the fully abstract semantic definition of Scheme and resulting in an efficient implementation consisting of a compiler and virtual machine model, the latter typically realized with a general purpose microprocessor. The derivation includes a number of sophisticated factorizations and representations and is also deep example of the underlying engineering methodology. The hardware research has created a mechanized algebra supporting the tedious and massive transformations often seen at lower levels of design. This work has progressed to the point that large scale devices, such as processors, can be derived from first-order finite state machine specifications. This is roughly where the language oriented research stops; thus, together, the two efforts establish a thread from the highest levels of abstract specification to detailed digital implementation. The Scheme Machine project challenges hardware derivation research in several ways, although the individual components of the system are of a similar scale to those we have worked with before. The machine has a custom dual-ported memory to support garbage collection. It consists of four tightly coupled processes--processor, collector, allocator, memory--with a very non-trivial synchronization relationship. Finally, there are deep issues of representation for the run-time objects of a symbolic processing language. The research centers on verification through integrated formal reasoning systems, but is also involved with modeling and prototyping environments. Since the derivation algebra is basd on an executable modeling language, there is opportunity to incorporate design animation in the design process. We are looking for ways to move smoothly and incrementally from executable specifications into hardware realization. For example, we can run the garbage collector specification, a Scheme program, directly against the physical memory prototype, and similarly, the instruction processor model against the heap implementation.
The SeaHorn Verification Framework
In this paper, we present SeaHorn, a software verification framework. The key distinguishing feature of SeaHorn is its modular design that separates the concerns of the syntax of the programming language, its operational semantics, and the verification semantics. SeaHorn encompasses several novelties: it (a) encodes verification conditions using an efficient yet precise inter-procedural technique, (b) provides flexibility in the verification semantics to allow different levels of precision, (c) leverages the state-of-the-art in software model checking and abstract interpretation for verification, and (d) uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with multiple verification tools based on Horn-clauses. SeaHorn provides users with a powerful verification tool and researchers with an extensible and customizable framework for experimenting with new software verification techniques. The effectiveness and scalability of SeaHorn are demonstrated by an extensive experimental evaluation using benchmarks from SV-COMP 2015 and real avionics code.
Smarter Earth Science Data System
The explosive growth in Earth observational data in the recent decade demands a better method of interoperability across heterogeneous systems. The Earth science data system community has mastered the art in storing large volume of observational data, but it is still unclear how this traditional method scale over time as we are entering the age of Big Data. Indexed search solutions such as Apache Solr (Smiley and Pugh, 2011) provides fast, scalable search via keyword or phases without any reasoning or inference. The modern search solutions such as Googles Knowledge Graph (Singhal, 2012) and Microsoft Bing, all utilize semantic reasoning to improve its accuracy in searches. The Earth science user community is demanding for an intelligent solution to help them finding the right data for their researches. The Ontological System for Context Artifacts and Resources (OSCAR) (Huang et al., 2012), was created in response to the DARPA Adaptive Vehicle Make (AVM) programs need for an intelligent context models management system to empower its terrain simulation subsystem. The core component of OSCAR is the Environmental Context Ontology (ECO) is built using the Semantic Web for Earth and Environmental Terminology (SWEET) (Raskin and Pan, 2005). This paper presents the current data archival methodology within a NASA Earth science data centers and discuss using semantic web to improve the way we capture and serve data to our users.
The Behavior, Constraint, and Scenario (BeCoS) Tool: A Web-Based Software Application for Modeling Behaviors and Scenarios
The Behavior, Constraint, and Scenario (BeCoS) tool has been developed to allow engineers to specify system and component behaviors. The tool is a web application that is developed in JavaScript and uses the React framework for the user interface and Redux for maintaining application state. The foundation of the tool is its underlying ontology, which expands upon a previously-defined behavior ontology with a scenario ontology. The behavior ontology includes elements like behaving elements, state variables, parameters, and constraints, while the scenario ontology includes core constructs like activities, temporal constraints, and timepoints. BeCoS allows users to easily create behaving elements and to specify their state variables, parameters, state machines, and constraints. BeCoS also allows users to develop temporal constraint networks that specify constraints on component states over time. BeCoS is a prototype tool that has been deployed and tested by systems engineers on the Europa Clipper project, which generated several use cases and helped steer its current developmental effort. By enabling systems engineers to specify behavior in a semantically-rigorous manner, BeCoS is an enabling technology for analyses that previously could not be performed, and when exporting its model to other tools, allows for consistent behavior models to be used.
The Behavior, Constraint, and Scenario (BeCoS) Tool: A Web-Based Software Application for Modeling Behaviors and Scenarios
The Behavior, Constraint, and Scenario (BeCoS) tool has been developed to allow engineers to specify system and component behaviors. The tool is a web application that is developed in JavaScript and uses the React framework for the user interface and Redux for maintaining application state. The foundation of the tool is its underlying ontology, which expands upon a previously-defined behavior ontology with a scenario ontology. The behavior ontology includes elements like behaving elements, state variables, parameters, and constraints, while the scenario ontology includes core constructs like activities, temporal constraints, and timepoints. BeCoS allows users to easily create behaving elements and to specify their state variables, parameters, state machines, and constraints. BeCoS also allows users to develop temporal constraint networks that specify constraints on component states over time. BeCoS is a prototype tool that has been deployed and tested by systems engineers on the Europa Clipper project, which generated several use cases and helped steer its current developmental effort. By enabling systems engineers to specify behavior in a semantically-rigorous manner, BeCoS is an enabling technology for analyses that previously could not be performed, and when exporting its model to other tools, allows for consistent behavior models to be used.
Exposing Hidden Parts of the SE Process: MBSE Patterns and Tools for Tracking and Traceability
An interesting benefit of applying Model-Based Systems Engineering (MBSE) is that the rigor and coordination intrinsic to MBSE forces us to apply Systems Engineering to our own traditional activities, processes, and products, which results in richer, more expressive models, more powerful reasoning, and a clearer and more effective Systems Engineering (SE) process. Our MBSE frameworks and languages contain semantic richness sufficient to describe our systems at any particular point in time, often with an emphasis on the description of the system at major milestones. This is unarguably a real asset. However, when we apply MBSE in service of missions that are in development, rapidly evolving, of a larger scale, and where interpersonal communication is a critical part of the design process, we discover that our frameworks and languages are still not quite rich enough to enable us to ask the kinds of questions and get the kinds of answers we want in order to address the concerns of day to day work. This paper will discuss some patterns and tools we have developed to help address some of the not-always-explicit SE concerns that we have identified through our MBSE work. Particularly, this paper will discuss flexible yet practical methods for defining and capturing maturity, workflow, and agreement traceability within our system models, extensible ways to perform and track model audits, and ways to report and interact with this knowledge in the context of MBSE applied to support NASA’s Europa Project.
Exposing Hidden Parts of the SE Process: MBSE Patterns and Tools for Tracking and Traceability
An interesting benefit of applying Model-Based Systems Engineering (MBSE) is that the rigor and coordination intrinsic to MBSE forces us to apply Systems Engineering to our own traditional activities, processes, and products, which results in richer, more expressive models, more powerful reasoning, and a clearer and more effective Systems Engineering (SE) process. Our MBSE frameworks and languages contain semantic richness sufficient to describe our systems at any particular point in time, often with an emphasis on the description of the system at major milestones. This is unarguably a real asset. However, when we apply MBSE in service of missions that are in development, rapidly evolving, of a larger scale, and where interpersonal communication is a critical part of the design process, we discover that our frameworks and languages are still not quite rich enough to enable us to ask the kinds of questions and get the kinds of answers we want in order to address the concerns of day to day work. This paper will discuss some patterns and tools we have developed to help address some of the not-always-explicit SE concerns that we have identified through our MBSE work. Particularly, this paper will discuss flexible yet practical methods for defining and capturing maturity, workflow, and agreement traceability within our system models, extensible ways to perform and track model audits, and ways to report and interact with this knowledge in the context of MBSE applied to support NASA’s Europa Project
Ontology Development and Evolution in the Accident Investigation Domain
InvestiigationOrganizer (IO) is a collaborative semantic web system designed to support the conduct of mishap investigations. IO provides a common repository for a wide range of mishap related information, allowing investigators to integrate evidence, causal models, and investigation results. IO has been used to support investigations ranging from a small property damage case to the loss of the Space Shuttle Columbia. Through IO'S use in these investigations, we have learned significant lessons? about the application of ontologies and semantic systems to solving real-world problems. This paper will describe the development of the ontology within IO, from the initial development, its growth in response to user requests during use in investigations, and the recent work that was done to control the results of that growth. This paper will also describe the lessons learned from this experience and how they may apply to the implementaton of future ontologies and semantic systems.
Approximate reasoning using terminological models
Term Subsumption Systems (TSS) form a knowledge-representation scheme in AI that can express the defining characteristics of concepts through a formal language that has a well-defined semantics and incorporates a reasoning mechanism that can deduce whether one concept subsumes another. However, TSS's have very limited ability to deal with the issue of uncertainty in knowledge bases. The objective of this research is to address issues in combining approximate reasoning with term subsumption systems. To do this, we have extended an existing AI architecture (CLASP) that is built on the top of a term subsumption system (LOOM). First, the assertional component of LOOM has been extended for asserting and representing uncertain propositions. Second, we have extended the pattern matcher of CLASP for plausible rule-based inferences. Third, an approximate reasoning model has been added to facilitate various kinds of approximate reasoning. And finally, the issue of inconsistency in truth values due to inheritance is addressed using justification of those values. This architecture enhances the reasoning capabilities of expert systems by providing support for reasoning under uncertainty using knowledge captured in TSS. Also, as definitional knowledge is explicit and separate from heuristic knowledge for plausible inferences, the maintainability of expert systems could be improved.
A dual-task investigation of automaticity in visual word processing
An analysis of activation models of visual word processing suggests that frequency-sensitive forms of lexical processing should proceed normally while unattended. This hypothesis was tested by having participants perform a speeded pitch discrimination task followed by lexical decisions or word naming. As the stimulus onset asynchrony between the tasks was reduced, lexical-decision and naming latencies increased dramatically. Word-frequency effects were additive with the increase, indicating that frequency-sensitive processing was subject to postponement while attention was devoted to the other task. Either (a) the same neural hardware shares responsibility for lexical processing and central stages of choice reaction time task processing and cannot perform both computations simultaneously, or (b) lexical processing is blocked in order to optimize performance on the pitch discrimination task. Either way, word processing is not as automatic as activation models suggest.
Climate Model Diagnostic Analyzer
The comprehensive and innovative evaluation of climate models with newly available global observations is critically needed for the improvement of climate model current-state representation and future-state predictability. A climate model diagnostic evaluation process requires physics-based multi-variable analyses that typically involve large-volume and heterogeneous datasets, making them both computation- and data-intensive. With an exploratory nature of climate data analyses and an explosive growth of datasets and service tools, scientists are struggling to keep track of their datasets, tools, and execution/study history, let alone sharing them with others. In response, we have developed a cloud-enabled, provenance-supported, web-service system called Climate Model Diagnostic Analyzer (CMDA). CMDA enables the physics-based, multivariable model performance evaluations and diagnoses through the comprehensive and synergistic use of multiple observational data, reanalysis data, and model outputs. At the same time, CMDA provides a crowd-sourcing space where scientists can organize their work efficiently and share their work with others. CMDA is empowered by many current state-of-the-art software packages in web service, provenance, and semantic search.
Investigating Interruptions: Implications for Flightdeck Performance
A fundamental aspect of multiple task management is attending to new stimuli and integrating associated task requirements into an ongoing task set; this is "interruption management" (IM). Anecdotal evidence and field studies indicate the frequency and consequences of interruptions, however experimental investigations of mechanisms influencing IM are scarce. Interruptions on commercial flightdecks are numerous, of various forms, and have been cited as contributing factors in many aviation incident and accident reports. This research grounds an experimental investigation of flightdeck interruptions in a proposed IM stage model. This model organizes basic research, identifies influencing mechanisms, and suggests appropriate dependent measures for IM. Fourteen airline pilots participated in a flightdeck simulation experiment to investigate the general effects of performing an interrupting task and interrupted procedure, and the effects of specific task factors: (1) modality; (2) embeddedness, or goal-level, of an interruption; (3) strength of association, or coupling-strength, between interrupted tasks; (4) semantic similarity; and (5) environmental stress. General effects of interruptions were extremely robust. All individual task factors significantly affected interruption management, except "similarity." Results extend the Interruption Management model, and are interpreted for their implications for interrupted flightdeck performance and intervention strategies for mitigating their effects on the flightdeck.
Simulation and Verification of Synchronous Set Relations in Rewriting Logic
This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property veri cation of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm veri cation techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the veri cation of temporal properties of a synchronous system.
NASA's ATM Ontology: Semantic Integration and Querying Across NAS Data Sources
NASA is developing an Air Traffic Management (ATM) Ontology as part of an advanced prototyping activity that demonstrates the utility of semantic technologies for integrating, querying, and searching over various sources of heterogeneous ATM data. The ontology encodes an overarching data model that functions as the backbone upon which to overlay data from multiple sources published by FAA, NOAA, NASA, and others. The integrated data can be queried to produce results not achievable using any single source alone. The ontology incorporates flight data, weather data, traffic management advisory data, airport delay data, and national airspace infrastructure data for a very limited spatial and temporal slice of airspace operations (one day of operations at a major airport).
Formal Methods in the Development of Highly Assured Software for Unmanned Aircraft Systems
In traditional software development methodologies, operational and functional requirements of systems are often specified in structured natural language notations. These restricted notations provide good documentation support, but only provide limited support for semantic analysis. These notations are generally not rich enough to unambiguously specify the requirements of safety-critical systems that, for example, involve complex numerical computations or that interact with the physical environment. Examples of these safety-critical systems are autonomous vehicles such as unmanned aircraft systems. This talk advocates the use of expressive formal logics, such as higher-order logic, to specify the operational and functional requirement of unmanned systems and to prove the correctness of these requirements. Semantic analysis of requirements written in higher-order logic is supported through the use of interactive theorem provers. Formal models serve as ideal reference implementations of functional requirements. Hence, formal logics enable software validation techniques where software implementations can be checked against functional requirements in a mechanical way. The Formal Methods group in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center has conducted research on the development and application of formal verification techniques to safety-critical applications of interest to NASA for more than 30 years. This talk illustrates the use of formal methods in the development of highly-assured autonomous unmanned aircraft systems.
The semantics of fuzzy logic
Summarized here are the results of recent research on the conceptual foundations of fuzzy logic. The focus is primarily on the principle characteristics of a model that quantifies resemblance between possible worlds by means of a similarity function that assigns a number between 0 and 1 to every pair of possible worlds. Introduction of such a function permits one to interpret the major constructs and methods of fuzzy logic: conditional and unconditional possibility and necessity distributions and the generalized modus ponens of Zadeh on the basis of related metric relationships between subsets of possible worlds.
The AutoBayes Program Synthesis System: System Description
AUTOBAYES is a fully automatic program synthesis system for the statistical data analysis domain. Its input is a concise description of a data analysis problem in the form of a statistical model; its output is optimized and fully documented C/C++ code which can be linked dynamically into the Matlab and Octave environments. AUTOBAYES synthesizes code by a schema-guided deductive process. Schemas (i.e., code templates with associated semantic constraints) are applied to the original problem and recursively to emerging subproblems. AUTOBAYES complements this approach by symbolic computation to derive closed-form solutions whenever possible. In this paper, we concentrate on the interaction between the symbolic computations and the deductive synthesis process. A statistical model specifies for each problem variable (i.e., data or parameter) its properties and dependencies in the form of a probability distribution, A typical data analysis task is to estimate the best possible parameter values from the given observations or measurements. The following example models normal-distributed data but takes prior information (e.g., from previous experiments) on the data's mean value and variance into account.