Special Coverage

Home

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.

Posted in: Briefs, TSP

Read More >>

Routines for Computing Pressure Drops in Venturis

A set of computer- program routines has been developed for calculating pressure drops and recoveries of flows through standard venturis, nozzle venturis, and orifices. Relative to prior methods used for such calculations, the method implemented by these routines offers greater accuracy because it involves fewer simplifying assumptions and is more generally applicable to wide ranges of flow conditions. These routines are based on conservation of momentum and energy equations for real nonideal fluids, the properties of which are calculated by curve-fitting subroutines based on empirical properties data. These routines are capable of representing cavitating, choked, non-cavitating, and unchoked flow conditions for liquids, gases, and supercritical fluids. For a computation of flow through a given venturi, nozzle venturi, or orifice, the routines determine which flow condition occurs: First, they calculate a throat pressure under the assumption that the flow is unchoked or non-cavitating, then they calculate the throat pressure under the assumption that the flow is choked or cavitating. The assumption that yields the higher throat pressure is selected as the correct one.

Posted in: Briefs

Read More >>

Software for Fault-Tolerant Matrix Multiplication

Formal Linear Algebra Recovery Environment is a computer program for high-performance, fault-tolerant matrix multiplication. The program is based on an extension of the prior theory and practice of fault-tolerant matrix·matrix multiplication of the form C = AB. This extension provides low-overhead methods for detecting errors, not only in C, but also in A and/or B. These methods enable the detection of all errors as long as, in a given case, only one entry in A, B, or C is corrupted. The program also provides for following a low-overhead roll-back approach to correct errors once detected. Results of computational experiments have demonstrated that the methods implemented in this program work well in practice while imposing an acceptably low level of overhead, relative to high-performance matrix-multiplication methods that do not afford fault tolerance.

Posted in: Software, Briefs, TSP

Read More >>

Updated System-Availibility and Resource-Allocation Program

A second version of the Availability, Cost and Resource Allocation (ACARA) computer program has become available. The first version was reported in "System-Availability and Resource- Allocation Program" (LEW-15713), NASA Tech Briefs, Vol. 19, No. 8 (August 1995), page 54. To recapitulate: ACARA analyzes the availability, mean-time-between- failures of components, life-cycle costs, and scheduling of resources of a complex system of equipment. ACARA uses a statistical Monte Carlo method to simulate the failure and repair of components while complying with user-specified constraints on spare parts and resources. ACARA evaluates the performance of the system on the basis of a mathematical model developed from a block-diagram representation. The previous version utilized the MS-DOS operating system and could not be run by use of the most recent versions of the Windows operating system. The current version incorporates the algorithms of the previous version but is compatible with Windows and utilizes menus and a file-management approach typical of Windows-based software.

Posted in: Briefs, TSP

Read More >>

Simulation Testing of Embedded Flight Software

Virtual Real Time (VRT) is a computer program for testing embedded flight software by computational simulation in a workstation, in contradistinction to testing it in its target central processing unit (CPU). The disadvantages of testing in the target CPU include the need for an expensive test bed, the necessity for testers and programmers to take turns using the test bed, and the lack of software tools for debugging in a real-time environment. By virtue of its architecture, most of the flight software of the type in question is amenable to development and testing on workstations, for which there is an abundance of commercially available debugging and analysis software tools. Unfortunately, the timing of a workstation differs from that of a target CPU in a test bed. VRT, in conjunction with closed-loop simulation software, provides a capability for executing embedded flight software on a workstation in a close-to-real-time environment. A scale factor is used to convert between execution time in VRT on a workstation and execution on a target CPU. VRT includes high-resolution operating-system timers that enable the synchronization of flight software with simulation software and ground software, all running on different workstations.

Posted in: Briefs, TSP

Read More >>

Software for Analyzing Laminar-to-Turbulent Flow Transitions

Langley Stability and Transition Analysis Codes (LASTRAC) is a set of engineering software tools developed with the C++ language and modern software technologies for use in analyzing transition from laminar to turbulent flows. LASTRAC is a product of on-going NASA Langley research projects related to transition flow physics modeling and simulations. It is intended to be a set of easy-to-use engineering tools that can be applied to routine engineering design studies. At the current stage, LASTRAC is capable of performing transition calculations based on linear stability theory (LST) or linear and nonlinear parabolized stability equations (PSE) for a broad range of flow regimes and configurations of interest for the design of low-speed as well as supersonic and hypersonic vehicles. At present, LASTRAC is limited to two-dimensional, axisymmetric, or infinite swept-wing boundary layers. Options for general three-dimensional boundary layers are currently under development. The LST option makes it possible to perform traditional N-factor transition correlation. Linear and nonlinear PSE are used to track instability wave evolution from small-amplitude till early transition stage in a high-fidelity manner. It is planned to incorporate modules in LASTRAC that models the receptivity (the process by which perturbations are introduced into laminar boundary-layer flow) and late stage of the transition process. These software modules are intended to enable LASTRAC to perform computations for different stages of laminar-to-turbulent transition in an integrated fashion.

Posted in: Briefs, TSP

Read More >>

The TechSat 21 Autonomous Sciencecraft Experiment

Software has been developed to perform a number of functions essential to autonomous operation in the Autonomous Sciencecraft Experiment (ASE), which is scheduled to be demonstrated aboard a constellation of three spacecraft, denoted TechSat 21, to be launched by the Air Force into orbit around the Earth in January 2006. A prior version of this software was reported in "Software for an Autonomous Constellation of Satellites" (NPO-30355), NASA Tech Briefs, Vol. 26, No. 11 (November 2002), page 44.

Posted in: Briefs, TSP

Read More >>