Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “custom software”

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 667 records · Page 37
All sourcesNASA NTRSDOE OSTI
NASA NTRS1994

A Custom Robotic System for Inspecting HEPA Filters in the Payload Changeout Room at the NASA Kennedy Space Center

In this paper, the prime objective is to describe a custom 4-dof (degree-of-freedom) robotic arm capable of autonomously or telerobotically performing systematic HEPA filter inspection and certification in the Shuttle Launch Pad Payload Changeout Rooms (PCR's) on pads A and B at the Kennedy Space Center, Florida. This HEPA filter inspection robot (HFIR) has been designed to be easily deployable and is equipped with the necessary sensory devices, control hardware, software and man-machine interfaces needed to implement HEPA filter inspection reliably and efficiently without damaging the filters or colliding with existing PCR structures or filters. The main purpose of the HFIR is to implement an automated positioning system to move special inspection sensors in pre-defined or manual patterns for the purpose of verifying filter integrity and efficiency. This will ultimately relieve NASA Payload Operations from significant problems associated with time, cost and personnel safety, impacts realized during non-automated PCR HFIR filter certification.

Spencer, James E., Jr.↗
NASA NTRS2002

Optical Testing of Diamond Machined, Aspheric Mirrors for Groundbased, Near-IR Astronomy

The Infrared Multi-Object Spectrometer (IRMOS) is a facility-class instrument for the Kitt Peak National Observatory 4 and 2.1 meter telescopes. IRMOS is a near-IR (0.8-2.5 micron) spectrometer and operates at approximately 80 K. The 6061-T651 aluminum bench and mirrors constitute an athermal design. The instrument produces simultaneous spectra at low- to mid-resolving power (R=lambda/delta lambda= 300-3000) of approximately 100 objects in its 2.8 x 2.0 arcmin field. We describe ambient and cryogenic optical testing of the IRMOS mirrors across a broad range in spatial frequency (figure error, mid-frequency error, and microroughness). The mirrors include three rotationally symmetric, off-axis conic sections, one off-axis biconic, and several flat fold mirrors. The symmetric mirrors include convex and concave prolate and oblate ellipsoids. They range in aperture from 94x86 mm to 286x269 mm and in f-number from 0.9 to 2.4. The biconic mirror is concave and has a 94x76 mm aperture, R(sub x)=377 mm, k(sub x)=0.0778, R(sub y)=407 mm, and k(sub y)=0.1265 and is decentered by -2 mm in X and 227 mm in Y. All of the mirrors have an aspect ratio of approximately 6:1. The surface error fabrication tolerances are less than 10 nm RMS microroughness, 'best effort' for mid-frequency error, and less than 63.3 nm RMS figure error. Ambient temperature (approximately 293 K) testing is performed for each of the three surface error regimes, and figure testing is also performed at approximately 80 K. Operation of the ADE Phaseshift MicroXAM white light interferometer (micro-roughness) and the Bauer Model 200 profilometer (mid-frequency error) is described. Both the sag and conic values of the aspheric mirrors make these tests challenging. Figure testing is performed using a Zygo GPI interferometer, custom computer generated holograms (CGH), and optomechanical alignment fiducials. Cryogenic CGH null testing is discussed in detail. We discuss complications such as the change in prescription with temperature and thermal gradients. Correction for the effect of the dewar window is also covered. We discuss the error budget for the optical test and alignment procedure. Data reduction is accomplished using commercial optical design and data analysis software packages. Results from CGH testing at cryogenic temperatures are encouraging thus far.

Chambers, V. John↗
NASA NTRSDate not supplied

MOC Automation with GMSEC and the Generic Extendable Message Utility (GEMU)

Automation has become critical for ground systems, improving efficiency and reliability while reducing costs across mission operations. The Goddard Mission Services Evolution Center (GMSEC) software suite has played a significant role in enabling this automation, leveraging its publish/subscribe paradigm through a message bus architecture to facilitate seamless communication and data flow. Historically, the GMSEC suite, through components like Criteria Action Table (CAT) has been pivotal in automating ground system capabilities. However, as technology advances, limitations in automation with CAT have emerged, creating an opportunity to enhance ground system automation through the introduction of GEMU. This new GMSEC component brings new capabilities and addresses specific automation constraints that CAT could not overcome, allowing for more sophisticated, flexible, and efficient message processing. GEMU, at its core, is designed to accelerate the development of custom GMSEC-compliant applications. It enables users to construct automated message processing pipelines quickly, supporting both drag-and-drop web-based configuration and scripting through a simple domain-specific language. This advancement not only simplifies the process but also reduces the time needed for implementing automated solutions. This presentation will outline GEMU’s potential value in improving mission operations automation. It will highlight the benefits of transitioning from CAT to GEMU and offer insights into how GEMU can drive operational efficiencies. We will also provide an overview of the automation capabilities of GEMU and its potential impact on mission operations centers (MOCs).

GMSEC↗
NASA NTRS1984

Hardware for a real-time multiprocessor simulator

The hardware for a real time multiprocessor simulator (RTMPS) developed at the NASA Lewis Research Center is described. The RTMPS is a multiple microprocessor system used to investigate the application of parallel processing concepts to real time simulation. It is designed to provide flexible data exchange paths between processors by using off the shelf microcomputer boards and minimal customized interfacing. A dedicated operator interface allows easy setup of the simulator and quick interpreting of simulation data. Simulations for the RTMPS are coded in a NASA designed real time multiprocessor language (RTMPL). This language is high level and geared to the multiprocessor environment. A real time multiprocessor operating system (RTMPOS) has also been developed that provides a user friendly operator interface. The RTMPS and supporting software are currently operational and are being evaluated at Lewis. The results of this evaluation will be used to specify the design of an optimized parallel processing system for real time simulation of dynamic systems.

Blech, R. A.↗
NASA NTRS2011

Test Generator for MATLAB Simulations

MATLAB Automated Test Tool, version 3.0 (MATT 3.0) is a software package that provides automated tools that reduce the time needed for extensive testing of simulation models that have been constructed in the MATLAB programming language by use of the Simulink and Real-Time Workshop programs. MATT 3.0 runs on top of the MATLAB engine application-program interface to communicate with the Simulink engine. MATT 3.0 automatically generates source code from the models, generates custom input data for testing both the models and the source code, and generates graphs and other presentations that facilitate comparison of the outputs of the models and the source code for the same input data. Context-sensitive and fully searchable help is provided in HyperText Markup Language (HTML) format.

Henry, Joel↗
NASA NTRS1990

Development of a quadrupole-based Secondary-Ion Mass Spectrometry (SIMS) system at Lewis Research Center

The design, construction, and initial use of an ion microprobe to carry out secondary ion mass spectrometry (SIMS) of solid samples is reported. The system is composed of a differentially pumped custom-made UHV (Ultra High Vacuum) chamber, a quadrupole mass spectrometer and a telefocus A-DIDA ion gun with the capability of producing beams of Cesium, as well as inert and reactive gases. The computer control and acquisition of the data were designed and implemented using a personal computer with plug-in boards, and external circuitry built as required to suit the system needs. The software is being developed by using a FORTH-like language. Initial tests aimed at characterizing the system, as well as preliminary surface and depth-profiling studies are presently underway.

Vargas-Aburto, Carlos↗
NASA NTRS2013

Enigma Version 12

Enigma Version 12 software combines model building, animation, and engineering visualization into one concise software package. Enigma employs a versatile user interface to allow average users access to even the most complex pieces of the application. Using Enigma eliminates the need to buy and learn several software packages to create an engineering visualization. Models can be created and/or modified within Enigma down to the polygon level. Textures and materials can be applied for additional realism. Within Enigma, these models can be combined to create systems of models that have a hierarchical relationship to one another, such as a robotic arm. Then these systems can be animated within the program or controlled by an external application programming interface (API). In addition, Enigma provides the ability to use plug-ins. Plugins allow the user to create custom code for a specific application and access the Enigma model and system data, but still use the Enigma drawing functionality. CAD files can be imported into Enigma and combined to create systems of computer graphics models that can be manipulated with constraints. An API is available so that an engineer can write a simulation and drive the computer graphics models with no knowledge of computer graphics. An animation editor allows an engineer to set up sequences of animations generated by simulations or by conceptual trajectories in order to record these to highquality media for presentation. Enigma Version 12 Lyndon B. Johnson Space Center, Houston, Texas 28 NASA Tech Briefs, September 2013 Planetary Protection Bioburden Analysis Program NASA's Jet Propulsion Laboratory, Pasadena, California This program is a Microsoft Access program that performed statistical analysis of the colony counts from assays performed on the Mars Science Laboratory (MSL) spacecraft to determine the bioburden density, 3-sigma biodensity, and the total bioburdens required for the MSL prelaunch reports. It also contains numerous tools that report the data in various ways to simplify the reports required. The program performs all the calculations directly in the MS Access program. Prior to this development, the data was exported to large Excel files that had to be cut and pasted to provide the desired results. The program contains a main menu and a number of submenus. Analyses can be performed by using either all the assays, or only the accountable assays that will be used in the final analysis. There are three options on the first menu: either calculate using (1) the old MER (Mars Exploration Rover) statistics, (2) the MSL statistics for all the assays, or This software implements penetration limit equations for common micrometeoroid and orbital debris (MMOD) shield configurations, windows, and thermal protection systems. Allowable MMOD risk is formulated in terms of the probability of penetration (PNP) of the spacecraft pressure hull. For calculating the risk, spacecraft geometry models, mission profiles, debris environment models, and penetration limit equations for installed shielding configurations are required. Risk assessment software such as NASA's BUMPERII is used to calculate mission PNP; however, they are unsuitable for use in shield design and preliminary analysis studies. The software defines a single equation for the design and performance evaluation of common MMOD shielding configurations, windows, and thermal protection systems, along with a description of their validity range and guidelines for their application. Recommendations are based on preliminary reviews of fundamental assumptions, and accuracy in predicting experimental impact test results. The software is programmed in Visual Basic for Applications for installation as a simple add-in for Microsoft Excel. The user is directed to a graphical user interface (GUI) that requires user inputs and provides solutions directly in Microsoft Excel workbooks. This work was done by Shannon Ryan of the USRA Lunar and Planetary Institute for Johnson Space Center. Further information is contained in a TSP (see page 1). MSC- 24582-1 Micrometeoroid and Orbital Debris (MMOD) Shield Ballistic Limit Analysis Program Lyndon B. Johnson Space Center, Houston, Texas Commercially, because it is so generic, Enigma can be used for almost any project that requires engineering visualization, model building, or animation. Models in Enigma can be exported to many other formats for use in other applications as well. Educationally, Enigma is being used to allow university students to visualize robotic algorithms in a simulation mode before using them with actual hardware.

Shores, David↗
NASA NTRS2003

Robonaut's Flexible Information Technology Infrastructure

Robonaut, NASA's humanoid robot, is designed to work as both an astronaut assistant and, in certain situations, an astronaut surrogate. This highly dexterous robot performs complex tasks under telepresence control that could previously only be carried out directly by humans. Currently with 47 degrees of freedom (DOF), Robonaut is a state-of-the-art human size telemanipulator system. while many of Robonaut's embedded components have been custom designed to meet packaging or environmental requirements, the primary computing systems used in Robonaut are currently commercial-off-the-shelf (COTS) products which have some correlation to flight qualified computer systems. This loose coupling of information technology (IT) resources allows Robonaut to exploit cost effective solutions while floating the technology base to take advantage of the rapid pace of IT advances. These IT systems utilize a software development environment, which is both compatible with COTS hardware as well as flight proven computing systems, preserving the majority of software development for a flight system. The ability to use highly integrated and flexible COTS software development tools improves productivity while minimizing redesign for a space flight system. Further, the flexibility of Robonaut's software and communication architecture has allowed it to become a widely used distributed development testbed for integrating new capabilities and furthering experimental research.

Askew, Scott↗
NASA NTRS2006

Correction for Thermal EMFs in Thermocouple Feedthroughs

A straightforward measurement technique provides for correction of thermal-electromotive-force (thermal-EMF) errors introduced by temperature gradients along the pins of non-thermocouple-alloy hermetic feedthrough connectors for thermocouple extension wires that must pass through bulkheads. This technique is an alternative to the traditional technique in which the thermal-EMF errors are eliminated by use of custom-made multipin hermetic feedthrough connectors that contain pins made of the same alloys as those of the thermocouple extension wires. One disadvantage of the traditional technique is that it is expensive and time-consuming to fabricate multipin custom thermocouple connectors. In addition, the thermocouple-alloy pins in these connectors tend to corrode easily and/or tend to be less rugged compared to the non-thermocouple-alloy pins of ordinary connectors. As the number of thermocouples (and thus pins) is increased in a given setup, the magnitude of these disadvantages increases accordingly. The present technique is implemented by means of a little additional hardware and software, the cost of which is more than offset by the savings incurred through the use of ordinary instead of thermocouple connectors. The figure schematically depicts a typical measurement setup to which the technique is applied. The additional hardware includes an isothermal block (made of copper) instrumented with a reference thermocouple and a compensation thermocouple. The reference thermocouple is connected to an external data-acquisition system (DAS) through a two-pin thermocouple-alloy hermetic feedthrough connector, but this is the only such connector in the apparatus. The compensation thermocouple is connected to the DAS through two pins of the same ordinary multipin connector that connects the measurement thermocouples to the DAS.

Ziemke, Robert A.↗
NASA NTRSDate not supplied

GeoNEX: A Geostationary Earth Observatory

The latest generation of geostationary satellites (Himawari 8/9, GOES-16/17, FY-4, GK-2A) carries sensors that closely mimic the spatial and spectral characteristics of widely used polar-orbiting, global monitoring sensors such as MODIS and VIIRS. When combined, data from various currently operating/planned geostationary platforms provide a geo-ring of hyper-temporal (5-10 minutes), multispectral observations at spatial resolutions as high as 500 m. These high frequency observations offer exciting new possibilities for monitoring our planet, including better retrievals of geophysical variables by overcoming cloud cover, enabling studies of diurnally varying phenomena in the atmosphere, land, and the oceans, and support operational decision-making in agriculture, hydrology and disaster management. The NASA Earth Exchange (NEX) team, in collaboration with scientists from JAXA, KARI, NOAA and other international institutions, created the GeoNEX (www.nasa.gov/geonex) pipeline to integrate data from all available geostationary platforms and produce and distribute spatially, temporally, and radiometrically consistent data for the earth science community. We envision various institutions adapting the Geo component (e.g., GeoNOAA, GeoKARI, GeoChiba, GeoJAXA, GeoCMA) and customizing the pipeline and downstream products to serve the local/regional research and applied science communities. To facilitate collaborative work among the partners, we have established the OpenNEX platform on the public cloud. OpenNEX provides researchers, developers, educators, and ordinary users with easy access to an integrated Earth science computational and data platform, enabling citizen scientists and application developers to realize the full value of GeoNEX data assets and software tools.

GeoNEX↗
NASA NTRS1999

Plug and Play Integration through Space Object Standardization

Plug and play is an industry standard promoted by Intel and Microsoft, and others that allows users to add and remove various input and output devices without making specific customizations to their systems. The idea behind concept is that using standard products eases integration of components and promotes capabilities of conforming products. The concept works because vendors comply with a standard specification. This paper reports the development of a reference architecture for the mission control domain, which is leveraging off this revolutionary concept. Standards are being developed at the application layer, which enable "plug and play" of mission software products. A Mission Control, reference architecture has been defined. For each sub-domain, the interfaces are modeled in Interface Definition Language (IDL). A subset of the IDL has been developed within both commercial off-the-shelf (COTS) and government (GOTS) products. Selected vendors have agreed to modify their products to be compatible with the defined IDL. The plug and play integration of these different products has been validated in a demonstration testbed.

Boyce, Leslye↗
NASA NTRS2010

SensorWeb 3G: Extending On-Orbit Sensor Capabilities to Enable Near Realtime User Configurability

This research effort prototypes an implementation of a standard interface, Web Coverage Processing Service (WCPS), which is an Open Geospatial Consortium(OGC) standard, to enable users to define, test, upload and execute algorithms for on-orbit sensor systems. The user is able to customize on-orbit data products that result from raw data streaming from an instrument. This extends the SensorWeb 2.0 concept that was developed under a previous Advanced Information System Technology (AIST) effort in which web services wrap sensors and a standardized Extensible Markup Language (XML) based scripting workflow language orchestrates processing steps across multiple domains. SensorWeb 3G extends the concept by providing the user controls into the flight software modules associated with on-orbit sensor and thus provides a degree of flexibility which does not presently exist. The successful demonstrations to date will be presented, which includes a realistic HyspIRI decadal mission testbed. Furthermore, benchmarks that were run will also be presented along with future demonstration and benchmark tests planned. Finally, we conclude with implications for the future and how this concept dovetails into efforts to develop "cloud computing" methods and standards.

Mandl, Daniel↗
NASA NTRS2010

Kennedy Space Center's Partnership with Graftel Incorporated

NASA Kennedy Space Center (KSC) has recently partnered with Graftel Incorporated under an exclusive license agreement for the manufacture and sale of the Smart Current Signature Sensor. The Smart Current Signature Sensor and software were designed and developed to be utilized on any application using solenoid valves. The system monitors the electrical and mechanical health of solenoids by comparing the electrical current profile of each solenoid actuation to a typical current profile and reporting deviation from its learned behavior. The objective of this partnership with Graftel is for them to develop the technology into a hand-held testing device for their customer base in the Nuclear Power Industry. The device will be used to perform diagnostic testing on electromechanical valves used in Nuclear Power plants. Initially, Graftel plans to have working units within the first year of license in order to show customers and allow them to put purchase requests into their next year's budget. The subject technology under discussion was commercialized by the Kennedy Space Center Technology Programs and Partnerships Office, which patented the technology and licensed it to Graftel, Inc., a company providing support, instrumentation, and calibration services to the nuclear community and private sector for over 10 years. For the nuclear power industry, Graftel designs, manufacturers, and calibrates a full line of testing instrumentation. Grafters smart sensors have been in use in the United States since 1993 and have proved to decrease set-up time and test durations. The project was funded by Non-Destructive Engineering, and it is felt that this technology will have more emphasis on future vehicles. Graftel plans to market the Current Signature Sensor to the Electric Utility industry. Graftel currently supplies product and services to the Nuclear Power Industry in the United States as well as internationally. Product and services sold are used in non-destructive testing for valves, penetrations and other applications. Graftel also supplies testing services to an industrial customer base. The customer base includes 90 percent of the U.S. Nuclear plants and plants in Brazil, Europe, and Asia. Graftel works internationally with two representative groups and employees and has ten people at the principle location and a group of contract engineers around the country.

Dunn, Carol Anne↗
NASA NTRSDate not supplied

3D Scanning System to Assess Gravity-Dependent Body Shape Changes

The human body shows unique morphological changes when exposed to different gravity conditions, including muscle atrophy, fluid shift, and spinal elongation. Such changes need to be incorporated for human-system integration in the vehicle habitat, garment, and spacesuit designs, as inaccurate body measurements can result in suboptimal crew protection that can potentially decrease injury tolerance. However, measurement tools have not been available for accurate assessments of body shape changes. This work aimed to develop a prototype 3-D body scanning system with the configuration and performance optimized for in-flight crewmember body scanning. A scan hardware system was developed using Intel RealSense commercial off-the-shelf 3D sensors. The sensor parameters were iteratively optimized and tested to obtain the performance level needed for body scanning. A scan booth structure was fabricated, with the overall size 4 x 4 x 8 feet. The specific number of sensors and mounting positions were determined by iterative simulations, which indicated that 16 cameras can capture 94% and 96% of body surface area from the 1st percentile female and 99th percentile male crew population subject. The mounted sensors were linked through a mix of USB-C and USB-3 cables and operated for data acquisition from a Linux laptop computer. A software prototype was developed using Python and Tkinter graphical user interface toolkit. A calibration procedure was also built using a panel of QR codes. A computer vision tool detected and decoded the unique ID and pattern locations of the QR codes. The calibration information determined the position and orientation of the 3D sensors with respect to each other. The scanner performance was assessed using a set of 3D printed custom manikins. The manikin size and shape were derived from the previous ISS study, which measured the crewmembers’ anthropometry changes across the different flight phases. The average anthropometric measurements at the pre-flight and flight day 15 were sampled and projected onto the 1st percentile female and 99th percentile male body shapes. Another pair of manikins were also 3D printed to simulate the neutral body posture, estimated from ISS microgravity environments. A preliminary analysis assessed the performance of the newly developed scanner against the reference scanner, which has been used at the NASA JSC for crew and test subject anthropometry. Although the new scanner data showed several artifacts and missing geometries in the occluded body areas such as armpits and crotch, overall shape matched with the reference scan. When the manikin surface coordinates were compared, a root mean square error of 1.3 cm was observed from the manikin torso segment. Linear measurements including the stature, knee height and circumference measurements at the chest and calf showed differences from the reference scan measurements, ranging between 0.3 and 0.9 cm. Overall, this work demonstrated a development framework for an in-flight scanner with design and operation optimized for crewmember body scanning. Further improvement can potentially provide previously unavailable anthropometric data from different gravitational environments, including 0-g, 1/6-g, and 1-g. Such data can improve suit fit, habitat design, exercise efficacy quantification and sizing of orthostatic intolerance garments.

K H Kim↗
NASA NTRS1997

Analyzing Tabular and State-Transition Requirements Specifications in PVS

We describe PVS's capabilities for representing tabular specifications of the kind advocated by Parnas and others, and show how PVS's Type Correctness Conditions (TCCs) are used to ensure certain well-formedness properties. We then show how these and other capabilities of PVS can be used to represent the AND/OR tables of Leveson and the Decision Tables of Sherry, and we demonstrate how PVS's TCCs can expose and help isolate errors in the latter. We extend this approach to represent the mode transition tables of the Software Cost Reduction (SCR) method in an attractive manner. We show how PVS can check these tables for well-formedness, and how PVS's model checking capabilities can be used to verify invariants and reachability properties of SCR requirements specifications, and inclusion relations between the behaviors of different specifications. These examples demonstrate how several capabilities of the PVS language and verification system can be used in combination to provide customized support for specific methodologies for documenting and analyzing requirements. Because they use only the standard capabilities of PVS, users can adapt and extend these customizations to suit their own needs. Those developing dedicated tools for individual methodologies may find these constructions in PVS helpful for prototyping purposes, or as a useful adjunct to a dedicated tool when the capabilities of a full theorem prover are required. The examples also illustrate the power and utility of an integrated general-purpose system such as PVS. For example, there was no need to adapt or extend the PVS model checker to make it work with SCR specifications described using the PVS TABLE construct: the model checker is applicable to any transition relation, independently of the PVS language constructs used in its definition.

Owre, Sam↗
NASA NTRS2005

James Webb Space Telescope XML Database: From the Beginning to Today

The James Webb Space Telescope (JWST) Project has been defining, developing, and exercising the use of a common eXtensible Markup Language (XML) for the command and telemetry (C&T) database structure. JWST is the first large NASA space mission to use XML for databases. The JWST project started developing the concepts for the C&T database in 2002. The database will need to last at least 20 years since it will be used beginning with flight software development, continuing through Observatory integration and test (I&T) and through operations. Also, a database tool kit has been provided to the 18 various flight software development laboratories located in the United States, Europe, and Canada that allows the local users to create their own databases. Recently the JWST Project has been working with the Jet Propulsion Laboratory (JPL) and Object Management Group (OMG) XML Telemetry and Command Exchange (XTCE) personnel to provide all the information needed by JWST and JPL for exchanging database information using a XML standard structure. The lack of standardization requires custom ingest scripts for each ground system segment, increasing the cost of the total system. Providing a non-proprietary standard of the telemetry and command database definition formation will allow dissimilar systems to communicate without the need for expensive mission specific database tools and testing of the systems after the database translation. The various ground system components that would benefit from a standardized database are the telemetry and command systems, archives, simulators, and trending tools. JWST has exchanged the XML database with the Eclipse, EPOCH, ASIST ground systems, Portable spacecraft simulator (PSS), a front-end system, and Integrated Trending and Plotting System (ITPS) successfully. This paper will discuss how JWST decided to use XML, the barriers to a new concept, experiences utilizing the XML structure, exchanging databases with other users, and issues that have been experienced in creating databases for the C&T system.

Gal-Edd, Jonathan↗
NASA NTRS2005

Requirements to Design to Code: Towards a Fully Formal Approach to Automatic Code Generation

A general-purpose method to mechanically transform system requirements into a provably equivalent model has yet to appear. Such a method represents a necessary step toward high-dependability system engineering for numerous possible application domains, including distributed software systems, sensor networks, robot operation, complex scripts for spacecraft integration and testing, and autonomous systems. Currently available tools and methods that start with a formal model of a system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The gap that current tools and methods leave unfilled is that their formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the classes of systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or in other appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations.

Hinchey, Michael G.↗
NASA NTRS2005

Requirements to Design to Code: Towards a Fully Formal Approach to Automatic Code Generation

A general-purpose method to mechanically transform system requirements into a provably equivalent model has yet to appear. Such a method represents a necessary step toward high-dependability system engineering for numerous possible application domains, including distributed software systems, sensor networks, robot operation, complex scripts for spacecraft integration and testing, and autonomous systems. Currently available tools and methods that start with a formal model of a: system and mechanically produce a provably equivalent implementation are valuable but not sufficient. The "gap" that current tools and methods leave unfilled is that their formal models cannot be proven to be equivalent to the system requirements as originated by the customer. For the ciasses of systems whose behavior can be described as a finite (but significant) set of scenarios, we offer a method for mechanically transforming requirements (expressed in restricted natural language, or in other appropriate graphical notations) into a provably equivalent formal model that can be used as the basis for code generation and other transformations.

Hinchey, Michael G.↗