Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “CoCoSim”

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.

13 records
All sourcesNASA NTRSDOE OSTI
NASA NTRS2020

CoCoSim, a Code Generation Framework for Control/command Applications: An Overview of CoCoSim for Multi-Periodic Discrete Simulink Models

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.

Bourbouh, Hamza↗
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

Design, Formalization, and Verification of Decision Making for Intelligent Systems

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.

Model-based development↗
NASA NTRS2018

Investigation of a Verification and Validation Tool with a Turbofan Aircraft Engine Application

The development of more advanced control architectures for turbofan aircraft engines can yield gains in performance and efficiency over the lifetime of an engine. However, the implementation of these increasingly complex controllers is contingent on their ability to provide safe, reliable engine operation. Therefore, having the means to verify the safety of new control algorithms is crucial. As a step towards this goal, CoCoSim, a publicly available verification tool for Simulink, is used to analyze C-MAPSS40k, a 40,000 lbf class turbo-fan engine model developed at NASA for testing new control algorithms. Due to current limitations of the verification software, several modifications are made to C-MAPSS40k to achieve compatibility with CoCoSim. Some of these modifications sacrifice fidelity to the original model. Several safety and performance requirements typical for turbofan engines are identified and constructed into a verification framework. Preliminary results using an industry standard baseline controller for these requirements are presented. While verification capabilities are demonstrated, a truly comprehensive analysis will require further development of the verification tool.

V&↗
NASA NTRSDate not supplied

The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained

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.

Anastasia Mavridou↗
NASA NTRSDate not supplied

Design, Formalization, and Verification of Decision Making for Intelligent Systems

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.

Model-based development↗
NASA NTRS2019

Bridging the Gap Between Requirements and Model Analysis: Evaluation on Cyber-Physical Challenge Problems

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.

Simulink↗
NASA NTRSDate not supplied

Capturing and Analyzing Requirements with FRET

FRET is an open source tool, developed at NASA Ames, 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. FRET helps users write FRETish requirements both by providing grammar information and examples during editing, but also through English and diagrammatic explanations to clarify subtle semantic issues. For each requirement, FRET automatically produces formalizations and supports interactive simulation of produced formalizations to ensure that they capture user intentions. Through its analysis portal, FRET connects to analysis tools by exporting verification code. Currently FRET connects to (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 also supports the consistency/realizability analysis of requirements for identifying conflicting requirements. In this tutorial, we introduce FRET and learn to speak and analyze FRETish through several examples.

FRET↗
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 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↗