SEARCH · Search NASA
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.
This document explains all the necessary steps in order to generate optimized C code from Simulink Models. This document also covers some general information on good programming practices, selection of variable types, how to organize models and subsystems, and finally how to test the generated C code and compare it with data from MATLAB.
The Linear Autoland Simulink model was created to be a modular test environment for testing of control system components in commercial aircraft. The input variables, physical laws, and referenced frames used are summarized. The state space theory underlying the model is surveyed and the location of the control actuators described. The equations used to realize the Dryden gust model to simulate winds and gusts are derived. A description of the pseudo-random number generation method used in the wind gust model is included. The longitudinal autopilot, lateral autopilot, automatic throttle autopilot, engine model and automatic trim devices are considered as subsystems. The experience in converting the Airlabs FORTRAN aircraft control system simulation to a graphical simulation tool (Matlab/Simulink) is described.
Simulink model for a New Energy 5kW hydropower turbine. ADCP data ("ds_streamwise_7_13.nc") and DC voltage, DC current, and rotor rotation observed from the New Energy EVG-005 Current Energy Converter (CEC) ("electrical_7_13_10ohms.nc") were collected at the Tanana River Test Site (TRTS) near Nenana Alaska. - Data was collected on July 13th, 2023 with a constant 10 ohms resistance applied with a DC load bank. - Simulink model is meant to resemble the electrical setup at the TRTS. - Model is initialized by running the "NewEnergy_2023_10hz.m" Matlab script. Then the Simulink model ("New_Energy_Model_PMSM.slx") can be run. - Results are processed with the "NewEnergy_2023_processing.m" Matlab code. The Matlab results are also saved in the "New_Energy_7_13_model_validation_results.mat" Matlab file. This can be directly loaded into the Matlab Workspace using the "Load()" command. - The timetable variables "electrical_model_downsampled" is the model results and the "electrical_limited" is the experimental data from the TRTS.
Pumped Storage Hydropower (PSH) is one of the most popular energy storage technologies in the world. It uses an upper reservoir to store water which can be later used during high-demand. In the United States, most of the energy storage capability actually corresponds to PSH. Moreover, PSH also brings multiple benefits to grid operation. This report presents the Simulink models of three common PSH technologies: Fixed-Speed (FS), Variable-Speed (VS), and Ternary (T)-PSH. These models are available to the general public on this GitHub repository, which contains the MATLAB model initialization files, the Simulink model files, and supplementary MATLAB code used to obtain the figures in this work. For each PSH model, an introductory description of the model components and other relevant functionalities are provided. For further information regarding the models and the initialization parameters, the reader is referred to the shared files in the repository. This report also presents the dynamic behavior of each model. The response of such models to a load event is analyzed and matched with each model's features. A custom IEEE 39 bus case is employed for the FS and T-PSH simulations, while the VS-PSH is simulated on a simplified three-bus test system due to the computational complexity of the model. For the T-PSH, the steady-state and the switching between several operating modes are also studied in this work.
We present CoCoSim, a framework to support the design, code generation and analysis of discrete dataflow model expressed in Simulink. In this work, we specifically focus on the analysis and code generation of multi-periodic systems. For that CoCoSim provides two complementary approaches: the first amounts to encode the multiperiodic semantics in a pure-synchronous one – à la Lustre–, enabling the use of model checker for verifying properties. The second provides a faithful code generation into multiple communicating (mono)synchronous components – à la Prelude– that can be then simulated or embedded in the final platform with any real-time scheduler. These approaches have been experimented in various settings.
Formal veri fication and simulation are powerful tools for the veri fication of requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically expressed in natural language. There is a gap between such requirements and their software implementations. We present a framework that bridges this gap by supporting a tight integration and feedback loop between high-level requirements and their analysis against software artifacts. Our framework implements an analysis portal within the fret requirements elicitation tool, thus forming an end-to-end, open-source environment where requirements are written in an intuitive, structured natural language, and are veri fied automatically against Simulink models.
Formal verification and simulation are powerful tools for the verification of requirements against complex systems. Requirements are developed in early stages of the software lifecycle and are typically expressed in natural language. There is a gap between such requirements and their software implementations.We present a framework that bridges this gap by supporting a tight integration and feedback loop between high-level requirements and their analysis against software artifacts. Our framework implements an analysis portal within the fret requirements elicitation tool, thus forming an end-to-end, open-source environment where requirements are written in an intuitive, structured natural language, and are verified automatically against Simulink models.
A numerical model of the Ares I upper stage main propulsion system is formulated based on first principles. Equation's are written as non-linear ordinary differential equations. The GASP fortran code is used to compute thermophysical properties of the working fluids. Complicated algebraic constraints are numerically solved. The model is implemented in Simulink and provides a rudimentary simulation of the time history of important pressures and temperatures during re-pressurization, boost and upper stage firing. The model is validated against an existing reliable code, and typical results are shown.
Explore the source record for details and available documents.
This tutorial presents CoCoSim, a verification framework for MATLAB Simulink and Stateflow models. We demonstrate CoCoSim’s architecture, designed to be compatible with Lustre-based verification tools, as well as easily extensible to other candidate backends. We focus on CoCoSim’s powerful compositional verification scheme, which allows for scalable verification through the usage of abstractions of subsystems, express ed in the form of Assume-Guarantee Contracts. We show CoCoSim’s interconnection with NASA’s Formal Requirements Tool (FRET), that enables a seamless transition between authoring and formally verifying requirements for Simulink/Stateflow models. Finally, we discuss work in progress with regards to test case generation options in CoCoSim, demonstrating the generation of MC/DC tests for Simulink artifacts.
The development of autonomous systems requires a rigorous process that can guarantee a system’s reliability in critical applications. At its core, an autonomous system bases its behavior on a well-defined decision making system. In this paper, we present a methodological basis for the design, formalization and formal verification of Decision Making systems for autonomous agents. The approach is generally applicable to operational objectives that can be functionally decomposed and subsequently represented as Hierarchical Finite State Machines. As a case study, we present the application of this method to implement a Decision Making model in Simulink. Furthermore, we present how we use NASA’s FRET tool to write requirements in structured natural language and generate formal specifications that can be automatically digested by NASA’s CoCoSim tool. Finally, we present how, by leveraging CoCoSim, we perform formal verification against the Simulink model and present analysis results.
The development of autonomous systems requires a rigorous process that can guarantee a system’s reliability in critical applications. At its core, an autonomous system bases its behavior on a well-defined decision making system. In this paper, we present a methodological basis for the design, formalization and formal verification of Decision Making systems for autonomous agents. The approach is generally applicable to operational objectives that can be functionally decomposed and subsequently represented as Hierarchical Finite State Machines. As a case study, we present the application of this method to implement a Decision Making model in Simulink. Furthermore, we present how we use NASA’s FRET tool to write requirements in structured natural language and generate formal specifications that can be automatically digested by NASA’s CoCoSim tool. Finally, we present how, by leveraging CoCoSim, we perform formal verification against the Simulink model and present analysis results.
As a part of the preliminary design work being performed for the Orion vehicle, the Orion to Spacecraft Adaptor (SA) separation mechanism was analyzed and sized, with findings presented here. Sizing is based on worst case abort condition as a result of an anomaly driving the launch vehicle engine thrust vector control hard-over causing a severe vehicle pitch over. This worst-case scenario occurs just before Upper Stage Main Engine Cut-Off when the vehicle is the lightest and the damping effect due to propellant slosh has been reduced to a minimum. To address this scenario and others, two modeling approaches were invoked. The first approach was a detailed Simulink model to quickly assess the Service Module Engine nozzle to SA clearance for a given separation mechanism. The second approach involved the generation of an Automatic Dynamic Analysis of Mechanical Systems (ADAMS) model to assess secondary effects due to mass centers of gravity that were slightly off the vehicle centerline. It also captured any interference between the Solar Arrays and the Spacecraft Adapter. A comparison of modeling results and accuracy are discussed. Most notably, incorporating a larger SA flange diameter allowed for a natural separation of the Orion and its engine nozzle even at relatively large pitch rates minimizing the kickoff force. Advantages and disadvantages of the Simulink model vs. a full geometric ADAMS model are discussed as well.
As a part of the preliminary design work being performed for the Orion vehicle, the Orion to Spacecraft Adaptor (SA) separation mechanism mechanism was analyzed and sized, with findings presented here. Sizing is based on worst case abort condition as a result of an anomaly driving the launch vehicle engine thrust vector control hard-over causing a severe vehicle pitch over. This worst case scenario occurs just before Upper Stage Main Engine Cut-Off (MECO) when the vehicle is the lightest and the damping effect due to propellant slosh has been reduced to a minimum. To address this scenario and others, two modeling approaches were invoked. The first approach was a detailed Simulink model to quickly assess the Service Module Engine nozzle to SA clearance for a given separation mechanism. The second approach involved the generation of an Automatic Dynamic Analysis of Mechanical Systems (ADAMS) model to assess secondary effects due to mass centers of gravity that were slightly off the vehicle centerline. It also captured any interference between the Solar Arrays and the Spacecraft Adapter. A comparison of modeling results and accuracy are discussed. Most notably, incorporating a larger SA flange diameter allowed for a natural separation of the Orion and its engine nozzle even at relatively large pitch rates minimizing the kickoff force. Advantages and disadvantages of the Simulink model vs. a full geometric ADAMS model are discussed as well.
As a part of the preliminary design work being performed for the Orion vehicle, the Orion to Spacecraft Adaptor (SA) separation mechanism was analyzed and sized, with findings presented here. Sizing is based on worst case abort condition as a result of an anomaly driving the launch vehicle engine thrust vector control hard-over causing a severe vehicle pitch over. This worst case scenario occurs just before Upper Stage Main Engine Cut-Off (MECO) when the vehicle is the lightest and the damping effect due to propellant slosh has been reduced to a minimum. To address this scenario and others, two modeling approaches were invoked. The first approach was a detailed Simulink model to quickly assess the Service Module Engine nozzle to SA clearance for a given separation mechanism. The second approach involved the generation of an Automatic Dynamic Analysis of Mechanical Systems (ADAMS) model to assess secondary effects due to mass centers of gravity that were slightly off the vehicle centerline. It also captured any interference between the Solar Arrays and the Spacecraft Adapter. A comparison of modeling results and accuracy are discussed. Most notably, incorporating a larger SA flange diameter allowed for a natural separation of the Orion and it's engine nozzle even at relatively large pitch rates minimizing the kickoff force. Advantages and disadvantages of the Simulink model vs. a full geometric ADAMS model are discussed as well.
We present a framework for introducing high-level requirement specifications in the automated analysis of dataflow models. By integrating the FRET requirements elicitation tool with the CoCoSim analyzer, our framework enables the analysis of hierarchical Simulink models against requirements written in a restricted English language. More precisely, we support: automatic extraction of Simulink model information and association of high-level requirements with target model signals and components; translation of temporal logic formulas into synchronous dataflow CoCoSpec specifications as well as Simulink monitors; and interpretation of counterexamples produced by the analysis both at the requirement and model level. The features provided by our framework are generic and can be used to integrate other requirements elicitation and Simulink/Lustre analysis tools. We report on the lessons learned from the application of our approach to the Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems. For the analysis, we used the Kind2, Zustre, and Simulink Design Verifier (SLDV) tools.
Formal verfication and simulation are powerful tools to validate requirements against complex systems. [Problem] Requirements are developed in early stages of the software lifecycle and are typically written in ambiguous natural language. There is a gap between such requirements and formal notations that can be used by verification tools, and lack of support for proper association of requirements with software artifacts for verification. [Principal idea] We propose to write requirements in an intuitive, structured natural language with formal semantics, and to support formalization and model/code verification as a smooth, well-integrated process. [Contribution] We have developed an end-to-end, open source requirements analysis framework that checks Simulink models against requirements written in structured natural language. Our framework is built in the Formal Requirements Elicitation Tool (fret); we use fret's requirements language named fretish, and formalization of fretish requirements in temporal logics. Our proposed framework contributes the following features: 1) automatic extraction of Simulink model information and association of fretish requirements with target model signals and components; 2) translation of temporal logic formulas into synchronous dataflow cocospec specifications as well as Simulink monitors, to be used by verification tools; we establish correctness of our translation through extensive automated testing; 3) interpretation of counterexamples produced by verification tools back at requirements level. These features support a tight integration and feedback loop between high level requirements and their analysis. We demonstrate our approach on a major case study: the Ten Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems.
Capturing and analyzing requirements of Cyber-Physical Systems (CPS) can be challenging, since CPS models typically involve time-varying and real-valued variables, physical system dynamics, or even adaptive behavior. MATLAB/Simulinkis a development and simulation framework that is widely used in industry to capture such systems. In this paper, we report on the application of NASA Ames tools to perform end-to-end analysis of the Ten Lockheed Martin Challenge Problems (LMCPS). LMCPS is a set of industrial Simulink model benchmarks and natural language requirements developed by domain experts. Our framework, which integrates the tools FRET and COCOSIM, is used to: 1) elicit, explain, and formalize the semantics of the given natural language requirements; 2) generate verification code and monitors that can be automatically attached to the Simulink models; 3) perform verification by using SMT-based model checkers. FRET and COCOSIM are open source, and can be used by other researchers and practitioners to replicate our case study. We provide a categorization of recurring patterns in the formalization of the requirements and discuss the strengths and weaknesses of our automated verification approach.