Mohammad Hejase | Search NASA

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 and Testing of Autonomous Distributed Space Systems

Distributed Space Systems (DSS) are an emerging class of mission designs that enable new scientific and commercial opportunities. In order to enable those new opportunities, these systems will need to have significantly expanded autonomous capabilities compared to their single-spacecraft predecessors. In this paper, we present Distributed Spacecraft Autonomy (DSA) project, a payload on NASA's Starling spacecraft experiment. We first describe a step-by-step process for characterizing what features are needed in an autonomous DSS, and show how this process applied to DSA. We then describe the Starling mission, a four-spacecraft swarm hosting multiple DSS payloads. We then describe DSA, which will mature in-space networking and autonomous planning technologies to measure topside ionosophere features using data from the Starling spacecraft's GPS receivers. We describe how DSA will coordinate observations of GPS satellites using Starling's underlying communications infrastructure combined with novel DSS technology. The flight validation of DSS technology will provide mature technology to enable future DSS missions.

Nicholas Cramer↗

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↗

NASA NTRSDate not supplied

Biosentinel: Mission Summary and Lessons Learned From the First Deep Space Biology CubeSat Mission

Launched on Artemis-1, BioSentinel carries a biology experiment into deep space for the first time in 50 years. A 6U CubeSat form factor was utilized for the spacecraft which included technologies newly developed or adapted for operations beyond Earth orbit. The spacecraft carries onboard budding yeast, Saccharomyces cerevisiae, as an analog to human cells to test the biological response to deep space radiation. This was the maiden deep-space voyage for many of the subsystems, and the first time to evaluate their performance in flight operation. Flying a CubeSat beyond LEO comes with unique challenges with respect to trajectory uncertainty and mission operations planning. The nominal plan was a lunar fly-by, followed by an insertion into Heliocentric orbit. However, some possible scenarios included lunar eclipses that could have severely impacted the power budget during that phase of the mission, while others could have resulted in a “Retrograde” hyperbola at swing-by resulting in the spacecraft traveling inward toward Earth or even towards a collision with the lunar surface. The commissioning phase of the mission was successful and completed a week ahead of schedule. It did not come without its exciting moments and challenges. First contact with the spacecraft uncovered that the vehicle was unexpectedly tumbling after deployment, a situation that needed to be corrected urgently. The mission operations team executed a contingency plan to stabilize the spacecraft, with just moments to spare before the battery ran out of power. The BioSensor payload onboard the spacecraft is a complex instrument that includes microfluidics, fluid systems, sensor control electronics, as well at the living yeast cells. BioSentinel also included a TimePix radiation sensor implemented by JSC’s RadWorks group. Dose and Linear Energy Transfer (LET) data is compared directly to the rate of DSB-and repair events measured by the S. cerevisiae cells. BioSentinel mature nanosatellite technologies included: deep space communications and navigation, autonomous attitude control and momentum management, and micro-propulsion systems, to provide an adaptable nanosatellite platform for deep space uses. This paper discusses the performance of the BioSentinel spacecraft through the mission phase, and includes lessons learned from challenges and anomalies. BioSentinel had many successes and will be a pathfinder for future deep space CubeSats and biology missions.

BioSentinel↗

NASA NTRSDate not supplied

Biosentinel: The First Deep Space Biology CubeSat Mission- Mission Summary and Lessons Learned

Launched on Artemis-1, BioSentinel carries a biology experiment into deep space for the first time in 50 years. A 6U CubeSat form factor was utilized for the spacecraft which included technologies newly developed or adapted for operations beyond Earth orbit. The spacecraft carries onboard budding yeast, Saccharomyces cerevisiae, as an analog to human cells to test the biological response to deep space radiation. This was the maiden deep-space voyage for many of the subsystems, and the first time to evaluate their performance in flight operation. Flying a CubeSat beyond LEO comes with unique challenges with respect to trajectory uncertainty and mission operations planning. The nominal plan was a lunar fly-by, followed by an insertion into Heliocentric orbit. However, some possible scenarios included lunar eclipses that could have severely impacted the power budget during that phase of the mission, while others could have resulted in a “Retrograde” hyperbola at swing-by resulting in the spacecraft traveling inward toward Earth or even towards a collision with the lunar surface. The commissioning phase of the mission was successful and completed a week ahead of schedule. It did not come without its exciting moments and challenges. First contact with the spacecraft uncovered that the vehicle was unexpectedly tumbling after deployment, a situation that needed to be corrected urgently. The mission operations team executed a contingency plan to stabilize the spacecraft, with just moments to spare before the battery ran out of power. The BioSensor payload onboard the spacecraft is a complex instrument that includes microfluidics, fluid systems, sensor control electronics, as well at the living yeast cells. BioSentinel also included a TimePix radiation sensor implemented by JSC’s RadWorks group. Dose and Linear Energy Transfer (LET) data is compared directly to the rate of DSB-and repair events measured by the S. cerevisiae cells. BioSentinel mature nanosatellite technologies included: deep space communications and navigation, autonomous attitude control and momentum management, and micro-propulsion systems, to provide an adaptable nanosatellite platform for deep space uses. This paper discusses the performance of the BioSentinel spacecraft through the mission phase, and includes lessons learned from challenges and anomalies. BioSentinel had many successes and will be a pathfinder for future deep space CubeSats and biology missions.

BioSentinel↗

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 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 NTRSDate not supplied

The Troupe System: an Autonomous Multi-Agent Rover Swarm

Autonomous cooperative robotic systems are the future of space exploration. The complexity of such systems makes their development, verification and assurance challenging. The Robust Software Engineering group at NASA Ames has developed the Troupe project that aims to explore the design and development of a swarm of autonomous rovers tasked to perform autonomous exploration and mapping of an unknown terrain. In this paper, we showcase the system design, and accompanying verification and validation tools integrated in the Troupe system development life-cycle.

TROUPE↗