Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Lustre”

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.

23 records · Page 2
All sourcesNASA NTRSDOE OSTI
NASA NTRSDate not supplied

CoCoSim Tutorial: Contract-based Compositional Verification of Simulink Models

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.

Formal Verification↗
NASA NTRSDate not supplied

FRET Tutorial

In this tutorial, we present the FRET tool for writing, understanding, formalizing and analyzing requirements. In practice, requirements are typically written in natural language, which is ambiguous and consequently not amenable to formal analysis. Since formal, mathematical notations are unintuitive, requirements in FRET are entered in a restricted, natural language, called FRETish with precise unambiguous meaning. This tutorial explains how requirements can be captured in FRETish and subsequently formalized in temporal logics and in the synchronous data flow language Lustre. We show, through multiple examples, how FRET assists users in understanding FRETish requirements and clarifying subtle semantic issues through English and diagrammatic explanations as well as interactive simulation. FInally, this tutorial describes how FRET can be used to perform realizability checking for identifying conflicting requirements and the connection of FRET with (1) the CoCoSim automated analysis tool for the verification of Simulink and Stateflow models, and (2) the Copilot runtime monitoring tool for the analysis of C programs.

FRET↗
NASA NTRS2020

Global earth mineral inventory: A data legacy

Minerals contain important clues to understanding the complex geologic history of Earth and other planetary bodies. Therefore, geologists have been collecting mineral samples and compiling data about these samples for centuries. These data have been used to better understand the movement of continental plates, the oxidation of Earth's atmosphere and the water regime of ancient martian landscapes. Datasets found at ‘RRUFF.info/Evolution’ and ‘mindat.org’ have documented a wealth of mineral occurrences around the world. One of the main goals in geoinformatics has been to facilitate discovery by creating and merging datasets from various scientific fields and using statistical methods and visualization tools to inspire and test hypotheses applicable to modelling Earth's past environments. To help achieve this goal, we have compiled physical, chemical and geological properties of minerals and linked them to the above-mentioned mineral occurrence datasets. As a part of the Deep Time Data Infrastructure, funded by the W.M. Keck Foundation, with significant support from the Deep Carbon Observatory (DCO) and the A.P. Sloan Foundation, GEMI (‘Global Earth Mineral Inventory’) was developed from the need of researchers to have all of the required mineral data visible in a single portal, connected by a robust, yet easy to understand schema. Our data legacy integrates these resources into a digestible format for exploration and analysis and has allowed researchers to gain valuable insights from mineralogical data. GEMI can be considered a network, with every node representing some feature of the datasets, for example, a node can represent geological parameters like colour, hardness or lustre. Exploring subnetworks gives the researcher a specific view of the data required for the task at hand. GEMI is accessible through the DCO Data Portal (https://dx.deepcarbon.net/11121/6200-6954-6634-8243-CC). We describe our efforts in compiling GEMI, the Data Policies for usage and sharing, and the evaluation metrics for this data legacy.

data legacy↗
NASA NTRSDate not supplied

Bridging the Gap Between Requirements and Simulink Model Analysis

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.

FRET↗