Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “formal”

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 415 records · Page 23
All sourcesNASA NTRSDOE OSTI
NASA NTRS2002

Using a Formal Approach for Reverse Engineering and Design Recovery to Support Software Reuse

This document describes 3rd year accomplishments and summarizes overall project accomplishments. Included as attachments are all published papers from year three. Note that the budget for this project was discontinued after year two, but that a residual budget from year two allowed minimal continuance into year three. Accomplishments include initial investigations into log-file based reverse engineering, service-based software reuse, and a source to XML generator.

Gannod, Gerald C.↗
NASA NTRS2003

Practical Formal Verification of Diagnosability of Large Models via Symbolic Model Checking

This document reports on the activities carried out during a four-week visit of Roberto Cavada at the NASA Ames Research Center. The main goal was to test the practical applicability of the framework proposed, where a diagnosability problem is reduced to a Symbolic Model Checking problem. Section 2 contains a brief explanation of major techniques currently used in Symbolic Model Checking, and how these techniques can be tuned in order to obtain good performances when using Model Checking tools. Diagnosability is performed on large and structured models of real plants. Section 3 describes how these plants are modeled, and how models can be simplified to improve the performance of Symbolic Model Checkers. Section 4 reports scalability results. Three test cases are briefly presented, and several parameters and techniques have been applied on those test cases in order to produce comparison tables. Furthermore, comparison between several Model Checkers is reported. Section 5 summarizes the application of diagnosability verification to a real application. Several properties have been tested, and results have been highlighted. Finally, section 6 draws some conclusions, and outlines future lines of research.

Cavada, Roberto↗
NASA NTRS2003

Mars: Updating Geologic Mapping Approaches and the Formal Stratigraphic Scheme

At the Fourth Mars Conference in 1989, Tanaka reviewed the stratigraphy and geologic history of Mars that had emerged based on systematic geologic mapping of the planet s surface using Viking data. This review looked at the stratigraphic column for Mars and assessed the global geologic history in terms of impact, fluvial, periglacial, aeolian, volcanic, and tectonic processes. Many significant new studies using Mars Global Surveyor (MGS) and now Mars Odyssey (MO) data are showing some important new insights and discoveries that are altering and deepening previous understandings. If we were to illustrate the current state of the science, we might compare it to a loose-leaf notebook in which pages are rapidly being added, removed, and rewritten, with plenty of room remaining. Much of the flux is due to new data, of course, but also much can be attributed to the re-examination of basic assumptions and approaches and our ability to employ ever more powerful computer techniques. Here, we will attempt to review, based on our experience, the areas where the most change seems to be occurring, what prospects we face in the immediate future, and where caution needs to be exercised.

K L Tanaka↗
NASA NTRS2004

Formalism Challenges of the Cougaar Model Driven Architecture

The Cognitive Agent Architecture (Cougaar) is one of the most sophisticated distributed agent architectures developed today. As part of its research and evolution, Cougaar is being studied for application to large, logistics-based applications for the Department of Defense (DoD). Anticipiting future complex applications of Cougaar, we are investigating the Model Driven Architecture (MDA) approach to understand how effective it would be for increasing productivity in Cougar-based development efforts. Recognizing the sophistication of the Cougaar development environment and the limitations of transformation technologies for agents, we have systematically developed an approach that combines component assembly in the large and transformation in the small. This paper describes some of the key elements that went into the Cougaar Model Driven Architecture approach and the characteristics that drove the approach.

Bohner, Shawn A.↗
NASA NTRS2004

Formal Consistency Verification of Deliberative Agents with Respect to Communication Protocols

The aim of this paper is to show a method that is able to detect inconsistencies in the reasoning carried out by a deliberative agent. The agent is supposed to be provided with a hybrid Knowledge Base expressed in a language called CCR-2, based on production rules and hierarchies of frames, which permits the representation of non-monotonic reasoning, uncertain reasoning and arithmetic constraints in the rules. The method can give a specification of the scenarios in which the agent would deduce an inconsistency. We define a scenario to be a description of the initial agent s state (in the agent life cycle), a deductive tree of rule firings, and a partially ordered set of messages and/or stimuli that the agent must receive from other agents and/or the environment. Moreover, the method will make sure that the scenarios will be valid w.r.t. the communication protocols in which the agent is involved.

Ramirez, Jaime↗
NASA NTRS2004

Formal Verification of Safety Properties for Aerospace Systems Through Algorithms Based on Exhaustive State-Space Exploration

The Runway Safety Monitor (RSM) designed by Lockheed Martin is part of NASA's effort to reduce aviation accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool SMART to investigate a number of safety properties in RSM. To mitigate the impact of state-space explosion, we built a highly discretized model of the system, obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the RSM conceptual design. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with NuSMV and SPIN have failed due to excessive memory consumption.

Ciardo, Gianfranco↗
NASA NTRS2006

Formal Verification of the Runway Safety Monitor

The Runway Safety Monitor (RSM) designed by Lockheed Martin is part of NASA's effort to reduce runway accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool SMART to investigate a number of safety properties in RSM. To mitigate the impact of state-space explosion, we built a highly discretized model of the system, obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the RSM conceptual design. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems.

Siminiceanu, Radu↗
NASA NTRS2002

Oceanography in the formal and informal classroom

The TOPEX/Poseidon and Jason-1 ocean altimeter missions offer the educator in the middle school or informal education venue a unique opportunity for reinforcing ocean science studies. An educational poster from NASA's Jet Propulsion Laboratory and France's Centre National d'Etudes Spatiales provide teachers and students a tool to examine topics such as the dynamics of ocean circulation, ocean research, and the oceans' role in climate.

TOPEX Jason oceanography education↗
NASA NTRS1993

Formal Functional Test Designs: Bridging the Gap Between Test Requirements and Test Specifications

This presentation describes the testing life cycle, the purpose of the test design phase, and test design methods and gives an example application. Also included is a description of Test Representation Language (TRL), a summary of the language, and an example of an application of TRL. A sample test requirement and sample test design are included.

testing life cycle test design test requirements T↗