Results for “Cyber-physical simulation”

NASA NTRS2020

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

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.

Mavridou, Anastasia↗

NASA NTRS2018

Serious Gaming for Building a Basis of Certification via Trust and Trustworthiness of Autonomous Systems

Autonomous systems governed by a variety of adaptive and nondeterministic algorithms are being planned for inclusion into safety-critical environments, such as unmanned aircraft and space systems in both civilian and military applications. However, until autonomous systems are proven and perceived to be capable and resilient in the face of unanticipated conditions, humans will be reluctant or unable to delegate authority, remaining in control aided by machine-based information and decision support. Proving capability, or trustworthiness, is a necessary component of certification. Perceived capability is a component of trust. Trustworthiness is an attribute of a cyber-physical system that requires context-driven metrics to prove and certify. Trust is an attribute of the agents participating in the system and is gained over time and multiple interactions through trustworthy behavior and transparency. Historically, artificial intelligence and machine learning systems provide answers without explanation - without a rationale or insight into the machine “thinking”. In order to function as trusted teammates, machines must be able to explain their decisions and actions. This transparency is a product of both content and communication. NASA’s Autonomy Teaming & TRAjectories for Complex Trusted Operational Reliability (ATTRACTOR) project seeks to build a basis for certification of autonomous systems via establishing metrics for trustworthiness and trust in multi-agent team interactions, using AI (Artificial Intelligence) explainability and persistent modeling and simulation, in the context of mission planning and execution, with analyzable trajectories. Inspired by Massively Multiplayer Online Role Playing Games (MMORPG) and Serious Gaming, the proposed ATTRACTOR modeling and simulation environment is similar to online gaming environments in which player (aka agent) participants interact with each other, affect their environment, and expect the simulation to persist and change regardless of any individual agent’s active participation. This persistent simulation environment will accommodate individual agents, groups of self-organizing agents, and large-scale infrastructure behavior. The effects of the emerging adaptation and coevolution can be observed and measured to building a basis of measurable trustworthiness and trust, toward certification of safety-critical autonomous systems.

Allen, B. Danette↗

NASA NTRS2010

SimCheck: An Expressive Type System for Simulink

MATLAB Simulink is a member of a class of visual languages that are used for modeling and simulating physical and cyber-physical systems. A Simulink model consists of blocks with input and output ports connected using links that carry signals. We extend the type system of Simulink with annotations and dimensions/units associated with ports and links. These types can capture invariants on signals as well as relations between signals. We define a type-checker that checks the wellformedness of Simulink blocks with respect to these type annotations. The type checker generates proof obligations that are solved by SRI's Yices solver for satisfiability modulo theories (SMT). This translation can be used to detect type errors, demonstrate counterexamples, generate test cases, or prove the absence of type errors. Our work is an initial step toward the symbolic analysis of MATLAB Simulink models.

Roy, Pritam↗

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

SafeMAP: Safe Multi-Agent Planning Framework Based on Dynamic Probabilistic Risk Assessment

This paper proposes a risk-aware framework for Safe Multi-Agent Planning (SafeMAP) that unifies disparate models for multi-agent systems in a Markovian process that allows for simultaneous system health monitoring, decision making under uncertainty, and multi-agent system collaboration. As operations beyond low earth orbit mature, there is an increased need for autonomous cyber-physical systems with onboard decision making capabilities. Multi-agent cyber-physical systems in particular offer the potential of increased efficiency, resiliency, and mission capabilities for future applications such as multi-rover terrain operations, distributed satellite operations, and management of smart lunar habitats. SafeMAP utilizes physics-based models of each agent and the relevant components, probability models of the environment and component operational states, and reward models for mission-specific objectives such as scientific task completion or resource consumption. The output of SafeMAP is a set of mission plans that satisfy the mission objective under specified risk/reward constraints. A readable interpretation of each of these generated mission plans is provided as an additional output. SafeMAP has been demonstrated on a simulated case study involving a four-rover system performing surface mapping operations and science tasks. Results of this paper demonstrate SafeMAP’s ability to generate explainable mission plans that satisfy the mission objective while minimizing risk under nominal and off-nominal conditions.

Mohammad Hejase↗

NASA NTRSDate not supplied

SafeMAP: Safe Multi-Agent Planning framework based on Dynamic Probabilistic Risk Assessment

This paper proposes a risk-aware framework for Safe Multi-Agent Planning (SafeMAP) that unifies disparate models for multi-agent systems in a Markovian process that allows for simultaneous system health monitoring, decision making under uncertainty, and multi-agent system collaboration. As operations beyond low earth orbit mature, there is an increased need for autonomous cyber-physical systems with onboard decision making capabilities. Multi-agent cyber-physical systems in particular offer the potential of increased efficiency, resiliency, and mission capabilities for future applications such as multi-rover terrain operations, distributed satellite operations, and management of smart lunar habitats. SafeMAP utilizes physics-based models of each agent and the relevant components, probability models of the environment and component operational states, and reward models for mission-specific objectives such as scientific task completion or resource consumption. The output of SafeMAP is a set of mission plans that satisfy the mission objective under specified risk/reward constraints. A readable interpretation of each of these generated mission plans is provided as an additional output. SafeMAP has been demonstrated on a simulated case study involving a four-rover system performing surface mapping operations and science tasks. Results of this paper demonstrate SafeMAP’s ability to generate explainable mission plans that satisfy the mission objective while minimizing risk under nominal and off-nominal conditions.

Mohammad Hejase↗