Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “spin 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.

At least 37 records · Page 2
All sourcesNASA NTRSDOE OSTI
NASA NTRS2018

Modeling with Scala

The activities and the associated formalisms for modeling and programming have many commonalities. In this paper we emphasize this point of view by modeling two examples in the programming language Scala, which have previously been modeled in the VDM specification language, and the Promela modeling language of the SPIN model checker respectively. The latter Scala model uses an internal DSL for hierarchical state machines, and a simple randomized testing framework exposing the same errors as found with SPIN. We believe, as the examples illustrate, that this use of a modern programming language for modeling is promising, especially if utilizing internal DSLs.

Joshi, Rajeev↗
NASA NTRS1999

Java PathFinder: A Translator From Java to Promela

JAVA PATHFINDER, JPF, is a prototype translator from JAVA to PROMELA, the modeling language of the SPIN model checker. JPF is a product of a major effort by the Automated Software Engineering group at NASA Ames to make model checking technology part of the software process. Experience has shown that severe bugs can be found in final code using this technique, and that automated translation from a programming language to a modeling language like PROMELA can help reducing the effort required.

Havelund, Klaus↗
NASA NTRS2016

Improved Analysis of GW150914 Using a Fully Spin-Precessing Waveform Model

This paper presents updated estimates of source parameters for GW150914, a binary black-hole coalescence event detected by the Laser Interferometer Gravitational-wave Observatory (LIGO) in 2015 [Abbott et al. Phys. Rev. Lett. 116, 061102 (2016).]. Abbott et al. [Phys. Rev. Lett. 116, 241102 (2016).] presented parameter estimation of the source using a 13-dimensional, phenomenological precessing-spin model (precessing IMRPhenom) and an 11-dimensional nonprecessing effective-one-body (EOB) model calibrated to numerical-relativity simulations, which forces spin alignment (nonprecessing EOBNR). Here, we present new results that include a 15-dimensional precessing-spin waveform model (precessing EOBNR) developed within the EOB formalism. We find good agreement with the parameters estimated previously [Abbott et al. Phys. Rev. Lett. 116, 241102 (2016).], and we quote updated component masses of 35(+5)(-3) solar M; and 30(+3)(-4) solar M; (where errors correspond to 90 symmetric credible intervals). We also present slightly tighter constraints on the dimensionless spin magnitudes of the two black holes, with a primary spin estimate is less than 0.65 and a secondary spin estimate is less than 0.75 at 90% probability. Abbott et al. [Phys. Rev. Lett. 116, 241102 (2016).] estimated the systematic parameter-extraction errors due to waveform-model uncertainty by combining the posterior probability densities of precessing IMRPhenom and nonprecessing EOBNR. Here, we find that the two precessing-spin models are in closer agreement, suggesting that these systematic errors are smaller than previously quoted.

Abbott, B. P.↗
NASA NTRS2004

Verifying AI Plan Models: Even the Best Laid Plans Need to be Verified

This viewgraph presentation reviews work on model checking, and specifically the SPIN model checker. The goal of this work is to retire a significant class of risks associated with the use of Artificial Intelligence (Al) Planners on Missions. This effort must provide tangible testing results to a mission using Al technology. It is hoped that the work should be possible to leverage the technique and tools throughout NASA

artificial intelligence↗
NASA NTRS1983

Magnus effects on spinning transonic missiles

Magnus forces and moments were measured on a basic-finner model spinning in transonic flow. Spin was induced by canted fins or by full-span or semi-span, outboard and inboard roll controls. Magnus force and moment reversals were caused by Mach number, reduced spin rate, and angle of attack variations. Magnus center of pressure was found to be independent of the angle of attack but varied with the Mach number and model configuration or reduced spin rate.

Seginer, A.↗
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 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 NTRS2005

Application of Lightweight Formal Methods to Software Security

Formal specification and verification of security has proven a challenging task. There is no single method that has proven feasible. Instead, an integrated approach which combines several formal techniques can increase the confidence in the verification of software security properties. Such an approach which species security properties in a library that can be reused by 2 instruments and their methodologies developed for the National Aeronautics and Space Administration (NASA) at the Jet Propulsion Laboratory (JPL) are described herein The Flexible Modeling Framework (FMF) is a model based verijkation instrument that uses Promela and the SPIN model checker. The Property Based Tester (PBT) uses TASPEC and a Text Execution Monitor (TEM). They are used to reduce vulnerabilities and unwanted exposures in software during the development and maintenance life cycles.

security↗
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 NTRS2000

Model Checking JAVA Programs Using Java Pathfinder

This paper describes a translator called JAVA PATHFINDER from JAVA to PROMELA, the "programming language" of the SPIN model checker. The purpose is to establish a framework for verification and debugging of JAVA programs based on model checking. This work should be seen in a broader attempt to make formal methods applicable "in the loop" of programming within NASA's areas such as space, aviation, and robotics. Our main goal is to create automated formal methods such that programmers themselves can apply these in their daily work (in the loop) without the need for specialists to manually reformulate a program into a different notation in order to analyze the program. This work is a continuation of an effort to formally verify, using SPIN, a multi-threaded operating system programmed in Lisp for the Deep-Space 1 spacecraft, and of previous work in applying existing model checkers and theorem provers to real applications.

Havelund, Klaus↗
NASA NTRS1986

Low-speed aerodynamic characteristics of a 1/8-scale X-29A airplane model at high angles of attack and sideslip

A 1/8-scale model of the X-29A airplane was tested in the Ames 12-Foot Pressure Wind Tunnel at a Mach number of 0.20 and Reynolds numbers of 0.13 x 10 to the 6th power to 2.00 x 10 to the 6th power based on a fuselage forebody depth of 0.4 ft, For the test series presented herein, the angle of attack ranged from 40 deg. to 90 deg. and the angle of sideslip ranged from -10 deg. to 30 deg. for the erect attitude. Tests with the model inverted covered angles of attack from -40 deg. to -90 deg. and angles of sideslip from -30 deg. to 10 deg. Data were obtained for the basic design and for several forebody strakes. An alternate forebody design was also tested. The results provided information for selection of forebody strakes for compensation of Reynolds number effect on the 1/25-scale free-spinning model tested in the Langley Spin Tunnel.

Whipple, R. D.↗
NASA NTRS2003

The HiVy toolset

The HiVy toolset provides model checking for statecharts. This is achieved by translating statechart specifications into the input language of the spin model checker.

model checking statechart translation validation↗
NASA NTRS1951

Pilot Escape from Spinning Airplanes as Determined from Free-spinning-tunnel Tests

Procedure for pilot escape from spinning airplanes has been determined by means of tests in which pilot escape was simulated from 21 airplane models spinning in the Langley 20-foot free-spinning tunnel. The results in general indicated that the pilot should bail out of the outboard side. Calculated centripetal accelerations acting on the pilot during a spin are presented.

SAFETY - PILOT ESCAPE TECHNIQUES↗
NASA NTRS2000

Formal Analysis of the Remote Agent Before and After Flight

This paper describes two separate efforts that used the SPIN model checker to verify deep space autonomy flight software. The first effort occurred at the beginning of a spiral development process and found five concurrency errors early in the design cycle that the developers acknowledge would not have been found through testing. This effort required a substantial manual modeling effort involving both abstraction and translation from the prototype LISP code to the PROMELA language used by SPIN. This experience and others led to research to address the gap between formal method tools and the development cycle used by software developers. The Java PathFinder tool which directly translates from Java to PROMELA was developed as part of this research, as well as automatic abstraction tools. In 1999 the flight software flew on a space mission, and a deadlock occurred in a sibling subsystem to the one which was the focus of the first verification effort. A second quick-response "cleanroom" verification effort found the concurrency error in a short amount of time. The error was isomorphic to one of the concurrency errors found during the first verification effort. The paper demonstrates that formal methods tools can find concurrency errors that indeed lead to loss of spacecraft functions, even for the complex software required for autonomy. Second, it describes progress in automatic translation and abstraction that eventually will enable formal methods tools to be inserted directly into the aerospace software development cycle.

Havelund, Klaus↗