Flight Software Verification

Flight software verification is a ladder of test venues ordered by fidelity and inversely by throughput. The bottom rung is a workstation running the flight software against simulated hardware; the top is the flight vehicle itself. The engineering question at every rung is which defect classes it can find and which it structurally cannot.

Five families of method sit on that ladder. Simulation and testbed testing are what every flown mission has relied on. Fault injection measures recovery behavior against a stated failure model. Model checking and other formal methods have been applied to narrow pieces of flown software and in laboratory trials. Scenario-based validation targets autonomy whose behavior cannot be enumerated. Post-launch defect analysis feeds back into all four. A 2022 survey of the flown JPL autonomy systems, from the Deep Space 1 Remote Agent Experiment to the Mars 2020 onboard scheduler, found that in every case most verification effort was testing plus informal methods such as code walkthroughs, coding rules and design reviews, and that formal methods were almost always reduced to running static code analyzers [10]. The exceptions were SPIN model checking of the Remote Agent executive, which found several concurrency bugs, and SPIN with statechart code generation on MSL flight software [10]. The sections below follow that order.

The ladder, and what each rung costs

MSL’s internal testing described four stages: unit tests, the Work Station Test Set, System Integrated Test, and Assembly Test and Launch Operations on real spacecraft hardware, with cost rising and availability falling at each step [4]. The Work Station Test Set runs the flight software under a VxWorks simulator on a Linux workstation and is described as cheap relative to every other method.

Venue	Fidelity	Speed	Mission
Work Station Test Set (WSTS)	flight software against modeled avionics, no real hardware	2 to 10 times real time depending on scenario complexity [3]	MSL
WSTS, Mars 2020 build	same, enhanced	6 times real time [5]	Mars 2020
SSim	flight software in the loop with rover mechanisms and terrain	up to 1000 times faster than the flight compute element [1]	MSL, Mars 2020
Mission System Testbed (MSTB)	hardware in the loop with two Rover Compute Elements, no actuators [5]	real time	Mars 2020
Vehicle System Testbed (VSTB)	near-duplicate rover [5]	real time	Mars 2020
Integrated Test Laboratory (ITL)	system-level, mixed real and simulated units [6]	real time	Cassini

The workstation simulator earns its place on usage, not on fidelity. MSL’s WSTS was first deployed in October 2006 and had reached its thirtieth release by 2008, by which point its monthly usage peaked near 3500 hours and it averaged an order of magnitude more use than the project’s hardware-in-the-loop testbeds [3]. It models every hardware behavior visible to the flight software as finite state machines, integrating differential equations where the dynamics require it, and supports fault injection at either the functional level or by setting individual bits, along with pause, resume and single step.

Mars 2020 built the Surface System Development Environment for the same reason inverted: Rover Compute Elements and motor controller assemblies were scarce and shared across subsystems, and the physical test venues, running three shifts a day seven days a week, still could not absorb the demand [2]. The sampling and caching subsystem alone has 19 actuators and over 100 sensors, including strain gauges, resolvers, temperature sensors and contact switches. The environment presents one interface to the flight software over three interchangeable backends: an abstraction layer giving deterministic force and motion simulation, a terrain simulator with slip modeling, visual odometry, pose tracking and rendered camera imagery, and a motor server that drives real testbed hardware over TCP/IP. Substituting the backend rather than the test case is what lets the same test run in software and on hardware.

What simulation found that nothing else would have

Two flight-software state interactions on MSL are the documented catches. In one, a MastCam focus mechanism lock was not properly monitored before a motion command, and a visual odometry command unconditionally reinforced that state even though it was not a drive command; SSim caught the improperly set focus lock that would have failed the entire drive, and SSim was extended to model MastCam as a result [1]. In the other, SSim was used to model ChemCam laser targeting in terrain-relative frames to check the beam against the rover body for self-intersection.

These are combinatorial state defects, and they are found in simulation because simulation is where the combinations can be run. MSL flight software carries more than 4200 commands with dozens of arguments each, 54,000 parameters and tens of thousands of state variables [1]. The arm at Rocknest alone executed 2404 moves, against 2303 for Opportunity over its entire Victoria Crater journey, and self-collision checking requires at least 3 mm of margin.

Hardware in the loop found a different class. Mars 2020 ran the development environment against brassboard hardware at three venues from 2017 and 2018, the docking testbed with robotic arm and dock hardware, a coring software venue with the corer, and a multi-station testbed with the caching assembly, which gave the flight software early runtime against real hardware at a point in the project when changing the software and the algorithms was still comparatively cheap [2]. Engineering model testing of the arm ran August 2018 to January 2019 covering requirements, preloading, docking and fault protection, engineering model caching assembly testing followed from December 2018, and the flight model caching assembly was run in a Mars-like thermal vacuum chamber in late 2019 and early 2020.

What the defect record says the testing misses

The one quantitative study of the question analyzed 199 critical post-launch anomalies across seven spacecraft, Galileo, Mars Global Surveyor, Cassini and Huygens, Deep Space 1, Mars Climate Orbiter, Mars Polar Lander and Stardust, using orthogonal defect classification: when the defect occurred, the trigger condition that surfaced it, the high-level entity fixed, and the actual fix [7]. Two results were unexpected to the authors. Outdated or missing procedures were involved in one fifth of the critical incidents, so the fix was to documentation rather than to code. And requirements changes were rarely because a previous requirement was wrong; they were new requirements for handling rare events or for compensating for hardware failures and degradation that had not been anticipated.

The same study found more problem reports classified as “nothing fixed” than expected. Those false positives, where test personnel believed the flight software was wrong when it was correct, turned out to forecast where operational personnel would later be confused: 311 developmental problem reports from MER avionics integration and test and assembly test and launch operations between April 2002 and January 2003 were analyzed on that basis, and the reports identified which features needed targeted training and documentation before launch [7]. The finding is about the operators rather than about the code.

Simulation as a design discipline, and as a credibility question

Event-driven simulation extends the workstation idea to distributed spacecraft. A hybrid continuous-time and discrete-event environment runs compiled flight software as a shared library with modeled scheduling, I/O and heap, and was used for 33 months on the VISORS guidance, navigation and control software and the Stanford RPO Kit; it averaged 9.53 s of wall time for 20.05 h of simulated time, about 7500 times real time, and it found a dynamic memory exhaustion defect against VISORS’s 50 MB limit, after whose sparse matrix fix the science campaign ran with about a 20 times memory margin [20]. Hardware validation was one processor-in-the-loop test on ARMv6 boards, not the flight computer, and the heap model is deliberately conservative rather than the flight allocator [20]. The work covers Earth orbit only, with no surface or rover application.

Model-based executable specifications are a laboratory-stage alternative to a hand-built simulator. A JPL feasibility experiment modeled a Remote Engineering Unit and its command path in SysML with JavaScript logic in the activity and state machine nodes, and ran the same test cases on the model and on an avionics testbed [24]. The tooling suited system and mission-scenario modeling but not hardware logic below the box level, and the event-stepped clock was dominated by the 8 Hz bus controller messaging rate, with roughly millisecond time scales out of reach. The paper shows no comparison results, and fault behaviors were drawn in static diagrams and never enacted in simulation code [24].

A simulation result is only as good as the evidence for the simulation. NASA-STD-7009B defines a Credibility Assessment Scale in two parts, one for model capability (data pedigree, verification, validation, technical review, process management) and one for results (use assessment, input pedigree, uncertainty characterization, robustness, review, process management) [19]. It sets no numeric accuracy threshold; the one quantified factor pegs “few”, “many” and “most” parameters at under 20, 20 to 50 and over 50 percent [19]. The cost of an under-characterized simulator shows in the SSDEV record: multiple person-months went to deciding whether a bug was in the flight software or in the test environment, and the stubbed motor controllers differed from flight ones in ways that surfaced only on flight-like avionics [2].

Rover autonomy has a second validation gap that simulators do not close, terrain. A Mars Exploration Rover-era argument holds that engineering-model cost and criticality-driven conservatism keep flight rovers out of rough analogue terrain, that the JPL sandbox and MarsYard facilities were flat and too short for long-traverse trials, and that under-validated autonomy then goes unused [21]. That paper reports no measurement; the argument is from project experience [21].

Verification of flown behavior on another planet

Self-collision checking on Mars 2020 shows what a flight record can and cannot establish. The Rover Collision Model executed 33,862 checks in the first 210 sols, 21,248 for the arm and 12,614 for SuperCam laser firing, with no unexpected check errors, and detected 594 arm and 214 laser calibration target intersections, all deliberate [23]. Zero errors is not a false negative rate: the only evidence of no missed collision is the absence of reported damage, and the one collision the model missed was caught by a human in sequence review [23]. The margins are defaults, 1.5 cm for the rover and 3 mm for close-clearance operations, with no derivation from measured uncertainty.

Scenario-based and model-based validation of autonomy

Exhaustive sequence testing is infeasible for planners. The Remote Agent Experiment on Deep Space 1 reduced the planner’s input space to 12 canonical initial states and 10 plan-start-time boundary points, with an experience-based upper bound of 200 to 300 plan-request scenarios for one tester with an automated scenario runner, plus 22 system-level execution scenarios and several hundred more for the executive and the model-based diagnosis engine [11]. That paper was written before the May 1999 flight test; it describes the plan, not defect-detection rates, and the authors state the approach will not scale to larger missions unchanged [11]. A contrary position holds that autonomy verification is not fundamentally harder than conventional spacecraft software verification, since no non-trivial software can be exhaustively tested and both rely on partitioning state space into equivalence classes [13]. That paper is argument, with no experiment [13].

Model checking was applied to a dually redundant spacecraft controller with checkpoint and rollback in a late 1990s JPL and West Virginia study: the detailed model had too many states to check, and manual abstraction to a partial specification brought it to a few hundred thousand states [12]. JPL’s later assurance research is reviewed in the same source, which concludes testing does not scale to autonomy; that conclusion is the authors’ opinion and the numbers are secondhand [12]. Model-based fault diagnosis was taken furthest on the ASTERIA CubeSat attitude control system, where more than 7 million archived coarse sun sensor telemetry points ran through the diagnosis engine and the star tracker model raised no false positives on nominal data [16]. The flight demonstration was a plan, not a result, and the stated goal of estimating false positive and false negative rates produced no rate [16].

Formal methods: what was tried and what it yielded

Outside the flown record, formal methods have been tried on trial projects. A 1995 NASA guidebook reports six trials; the Space Shuttle Jet Select low-level specification covered 75 pages of requirements in roughly 6 work months and raised 46 requirements issues, mostly minor, while an abstract 3-page respecification with 24 proofs raised 6 [15]. The guidebook itself warns that rates cannot be computed from single-project trials, and the two productivity figures in it disagree [15]. The case for the approach in digital systems is arithmetic on the failure budget: a catastrophic failure condition on a civil transport aircraft is allowed 10^-9 per hour, while experiment can establish only 10^-4 to 10^-5 per hour for complex software, because the operational profile for rare events cannot be reproduced [14]. That argument concerns airborne systems under FAA guidance and does not transfer to a mission of different duration without redoing the arithmetic [14]. The 1988 NASA history of onboard computing documents verification and change management for the Shuttle software as a process; it is secondary and carries no defect data [18]. Residual defect rates quoted in the Chien survey run from 0.1 per thousand lines for Shuttle avionics software to 0.2 for leading commercial software, 1.4 for a broad survey and 5 to 55 for military systems, none measured there [10].

What a fault injection campaign can and cannot report

The reference measurement on fault detection and recovery in a fault-tolerant flight computer is the FTMP engineering model campaign: 21,055 pin-level stuck faults injected on eight card types in one of ten line replaceable units, of which 17,418 were detected, every detected fault correctly identified and recovered by purging the module and taking a spare or degrading, and an average system reconfiguration time of 82 ms, with per-card averages from 46 ms for the system bus controller to 113 ms for PROM [9]. The floor under that recovery time is not the voters but the configuration control task running in the 3.125 Hz rate group, which is the same reason a spacecraft whose fault response is a scheduled task recovers in tens of milliseconds rather than microseconds.

The report refuses to turn the remaining 17.3 percent into a coverage figure, and the refusal is the transferable part: unused gates inside a package and unused signal pins are undetectable and also harmless, no classification separating them from real misses was done, so no coverage number is stated at all [9]. Two card types are missing from the data set because the only socketed CMOS sample was destroyed in handling, everything was injected in one unit of ten, and a stuck pin is a hardware failure model rather than an upset, a latch that nothing monitors, or a common-mode design fault.

The comparison design is different: SIFT puts redundancy in software, with each processor reading its neighbors’ results and voting itself, so that fault masking, diagnosis and reconfiguration are ordinary programs; its reliability model targets 10^-9 failure probability per 10-hour flight with fault rates that the report states are assumptions to be determined by the test program [17]. For commercial processors the Remote Exploration and Experimentation fault model projects ground radiation data into upset rates, for example a predicted 0.170 parity-detectable upsets per day in a PowerPC 750 256 KB L2 cache on the Mars surface against 2.643 per day in interplanetary space at solar minimum [22]. Both numbers are predictions, and software-implemented fault injection cannot reach caches, which is why that work adds a cache contents estimator [22].

Verifying software whose behavior is not enumerable

The Mars 2020 onboard planner is the hardest case in the record because its output depends on the state the rover happens to be in. The verification campaign ran in spring 2022, after more than a year of Perseverance surface operations under the master and submaster scheme, and drew its scenarios from hundreds of sols of real planning [5]. Requirements were managed in DOORS Next Generation with a matrix linking each requirement to the verification activities providing its evidence, test setup and configuration were standardized in Jupyter notebooks, and the bulk of execution ran on WSTS at 6 times real time, with a lightweight planner simulator for cheaper cases, the Mission System Testbed for performance and thermal fidelity, and the Vehicle System Testbed for end-to-end runs. The planner entered primary operations on 5 October 2023 [5].

What the campaign explicitly could not cover is stated: the unbounded problem space of conditions the planner will meet in flight, which had to be constrained to a finite set of testable units; unknown deviations from predicted activity execution; and the behavioral uncertainty the flexible execution scheme introduces [5]. The anomalies closed during testing cluster around heating: managing onboard heating is difficult because temperatures must be monitored before heating starts, the thermal tables carry uncertainty, and heating can span a sleep cycle. The planner runs on a 133 MHz RAD750 rated at 266 MIPS, shared with the rest of the flight software [5].

Regression as the dominant cost after launch

Cassini’s methodology is the long-duration case: attitude control flight software implementation began in 1993, the launch load completed in 1997, and the prime mission ran from July 2004 [6]. Pre-launch testing was a ten-step sequence from requirements trace matrices through test plans, case design, test trace matrices, procedures, a readiness review, execution, anomaly reporting, analysis and reporting. Unit tests verified functions, modes and states and boundary conditions with interfaces stubbed; an integration baseline was configuration-controlled at the end of each phase; and acceptance testing verified the requirement test matrix with scenario and functional tests covering whatever the matrix did not.

The test environment was tiered like MSL’s but with real units mixed in. The flight software development simulator ran faster than real time on the same UNIX platform as the software; the subsystem test bench, and after launch the Cassini attitude control test station, ran real time with two flight computers, two inertial reference units, one real reaction wheel assembly plus simulated ones, and a simulated power subsystem; and the Integrated Test Laboratory ran system level in real time with two flight computers, two engineering flight computers, two stellar reference units, two Sun sensor assemblies, two main engine valve drivers, five engine gimbal actuators of which two were real, and two solid state recorders [6].

Each critical event got its own build and its own campaign: the A7 cruise build, then A8.6.7 for Saturn orbit insertion, A8.7.1 for probe release and relay, and A8.7.2 and its variants for the remainder of the prime mission [6]. Operations testing over the first two and a half years covered functionality and mission performance, stress testing to find the system’s limits, and review of uplink products and procedures. Full flight software uploads had become virtually non-existent by the prime mission, and the operating philosophy was conservative: do not change logic unless necessary. The same instinct governs the Mars 2020 phased delivery of onboard planning authority [5]. A project retrospective by a member of the operations team describes the same platform, a 1750A processor running object-oriented Ada, and its in-flight upload and patch methods over an eleven-year prime mission [25]. Its change counts are project estimates with no defect rate normalized to size, and it applies to that platform rather than to modern flight processors [25].

Testbeds that are not computers

The Phoenix lander’s Payload Interoperability Testbed at the University of Arizona held a near-duplicate lander and arm and served a purpose no software simulator does: image comparison [8]. Before a sample delivery, the scoop was positioned over the selected instrument inlet port, a Robotic Arm Camera image was taken, and it was overlaid on an image of the same pose taken in the testbed, with positioning corrected from the difference. The testbed image is the reference the flight image is judged against, and no model substitutes for it because the discrepancy being looked for is exactly what the model does not know.

Recent work, 2025 to 2026

Flown: the Mars 2020 Simple Planner onboard planner was deployed on Perseverance on 5 October 2023 after a verification and validation campaign; the source is a briefing deck and gives no test case counts, pass rates or measured runtimes [27]. The ENav autonomous navigation algorithm verified by Monte Carlo simulation and Mars Yard testing had driven 32.1 km at an average of 92 m/h through sol 1312 [35]. The first on-orbit demonstration of a reinforcement-learned controller replaced the Astrobee wrench controller on the ISS after a path through Isaac Lab training, the Ames Gazebo simulator and an air-bearing table; only the curriculum-trained policy was flown [31].

Ground-tested: SPLICE hazard detection flight software was run on real lidar elevation maps from a March 2025 helicopter campaign at Kennedy Space Center, scored against a 1 cm per pixel photogrammetry survey, but on three post-processed maps from one site [29]. The MEXEC framework for the Endurance lunar rover concept was extended to manage battery and thermal state and tested in the Mars Yard, where the battery was physically swapped rather than recharged [30]. The SYNOPSIS science-autonomy library was integrated into cFS and F-Prime and exercised in NOS3 by replaying archived MSL data offline, with no onboard runtime, memory or power measurement [28].

Proposals and simulation only: temporal-logic-constrained test and schedule generation by SMT solving uses invented rover examples, not a built vehicle [26]. Hamilton-Jacobi reachability for perception-based controllers yields a sound backward reachable tube under a bounded perceptual error, shown only in simulation with an assumed error model [32]. A graceful degradation architecture with runtime fault injection has no processor, timing budget or flight software behind it [33]. Anomaly detectors for the Endurance rover trained on simulator-injected faults measure self-consistency with the generating simulator, not detection of real faults [34].

What each rung catches and misses

Method	Catches	Structurally misses
Workstation simulator	flight software logic, state machine interactions, fault responses to injected faults [3]	data content of instruments it models only in format [3]; real-time behavior, since it deliberately runs off real time [3]
Flight software in the loop with mechanism models	command sequence errors, state interaction defects, self-collision [1]	forces it averages from historical data rather than models [1]; instrument power, thermal and telecom behavior [1]
Hardware in the loop, brassboard	interface and timing behavior against real actuators early enough to change the algorithm [2]	microsecond-scale bus responses the simulation coordinates on time slices [2]
Flight-like vehicle	end-to-end behavior [5]	the state combinations that only a real mission produces [5]
Post-launch defect analysis	that one fifth of critical incidents trace to procedures, not code [7]	nothing, but only after the fact [7]

What is not established

No source in this set gives defect counts by venue, so the share of defects each rung finds is not known: the workstation simulator is credited with finding flight software defects but without a count or a hardware-testbed comparison [3], and SSDEV has no test hours or coverage figures [2]. Its fidelity gaps are documented by their consequences, not characterized, so what else was under-modeled is unknown [2]. Flown autonomy verification is not quantified for effort or coverage in the one survey of it [10]. Formal method trial data is single-project and cannot support effectiveness rates [15]. Model-based diagnosis has no measured false positive or false negative rate on an operational mission [16]. The collision model has no accuracy measurement beyond absence of reported damage [23]. SysML-based executable models of avionics have no demonstrated match to hardware results and no enacted fault injection [24].

References

Verma, V. and Leger, C. (2019). SSim: NASA Mars Rover Robotics Flight Software Simulation . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{verma2019ssim,
  title = {SSim: NASA Mars Rover Robotics Flight Software Simulation},
  author = {Verma, Vandi and Leger, Chris},
  booktitle = {IEEE Aerospace Conference},
  pages = {1-11},
  address = {Big Sky, Montana},
  year = {2019},
  doi = {10.1109/aero.2019.8741862},
  abstract = {Each new Mars rover has pursued increasingly richer science while tolerating a wider variety of environmental conditions and hardware degradation over longer mission operation duration. Sojourner operated for 83 sols (Martian days), Spirit for 2208 sols, and Opportunity is at 5111 sols, and Curiosity operation is ongoing at 2208 sols. To handle this increase in capability, the complexity of onboard flight software has increased. MSL (also known as Curiosity), uses more flight software lines of code than all previous missions to Mars combined, including both successes and failures[1]. MSL has more than 4,200 commands with as many as dozens of arguments, 54,000 parameters, and tens of thousands of additional state variables. A single high-level command may perform hours of configurable robotic arm and sampling behavior. Incorrect usage can result in the loss of an activity or the loss of the mission. Surface Simulation (“SSim”) was developed to address the challenge of making full and effective use of many capabilities of MSL, while managing complexity and risk. SSim is software that performs rapid context sensitive simulation of flight software. NASA Mars missions are comprised of three phases: several months of Cruise, a brief but exciting Entry Descent and Landing (EDL), and a Surface mission that typically lasts as long as the hardware survives. SSim is meant for use during the surface phase when the mission fulfills its primary objectives. The focus of SSim on MSL was the robotic flight software, including rover mobility and navigation, robotic arm manipulation, and sample acquisition, processing, and delivery. It can execute behaviors in simulation a thousand times faster than they execute in real time on the flight compute element. SSim is used by rover drivers to develop and validate command sequences throughout the planning cycle. SSim has been used to plan all of the Curiosity robotic operations since landing and is expected to continue to be used for the remaining life of the rover. Due to the impact of SSim on MSL, the Mars 2020 mission plans to increase the scope of SSim during flight operations, simulating not only rover planner operations, but all surface operations, including the instrument, power, thermal and telecommunication behavior. SSim is part of the Rover Sequencing and Visualization (RSVP) suite of Rover Planning tools [2]. In the paper we provide an overview of SSim architecture, design, implementation, and usage on MSL, as well as an overview of plans for Mars 2020.}
}

Brooks, S., Litwin, T., Biesiadecki, J., Abcouwer, N., Del Sesto, T., McHenry, M., Myint, S., Twu, P. and Wai, D. (2022). Testing Mars 2020 Flight Software and Hardware in the Surface System Development Environment . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{brooks2022testing,
  title = {Testing Mars 2020 Flight Software and Hardware in the Surface System Development Environment},
  author = {Brooks, Sawyer and Litwin, Todd and Biesiadecki, Jeffrey and Abcouwer, Neil and Del Sesto, Tyler and McHenry, Michael and Myint, Steven and Twu, Philip and Wai, Dennis},
  booktitle = {IEEE Aerospace Conference},
  pages = {1-13},
  address = {Big Sky, Montana},
  year = {2022},
  doi = {10.1109/aero53065.2022.9843794},
  abstract = {The Mars 2020 (M2020) Perseverance Rover is NASA's most advanced planetary rover mission to date. It includes a novel Sample Caching Subsystem (SCS) which will collect rock cores for possible future return to Earth, as well as an improved mobility system with enhanced autonomous navigation which will enable it to traverse faster and farther than prior rovers. The development of both systems required extensive flight software and flight hardware testing. To support this testing, we developed the Surface System Development Environment (SSDEV) and used it for a wide variety of testing. SSDEV is a bundled subset of M2020 Flight Software which runs on commercially available Linux computers and can be combined with multiple backend options for simulation and hardware control. The SSDEV architecture enabled our teams to perform much more testing of flight software and flight hardware than would have otherwise been possible. As a secondary benefit, the SSDEV-based test campaigns also helped our teams enter the operations phase of the mission with greater readiness of operations products and tools. In this paper, we summarize the motivation for SSDEV, provide an overview of the SSDEV architecture, list several examples of how SSDEV was used, and summarize lessons learned. SSDEV is not a substitute for integrated testing with flight-like avionics, but it enabled substantially more testing than would have otherwise been possible and also provided some unique benefits. We recommend architectures like SSDEV to future projects that need to perform extensive hardware and software testing using a limited set of flight-like avionics.}
}

Henriquez, D., Canham, T., Chang, J. T. and McMahon, E. (2008). Workstation-Based Avionics Simulator to Support Mars Science Laboratory Flight Software Development . AIAA SPACE Conference. Source

BibTeX

@inproceedings{henriquez2008workstation,
  title = {Workstation-Based Avionics Simulator to Support Mars Science Laboratory Flight Software Development},
  author = {Henriquez, David and Canham, Timothy and Chang, Johnny T. and McMahon, Elihu},
  booktitle = {AIAA SPACE Conference},
  year = {2008},
  doi = {10.2514/6.2008-6550},
  abstract = {The Mars Science Laboratory developed the WorkStation TestSet (WSTS) to support flight software development. The WSTS is the non-real-time flight avionics simulator that is designed to be completely software-based and run on a workstation class Linux PC. This provides flight software developers with their own virtual avionics testbed and allows device-level and functional software testing when hardware testbeds are either not yet available or have limited availability. The WSTS has successfully off-loaded many flight software development activities from the project testbeds. At the writing of this paper, the WSTS has averaged an order of magnitude more usage than the project's hardware testbeds.}
}

Jones, J. D. and Lam, D. (2011). Mars Science Laboratory Flight Software Internal Testing . NASA Jet Propulsion Laboratory, Undergraduate Student Research Program Final Report. Source

BibTeX

@techreport{jones2011mars,
  title = {Mars Science Laboratory Flight Software Internal Testing},
  author = {Jones, Justin D. and Lam, Danny},
  institution = {NASA Jet Propulsion Laboratory, Undergraduate Student Research Program Final Report},
  year = {2011},
  url = {https://dataverse.jpl.nasa.gov/dataset.xhtml?persistentId=hdl:2014/43488}
}

Parjan, S. and Gaines, D. (2024). In OBP We Trust: Verification and Validation of the M2020 On Board Planner Flight Software . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{parjan2024obp,
  title = {In OBP We Trust: Verification and Validation of the M2020 On Board Planner Flight Software},
  author = {Parjan, Shreya and Gaines, Dan},
  booktitle = {IEEE Aerospace Conference},
  address = {Big Sky, Montana},
  year = {2024},
  doi = {10.48577/jpl.67lmez},
  abstract = {With a planned deployment to the Perseverance roverin October 2023, the Mars 2020 On Board Planner (OBP) flightsoftware (FSW) will allow the rover to conserve energy and au-tonomously perform more activities when surplus resources (i.e.energy, data volume, time) are available. This functionality iscritical to support efficient resource management and maximizethe productivity of the vehicle as the rover’s battery degradesover time, particularly as the Mars Sample Return mission(MSR) may rely on Perseverance to facilitate sample deliveryto the return lander. Up until OBP’s deployment, operatorshave used the Master/Sub-Master paradigm (M/SM) for allMars missions to-date, in which rigid plans are uplinked to therover based on highly conservative models of activity resourceconsumption and duration that can unnecessarily constrain on-board plans. Thus, OBP must be robust enough to merit thetrust of mission science and operations personnel and preservethe health and safety of the spacecraft. To this end, we havecompleted a thorough verification and validation (V&V) cam-paign of the first iteration of OBP that will be deployed to therover as part of new Simple Planner (SP) operations paradigm.The campaign heavily relied on software testing to ensure thatcore flight software capabilities were met and that the softwarecomprehensively covered potential edge cases. In this paper,we motivate the need for a thorough V&V campaign going intothe deployment of On Board Planner to the Perseverance rover,contextualize how OBP integrates with the rest of the vehicle’sflight software, and leverage three case studies to evidence howtesting provided critical support towards the successful infusionof onboard scheduling software on the rover.}
}

Wang, E. and Brown, J. (2007). Cassini's Test Methodology for Flight Software Verification and Operations . AIAA SPACE Conference. Source

BibTeX

@inproceedings{wang2007cassini,
  title = {Cassini's Test Methodology for Flight Software Verification and Operations},
  author = {Wang, Eric and Brown, Jay},
  booktitle = {AIAA SPACE Conference},
  year = {2007},
  url = {https://dataverse.jpl.nasa.gov/dataset.xhtml?persistentId=hdl:2014/41356}
}

Lutz, R. R. and Mikulski, I. C. (2003). Patterns of Software Defect Data on Spacecraft . NASA Office of Safety and Mission Assurance, Jet Propulsion Laboratory. Source

BibTeX

@techreport{lutz2003patterns,
  title = {Patterns of Software Defect Data on Spacecraft},
  author = {Lutz, Robyn R. and Mikulski, Ines Carmen},
  institution = {NASA Office of Safety and Mission Assurance, Jet Propulsion Laboratory},
  year = {2003},
  url = {https://dataverse.jpl.nasa.gov/dataset.xhtml?persistentId=hdl:2014/7132}
}

Bonitz, R., Shiraishi, L., Robinson, M., Carsten, J., Volpe, R., Trebi-Ollennu, A., Arvidson, R. E., Chu, P. C., Wilson, J. J. and Davis, K. R. (2009). The Phoenix Mars Lander Robotic Arm . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{bonitz2009phoenix,
  title = {The Phoenix Mars Lander Robotic Arm},
  author = {Bonitz, Robert and Shiraishi, Lori and Robinson, Matthew and Carsten, Joseph and Volpe, Richard and Trebi-Ollennu, Ashitey and Arvidson, Raymond E. and Chu, P. C. and Wilson, J. J. and Davis, K. R.},
  booktitle = {IEEE Aerospace Conference},
  pages = {1-12},
  organization = {Jet Propulsion Laboratory, California Institute of Technology},
  address = {Big Sky, Montana},
  year = {2009},
  doi = {10.1109/aero.2009.4839306},
  abstract = {The Phoenix Mars Lander Robotic Arm (RA) has operated for 149 sols since the Lander touched down on the north polar region of Mars on May 25, 2008. During its mission it has dug numerous trenches in the Martian regolith, acquired samples of Martian dry and icy soil, and delivered them to the Thermal Evolved Gas Analyzer (TEGA) and the Microscopy, Electrochemistry, and Conductivity Analyzer (MECA). The RA inserted the Thermal and Electrical Conductivity Probe (TECP) into the Martian regolith and positioned it at various heights above the surface for relative humidity measurements. The RA was used to point the Robotic Arm Camera to take images of the surface, trenches, samples within the scoop, and other objects of scientific interest within its workspace. Data from the RA sensors during trenching, scraping, and trench cave-in experiments have been used to infer mechanical properties of the Martian soil. This paper describes the design and operations of the RA as a critical component of the Phoenix Mars Lander necessary to achieve the scientific goals of the mission.}
}

Lala, J. H. and Smith, T. B. I. (1983). Development and Evaluation of a Fault-Tolerant Multiprocessor (FTMP) Computer. Volume III: FTMP Test and Evaluation . Charles Stark Draper Laboratory for NASA Langley Research Center, NASA CR-166073. Source

BibTeX

@techreport{lala1983development,
  title = {Development and Evaluation of a Fault-Tolerant Multiprocessor (FTMP) Computer. Volume III: FTMP Test and Evaluation},
  author = {Lala, Jaynarayan H. and Smith, T. Basil, III},
  number = {NASA CR-166073},
  institution = {Charles Stark Draper Laboratory for NASA Langley Research Center},
  year = {1983},
  url = {https://ntrs.nasa.gov/citations/19850022395},
  abstract = {The experimental test and evaluation of the Fault-Tolerant Multiprocessor (FTMP) is described. Major objectives of this exercise include expanding validation envelope, building confidence in the system, revealing any weaknesses in the architectural concepts and in their execution in hardware and software, and in general, stressing the hardware and software. To this end, pin-level faults were injected into one LRU of the FTMP and the FTMP response was measured in terms of fault detection, isolation, and recovery times. A total of 21,055 stuck-at-0, stuck-at-1 and invert-signal faults were injected in the CPU, memory, bus interface circuits, Bus Guardian Units, and voters and error latches. Of these, 17,418 were detected. At least 80 percent of undetected faults are estimated to be on unused pins. The multiprocessor identified all detected faults correctly and recovered successfully in each case. Total recovery time for all faults averaged a little over one second. This can be reduced to half a second by including appropriate self-tests.}
}

Chien, S. (2022). Formal Methods for Trusted Space Autonomy, Boon or Bane? . NASA Formal Methods. Source

BibTeX

@inproceedings{chien2022formal,
  title = {Formal Methods for Trusted Space Autonomy, Boon or Bane?},
  author = {Chien, Steve},
  booktitle = {NASA Formal Methods},
  series = {Lecture Notes in Computer Science},
  pages = {3-13},
  publisher = {Springer International Publishing},
  year = {2022},
  doi = {10.1007/978-3-031-06773-0_1}
}

Smith, B., Millar, B., Dunphy, J., Tung, Y., Nayak, P., Gamble, E. and Clark, M. (1999). Validation and Verification of the Remote Agent For Spacecraft Autonomy . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{smith1999validation,
  title = {Validation and Verification of the Remote Agent For Spacecraft Autonomy},
  author = {Smith, B. and Millar, B. and Dunphy, J. and Tung, Y. and Nayak, P. and Gamble, E. and Clark, M.},
  booktitle = {IEEE Aerospace Conference},
  pages = {449-468 vol.1},
  year = {1999},
  doi = {10.1109/aero.1999.794352},
  abstract = {The six-day Remote Agent Experiment (RAX) on the Deep Space 1 mission will be the first time that an artificially intelligent agent will control a NASA spacecraft. Successful completion of this experiment will open the way for AI-based autonomy technology on future missions. An important validation objective for RAX is implementation of a credible validation and verification strategy for RAX that also "scales up" to missions that make full use of spacecraft autonomy. Autonomous flight software presents novel and difficult testing challenges that traditional flight software (FSW) does not face. Since autonomous software must respond robustly in an immense number of situations, the all-paths testing approaches used for traditional FSW is not feasible. Instead, we advocate a combination of scenario-based testing and model-based validation. This paper describes the testing challenges faced by autonomous spacecraft commanding software, discusses the testing strategies and model-validation methods that we found effective for RAX, and argues that these methods will "scale up" to missions that make full use of spacecraft autonomy. Among the key challenges for validating autonomous systems such as the RAX are ensuring adequate coverage for scenario-based tests, developing methods for specifying the expected behavior, and developing automated tools for verifying the observed behavior against those specifications. Another challenge, also faced by traditional FSW, is the scarcity of high-fidelity test-beds. The test plan must be designed to take advantage of lower-fidelity test-beds without compromising test effectiveness.}
}

Feather, M. S. and Pinto, A. (2023). Assurance for Autonomy – JPL’s past research, lessons learned, and future directions . IEEE International Conference on Assured Autonomy. Source

BibTeX

@inproceedings{feather2023assurance,
  title = {Assurance for Autonomy – JPL’s past research, lessons learned, and future directions},
  author = {Feather, Martin S. and Pinto, Alessandro},
  booktitle = {IEEE International Conference on Assured Autonomy},
  pages = {97-105},
  year = {2023},
  url = {https://dataverse.jpl.nasa.gov/api/access/datafile/86750}
}

Gat, E. (2004). Autonomy software verification and validation might not be as hard as it seems . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{gat2004autonomy,
  title = {Autonomy software verification and validation might not be as hard as it seems},
  author = {Gat, E.},
  booktitle = {IEEE Aerospace Conference},
  pages = {3123-3128},
  year = {2004},
  doi = {10.1109/aero.2004.1368117},
  abstract = {The verification and validation of autonomy software is widely believed to be a challenging unsolved problem. To a certain extent this is true, but in this paper I argue that the problem is not nearly as severe as seems to be widely perceived. Many of the perceived hard problems in autonomy software V&V also exist for traditional software, and can be solved using many of the same methods and techniques used for traditional spacecraft software. In particular, the problem of intractably large state spaces exists for any nontrivial software system. This problem can be addressed for autonomy software in the same way that it has been addressed for traditional software: by decomposing the large state space into a tractable number of equivalence classes that exhibit qualitatively identical behavior, each one containing a large number of states.}
}

Rushby, J. (1995). Formal Methods and Their Role in Digital Systems Validation for Airborne Systems . SRI International, prepared for NASA Langley Research Center, NASA Contractor Report 4673 (SRI CSL-95-1), Contract NAS1-18969. Source

BibTeX

@techreport{rushby1995formal,
  title = {Formal Methods and Their Role in Digital Systems Validation for Airborne Systems},
  author = {Rushby, John},
  number = {NASA Contractor Report 4673 (SRI CSL-95-1), Contract NAS1-18969},
  institution = {SRI International, prepared for NASA Langley Research Center},
  year = {1995},
  url = {https://ntrs.nasa.gov/citations/19960008816},
  abstract = {This report is based on one prepared as a chapter for the FAA Digital Systems Validation Handbook (a guide to assist FAA certification specialists with advanced technology issues). Its purpose is to explain the use of formal methods in the specification and verification of software and hardware requirements, designs, and implementations; to identify the benefits, weaknesses, and difficulties in applying these methods to digital systems used in critical applications; and to suggest factors for consideration when formal methods are offered in support of certification. The presentation concentrates on the rationale for formal methods and on their contribution to assurance for critical applications within a context such as that provided by DO-178B (the guidelines for software used on board civil aircraft); it is intended as an introduction for those to whom these topics are new.}
}

NASA Office of Safety and Mission Assurance. (1995). Formal Methods Specification and Verification Guidebook for Software and Computer Systems, Volume I: Planning and Technology Insertion . National Aeronautics and Space Administration, NASA-GB-002-95. Source

BibTeX

@techreport{nasa1995formal,
  title = {Formal Methods Specification and Verification Guidebook for Software and Computer Systems, Volume I: Planning and Technology Insertion},
  author = {{NASA Office of Safety} and {Mission Assurance}},
  number = {NASA-GB-002-95},
  institution = {National Aeronautics and Space Administration},
  year = {1995},
  url = {https://ntrs.nasa.gov/citations/19980228002},
  abstract = {The Formal Methods Specification and Verification Guidebook for Software and Computer Systems describes a set of techniques called Formal Methods (FM), and outlines their use in the specification and verification of computer systems and software. Development of increasingly complex systems has created a need for improved specification and verification techniques. NASA's Safety and Mission Quality Office has supported the investigation of techniques such as FM, which are now an accepted method for enhancing the quality of aerospace applications. The guidebook provides information for managers and practitioners who are interested in integrating FM into an existing systems development process. Information includes technical and administrative considerations that must be addressed when establishing the use of FM on a specific project. The guidebook is intended to aid decision makers in the successful application of FM to the development of high-quality systems at reasonable cost. This is the first volume of a planned two-volume set. The current volume focuses on administrative and planning considerations for the successful application of FM.}
}

Nikora, A., Aleem, M., Mackey, R., Fesq, L., Chung, S., Kolcio, K., Prather, M. and Matthew, L. (2020). Demonstrating Assurance of Model-Based Fault Diagnosis Systems on an Operational Mission . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{nikora2020demonstrating,
  title = {Demonstrating Assurance of Model-Based Fault Diagnosis Systems on an Operational Mission},
  author = {Nikora, Allen and Aleem, Mishaal and Mackey, Ryan and Fesq, Lorraine and Chung, Seung and Kolcio, Ksenia and Prather, Maurice and Matthew, Litke},
  booktitle = {IEEE Aerospace Conference},
  pages = {1-16},
  publisher = {IEEE},
  year = {2020},
  doi = {10.1109/aero47225.2020.9172282},
  abstract = {Developers of robotic scientific and commercial spacecraft are trending towards use of onboard autonomous capabilities for responding quickly to dynamic environments and rapidly changing situations. These capabilities need to know the state of the spacecraft's health. Model-based fault diagnosis (MBFD) is an approach to estimating health by continuously verifying accurate behavior and diagnosing off-nominal behavior. Proper functioning of MBFD depends on 1) the quality of the diagnostic system model that is analyzed and compared to commands and onboard measurements to estimate a system's health state, and 2) the correct functionality of the diagnosis engine interrogating the model and comparing its analyses to observed system behavior. Our goal is to develop Verification and Validation (V&V) techniques for MBFD to provide future missions sufficient confidence in its functionality and performance to deploy it on the systems they develop. Our work has been focused on infusing the techniques we developed earlier to an operational mission. First, we are constructing diagnostic models of a spacecraft attitude control system and updating our diagnostic engine so they can be demonstrated aboard the Arcsecond Space Telescope Enabling Research in Astrophysics (ASTERIA) mission, an operational spacecraft for which experiments in autonomy are being planned and executed, using the V&V techniques we have previously developed to assure they are both correct and complete. Since it is nearing the end of its life, ASTERIA provides a unique opportunity to demonstrate MBFD since the monitored components are expected to fail. Our demonstration will give system developers additional confidence to make timely, informed MBFD deployment decisions. Second, we will be completing performance assessments of the diagnostic engine/diagnostic model ensemble both on the flight system and ground-based testbeds to gain confidence in MBFD's ability to run successfully in a spacecraft's resource-constrained environment without adversely affecting other on-board activities. Finally, we are capturing our experience in preparing this demonstration in a set of checklists and guidance documents. Current practice includes high-level institutional guidance documents and standards, but at a high level of abstraction that does not necessarily address specific MBFD concerns. The purpose of the new checklists is to provide future mission developers clear, unambiguous, procedure-oriented guidance on assuring MBFD. This paper describes our work in these areas. For the first area, we describe the diagnostic models and updated diagnostic engine that will be used for the on-board demonstration. We describe how the V&V techniques we developed earlier are used to assure model and engine correctness and completeness. For the second area, we identify the performance measurement and assessment techniques used to characterize the diagnostic engine and diagnostic models, and discuss the effect of measured performance on overall mission operation. Finally, we present the checklist and guidance documents and describe how they meet the goals of providing system developers with clear, unambiguous, procedure-oriented guidance on MBFD assurance. We show how the techniques we have developed map into those artifacts.}
}

Goldberg, J., Green, M. W., Kautz, W. H., Levitt, K. N., Melliar-Smith, P. M., Schwartz, R. L. and Weinstock, C. B. (1984). Development and Analysis of the Software Implemented Fault-Tolerance (SIFT) Computer . SRI International for NASA Langley Research Center, NASA CR-172146. Source

BibTeX

@techreport{goldberg1984development,
  title = {Development and Analysis of the Software Implemented Fault-Tolerance (SIFT) Computer},
  author = {Goldberg, Jack and Green, Milton W. and Kautz, William H. and Levitt, Karl N. and Melliar-Smith, P. Michael and Schwartz, Richard L. and Weinstock, Charles B.},
  number = {NASA CR-172146},
  institution = {SRI International for NASA Langley Research Center},
  year = {1984},
  url = {https://ntrs.nasa.gov/citations/19840010885},
  abstract = {SIFT (Software Implemented Fault Tolerance) is an experimental, fault-tolerant computer system designed to meet the extreme reliability requirements for safety-critical functions in advanced aircraft. Errors are masked by performing a majority voting operation over the results of identical computations, and faulty processors are removed from service by reassigning computations to the nonfaulty processors. This scheme has been implemented in a special architecture using a set of standard Bendix BDX930 processors, augmented by a special asynchronous-broadcast communication interface that provides direct, processor to processor communication among all processors. Fault isolation is accomplished in hardware; all other fault-tolerance functions, together with scheduling and synchronization are implemented exclusively by executive system software. The system reliability is predicted by a Markov model. Mathematical consistency of the system software with respect to the reliability model has been partially verified, using recently developed tools for machine-aided proof of program correctness.}
}

Tomayko, J. E. (1988). Computers in Spaceflight: The NASA Experience . NASA, NASA-CR-182505. Source

BibTeX

@techreport{tomayko1988computers,
  title = {Computers in Spaceflight: The {NASA} Experience},
  author = {Tomayko, James E.},
  number = {NASA-CR-182505},
  institution = {NASA},
  year = {1988},
  url = {https://ntrs.nasa.gov/citations/19880069935},
  abstract = {This book examines the computer systems used in actual spaceflight or in close support of it. Computer systems used in administration and in aeronautical and other research not directly related to spaceflight are ignored. Each chapter deals with either a specific program, such as Gemini or Apollo onboard computers, or a closely related set of systems, such as launch processing or mission control.. A glossary of computer terms is included.}
}

NASA. (2024). NASA-STD-7009B: Standard for Models and Simulations . NASA Office of the Chief Engineer. Source

BibTeX

@techreport{nasa2024models,
  title = {NASA-STD-7009B: Standard for Models and Simulations},
  author = {{NASA}},
  institution = {NASA Office of the Chief Engineer},
  year = {2024},
  url = {https://standards.nasa.gov/standard/nasa/nasa-std-7009}
}

Bell, T. and D'Amico, S. (2025). Event-Driven Simulation for Rapid Iterative Development of Distributed Space Flight Software . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{bell2025event,
  title = {Event-Driven Simulation for Rapid Iterative Development of Distributed Space Flight Software},
  author = {Bell, Toby and D'Amico, Simone},
  booktitle = {IEEE Aerospace Conference},
  pages = {1-19},
  year = {2025},
  doi = {10.1109/aero63441.2025.11068699},
  abstract = {This paper presents the design, development, and application of a novel space simulation environment for rapidly prototyping and testing flight software for distributed space systems. The environment combines the flexibility, determinism, and observability of software-only simulation with a level of fidelity and depth normally attained by real-time hardware-in-the-loop testing. Ultimately, this work enables an engineering process in which flight software is continuously improved and delivered in its final, flight-ready form, and which reduces the cost of design changes and software revisions with respect to a traditional linear development process. Three key methods not found in existing tools enable this environment's novel capabilities: first, a hybrid event-driven simulation architecture that combines continuous-time and discrete-event simulation paradigms; second, a design for lightweight application-layer software virtualization that allows executing compiled flight software binaries while modeling process scheduling, input/ output, and memory use; and third, high-fidelity models for the multi-spacecraft space environment, including for wireless communication, relative sensing such as differential GPS and cameras, and flight computer system health metrics like heap exhaustion and fragmentation. The simulation environment's capabilities are applied to the iterative development and testing of two flight-ready software packages: the guidance, navigation, and control software for the VISORS mission, and the Stanford Space Rendezvous Laboratory's software kit for rendezvous and proximity operations. Results from 33 months of flight software development demonstrate the use of this simulation environment to rapidly and reliably identify and resolve defects, characterize navigation and control performance, and scrutinize implementation details like memory allocation and inter-spacecraft network protocols.}
}

Tunstel, E. W. (2003). Autonomous mobility software validation challenges for planetary surface missions . Journal of Spacecraft and Rockets. Source

BibTeX

@article{tunstel2003autonomous,
  title = {Autonomous mobility software validation challenges for planetary surface missions},
  author = {Tunstel, Edward W.},
  journal = {Journal of Spacecraft and Rockets},
  publisher = {JPL Open Repository},
  year = {2003},
  url = {https://dataverse.jpl.nasa.gov/dataset.xhtml?persistentId=hdl:2014/7133}
}

Ferraro, R. and Some, R. (2002). REE radiation fault model: a tool for organizing and communicating radiation test data and constructing COTS based spaceborn computing systems . JPL Open Repository. Source

BibTeX

@inproceedings{ferraro2002ree,
  title = {REE radiation fault model: a tool for organizing and communicating radiation test data and constructing COTS based spaceborn computing systems},
  author = {Ferraro, R. and Some, R.},
  publisher = {JPL Open Repository},
  year = {2002},
  url = {https://dataverse.jpl.nasa.gov/dataset.xhtml?persistentId=hdl:2014/37184}
}

Verma, V., Huang, J., Bailey, P., Carsten, J. and Klein, D. (2022). Perseverance Rover Collision Model for a range of Autonomous Behaviors . IEEE Aerospace Conference. Source

BibTeX

@inproceedings{verma2022perseverance,
  title = {Perseverance Rover Collision Model for a range of Autonomous Behaviors},
  author = {Verma, Vandi and Huang, Justin and Bailey, Philip and Carsten, Joseph and Klein, Douglas},
  booktitle = {IEEE Aerospace Conference},
  pages = {1-18},
  publisher = {IEEE},
  year = {2022},
  doi = {10.1109/aero53065.2022.9843632}
}

Khan, M. O., Sievers, M. and Standley, S. (2012). Model-based verification and validation of spacecraft avionics . Infotech@Aerospace. Source

BibTeX

@inproceedings{khan2012model,
  title = {Model-based verification and validation of spacecraft avionics},
  author = {Khan, M. Omair and Sievers, Michael and Standley, Shaun},
  booktitle = {Infotech@Aerospace},
  publisher = {American Institute of Aeronautics and Astronautics},
  year = {2012},
  doi = {10.2514/6.2012-2555},
  abstract = {Verification and Validation (VV the norm for thermal and structural VV this experiment demonstrated such an approach is possible.}
}

Brown, J. (2008). Cassini Attitude Control Flight Software: From Development to In-Flight Operation . AIAA Guidance, Navigation, and Control Conference. Source

BibTeX

@inproceedings{brown2008cassini,
  title = {Cassini Attitude Control Flight Software: From Development to In-Flight Operation},
  author = {Brown, Jay},
  booktitle = {AIAA Guidance, Navigation, and Control Conference},
  volume = {88},
  year = {2008},
  doi = {10.2514/6.2008-6806},
  abstract = {The Cassini Attitude and Articulation Control Subsystem (AACS) Flight Software (FSW) has achieved its intended design goals by successfully guiding and controlling the Cassini-Huygens planetary mission to Saturn and its moons. This paper describes an overview of AACS FSW details from early design, development, implementation, and test to its fruition of operating and maintaining spacecraft control over an eleven year prime mission. Starting from phases of FSW development, topics expand to FSW development methodology, achievements utilizing in-flight autonomy, and summarize lessons learned during flight operations which can be useful to FSW in current and future spacecraft missions.}
}

Havelund, K. (2026). Testing and Verification of Autonomy with Temporal Constraints . Root. doi.org/10.48577/jpl.v1oaf7

BibTeX

@misc{havelund2026testing,
  title = {Testing and Verification of Autonomy with Temporal Constraints},
  author = {Havelund, Klaus},
  journal = {Root},
  year = {2026},
  doi = {10.48577/jpl.v1oaf7},
  abstract = {No abstract available.}
}

Chien, S. (2025). Mars 2020 Simple Planner: Trusted Autonomy on Mars . Root. doi.org/10.48577/jpl.rdbggx

BibTeX

@misc{chien2025mars,
  title = {Mars 2020 Simple Planner: Trusted Autonomy on Mars},
  author = {Chien, Steve},
  journal = {Root},
  year = {2025},
  doi = {10.48577/jpl.rdbggx},
  abstract = {No abstract available.}
}

Wronkiewicz, M., Doran, G., Lightholder, J., Hasnain, Z., Stockham, R., Brown, R. J., Zemerick, S. A. and Mandrake, L. (2026). A Flight-Ready Software Platform for Deploying Science Autonomy Onboard Spacecraft . IEEE Transactions on Aerospace and Electronic Systems. Source

BibTeX

@article{wronkiewicz2026flight,
  title = {A Flight-Ready Software Platform for Deploying Science Autonomy Onboard Spacecraft},
  author = {Wronkiewicz, Mark and Doran, Gary and Lightholder, Jack and Hasnain, Zaki and Stockham, Rex and Brown, Robert J. and Zemerick, Scott A. and Mandrake, Lukas},
  journal = {IEEE Transactions on Aerospace and Electronic Systems},
  volume = {62},
  pages = {3879--3890},
  year = {2026},
  doi = {10.1109/taes.2025.3650728},
  abstract = {Spacecraft exploring Earth and other bodies in the solar system are producing increasingly large and complex volumes of scientific data. Recently, the field of science autonomy has begun to develop data analysis algorithms to select, prioritize, and characterize science instrument data directly onboard the spacecraft. These data-derived insights can then inform downstream autonomous decisions like data prioritization to mitigate data bandwidth constraints. However, science autonomy development has largely focused on bespoke, instrument-specific algorithms; there are no generalized platforms for sharing reusable utilities or centralizing the operation of multiple science autonomy algorithms. To accelerate future development of flight-ready science autonomy, we developed a software package called Science Yield Improvement via Onboard Prioritization and Summary of Information System (SYNOPSIS). SYNOPSIS manages the execution of one or more science autonomy algorithms, stores their outputs in a centralized database, and prioritizes data even across multiple instruments. We simulated the use of SYNOPSIS with science autonomy algorithms to analyze and prioritize data collected by the Curiosity rover on Mars and integrated it into two popular flight software packages — core Flight System (cFS) and F-Prime — to ease infusion of future science autonomy algorithms. As opportunities for onboard data analysis grow with the volume and complexity of data, we expect that platform technologies like SYNOPSIS will facilitate future exploration of our solar system.}
}

Chen, P.-T., Liu, J. Y., Bocchino, R. L. J., Mendeck, G. F. and Vaughan, G. M. (2026). Hazard Detection Flight Software for Processing LIDAR Generated DEM . AIAA SciTech. Source

BibTeX

@inproceedings{chen2026hazard,
  title = {Hazard Detection Flight Software for Processing LIDAR Generated DEM},
  author = {Chen, Po-Ting and Liu, John Y. and Bocchino, Robert L., Jr. and Mendeck, Gavin F. and Vaughan, Geoffrey M.},
  booktitle = {AIAA SciTech},
  publisher = {JPL Open Repository},
  year = {2026},
  doi = {10.48577/jpl.d3e9iv},
  abstract = {Hazard Detection (HD) is an enabling technology for safe landing on planetary bodies when the lander hazard tolerance capability is at the resolution limit of orbital imagery. This situation is common to many planetary bodies in the Solar System including Moon and Mars. At these locations, an autonomous lander can utilize a Light Detection and Ranging (LIDAR) sensor to map the landing area and construct a Digital Elevation Map (DEM) in real-time. The HD software developed by the Safe and Precise Landing Integrated Capabilities Evolution (SPLICE) project is designed to process a DEM and identify safe landing locations in real-time. The hazard detection method is applicable to 4-legged lander geometry and is adaptable to different hazard tolerance and run time requirements. This paper discusses the hazard detection performance of the SPLICE HD software using DEMs generated by the SPLICE Hazard Detection LIDAR.}
}

Ingham, M., Rouquette, N., Ardito, S., Bandyopadhyay, S., Hasnain, Z., Hasseler, T., Huffman, B., Patterson, K., Rabideau, G. and Vaquero, T. S. (2026). Autonomous Onboard Planning, Execution and Resource Management for the Endurance Lunar Rover . AIAA SCITECH Forum. Source

BibTeX

@inproceedings{ingham2026autonomous,
  title = {Autonomous Onboard Planning, Execution and Resource Management for the Endurance Lunar Rover},
  author = {Ingham, Michel and Rouquette, Nicolas and Ardito, Steven and Bandyopadhyay, Saptarshi and Hasnain, Zaki and Hasseler, Tristan and Huffman, Bennett and Patterson, Katharine and Rabideau, Gregg and Vaquero, Tiago Stegun},
  booktitle = {AIAA SCITECH Forum},
  year = {2026},
  doi = {10.48577/jpl.gy1l0y},
  abstract = {The Endurance mission concept requires a lunar rover to drive roughly 2500 kilometers, maintaining a high rate of traverse on the order of 100 kilometers per lunar day. The long distance and high traverse rate of this proposed rover mission will require a system with unprecedented levels of onboard autonomy. Specifically, it will require onboard reasoning capabilities to provide management of critical state and resources, including power/energy and thermal state. To achieve the ambitious mission objectives, anomalies related to the system or the environment state will have to be overcome quickly, with limited ground-in-the-loop interruptions. In this paper, we review the architecture and implementation of system-level autonomy software that will enable the required responsive behavior, with particular focus on flexible execution functions provided by an onboard activity planning and execution capability called MEXEC (Multi-mission EXECutive). We introduce a new set of scenarios for the FY2025 field test campaign, in which our system-level autonomy software has been augmented with behavioral software providing power and thermal management functions. Finally, we present results from testing the new integrated autonomy capabilities, both in simulation and in field tests.}
}

Stewart, K. H., Chapin, S., Leontie, R. and Henshaw, C. G. (2025). Crossing the Sim2Real Gap Between Simulation and Ground Testing to Space Deployment of Autonomous Free-flyer Control . arXiv. Source

BibTeX

@article{stewart2025crossing,
  title = {Crossing the Sim2Real Gap Between Simulation and Ground Testing to Space Deployment of Autonomous Free-flyer Control},
  author = {Stewart, K. H. and Chapin, Samantha and Leontie, Roxana and Henshaw, Carl Glen},
  journal = {arXiv},
  year = {2025},
  doi = {10.1109/isparo66239.2025.11436888},
  abstract = {Reinforcement learning (RL) offers transformative potential for robotic control in space. We present the first on-orbit demonstration of RL-based autonomous control of a free-flying robot, the NASA Astrobee, aboard the International Space Station (ISS). Using NVIDIA's Omniverse physics simulator and curriculum learning, we trained a deep neural network to replace Astrobee's standard attitude and translation control, enabling it to navigate in microgravity. Our results validate a novel training pipeline that bridges the simulation-to-reality (Sim2Real) gap, utilizing a GPU-accelerated, scientific-grade simulation environment for efficient Monte Carlo RL training. This successful deployment demonstrates the feasibility of training RL policies terrestrially and transferring them to space-based applications. This paves the way for future work in In-Space Servicing, Assembly, and Manufacturing (ISAM), enabling rapid on-orbit adaptation to dynamic mission requirements.}
}

Lin, A., Pinto, A. and Bansal, S. (2026). Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis . International Design Engineering Technical Conferences and Computers and Information in Engineering Conference. Source

BibTeX

@inproceedings{lin2026robust,
  title = {Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis},
  author = {Lin, Albert and Pinto, Alessandro and Bansal, Somil},
  booktitle = {International Design Engineering Technical Conferences and Computers and Information in Engineering Conference},
  publisher = {JPL Open Repository},
  year = {2026},
  doi = {10.48577/jpl.t9lsz1},
  abstract = {As perception-based controllers for autonomous systems become increasingly popular in the real world, it is important that we can formally verify their safety and performance despite perceptual uncertainty. Unfortunately, the verification of such systems remains challenging, largely due to the complexity of the controllers, which are often nonlinear, nonconvex, learning-based, and/or black- box. Prior works propose verification algorithms that are based on approximate reachability meth- ods, but they often restrict the class of controllers and systems that can be handled or result in overly conservative analyses. Hamilton-Jacobi (HJ) reachability analysis is a popular formal verification tool for general nonlinear systems that can compute optimal reachable sets under worst-case system uncertainties; however, its application to perception-based systems is currently underexplored. In this work, we propose RoVer-CoRe, a framework for the Robust Verification of Controllers via HJ Reachability. To the best of our knowledge, RoVer-CoRe is the first HJ reachability-based frame- work for the verification of perception-based systems under perceptual uncertainty. Our key insight is to concatenate the system controller, observation function, and the state estimation modules to obtain an equivalent closed-loop system that is readily compatible with existing reachability frame- works. Within RoVer-CoRe, we propose novel methods for formal safety verification and robust controller design. We demonstrate the efficacy of the framework in case studies involving aircraft taxiing and NN-based rover navigation.}
}

Biberstein, J., Karaman, S., De Weck, O., Sternberg, D., Fesq, L., Kolcio, K. and Prather, M. (2026). Graceful Degradation of Spacecraft Capabilities with Simulated Component Failure . Intersociety Energy Conversion Engineering Conference. Source

BibTeX

@inproceedings{biberstein2026graceful,
  title = {Graceful Degradation of Spacecraft Capabilities with Simulated Component Failure},
  author = {Biberstein, Josef and Karaman, Sertac and De Weck, Olivier and Sternberg, David and Fesq, Lorraine and Kolcio, Ksenia and Prather, Maurice},
  booktitle = {Intersociety Energy Conversion Engineering Conference},
  publisher = {JPL Open Repository},
  year = {2026},
  doi = {10.48577/jpl.xbi72d},
  abstract = {Development of fault detection, identification, and recovery systems for space missions requires engineers to consider interactions among all spacecraft subsystems. These systems must be robust and rigorously tested so as to not cause harm to the spacecraft. Combined with the complexity of the interactions that must be considered, this leads to conservative approaches even in modern spacecraft where the system includes redundant components, yet the response to most faults is to transition to safe mode and wait for intervention from the ground. However, a single fault may not disable a spacecraft to an extent which precludes continued operation, especially in spacecraft with redundant components. In this case, transitioning to safe mode and waiting for human intervention leads to mission downtime which impacts spacecraft performance and could be avoided. In this work, we prototype a new framework for fault detection, identification, and recovery that introduces graceful degradation of spacecraft capability in the presence of component failure. To demonstrate our framework, we focus on the attitude control subsystem. We simulate using the syssim library, a software package that enables the modular modeling of arbitrary dynamical systems with a robust and expressive API for defining faults to be injected at runtime. The MONSID library — a model-based health assessment software based on the technique of constraint suspension developed by Okean Solutions — is used in the loop for fault detection and diagnosis. We evaluate the performance of this ensemble on a non-trivial cascading fault in a set of sensors associated with an attitude control system. Graceful degradation is demonstrated across groups of redundant components that allow the spacecraft to continue operation even when a single component, such as a reaction wheel or gyroscope, has failed.}
}

Claridge, S., Patterson, J., Hasnain, Z., Goel, A., Patterson, K., Rouquette, N. F., Wagner, C., Hasseler, T. D. and Ingham, M. D. (2026). Supervised and Unsupervised Methods for Detecting Anomalies in an Autonomous Long-range Lunar Rover . EUROPEAN CONFERENCE OF THE PROGNOSTICS AND HEALTH MANAGEMENT SOCIETY. Source

BibTeX

@inproceedings{claridge2026supervised,
  title = {Supervised and Unsupervised Methods for Detecting Anomalies in an Autonomous Long-range Lunar Rover},
  author = {Claridge, Sofie and Patterson, Jack and Hasnain, Zaki and Goel, Ashish and Patterson, Katharine and Rouquette, Nicolas F. and Wagner, Caleb and Hasseler, Tristan D. and Ingham, Michel D.},
  booktitle = {EUROPEAN CONFERENCE OF THE PROGNOSTICS AND HEALTH MANAGEMENT SOCIETY},
  publisher = {JPL Open Repository},
  year = {2026},
  doi = {10.48577/jpl.kqud0q},
  abstract = {Autonomous space systems must navigate complex environments and accomplish concurrent tasks without continuous input and supervision from human operators. Interactions between subsystems and with the environment may lead to unintended behavior, resulting in downtime, delays, goal degradation, loss of functionality, or even catastrophic failures. The Endurance mission concept requires a lunar rover to traverse thousands of kilometers over a long period of time (multiple years) across the South Pole-Aitken Basin on the far side of the Moon. Onboard system health management is required to detect and diagnose anomalies and faults that pose a risk to mission objectives. To this end, we propose training both unsupervised and supervised machine learning models to detect and diagnose anomalies onboard a rover over the courseof a mission, supported by a pipeline for anomaly data generation that enables training and evaluation. We generate synthetic anomaly signatures using a low-fidelity mission simulator which outputs labeled datasets to enable supervised learning. We present results from a field experiment in which we deploy this supervised model as a ROS network node in a rover-ground network. In parallel, we train unsupervised models to detect anomalies in the mobility system by training on experimental field data and present results which verify the ability to detect anomalies observed by field operators as well as anomalies which were not detected by the operators. Our work demonstrates how machine learning models can detect anomalies onboard by leveraging multiple data sources, including pre-launch test data and operational data from earlier phases of the mission, and provides a pathway for improving anomaly detection as a rover’s mission progresses.}
}

Toupet, O., Ono, M., del Sesto, T., Maimone, M. and McHenry, M. (2026). Enhanced Autonomous Navigation on the Perseverance Mars Rover . IEEE Transactions on Field Robotics. Source

BibTeX

@article{toupet2026enhanced,
  title = {Enhanced Autonomous Navigation on the Perseverance Mars Rover},
  author = {Toupet, Olivier and Ono, Masahiro and del Sesto, Tyler and Maimone, Mark and McHenry, Michael},
  journal = {IEEE Transactions on Field Robotics},
  volume = {3},
  pages = {83--124},
  year = {2026},
  doi = {10.1109/tfr.2025.3636366},
  abstract = {This paper presentsEnhanced Autonomous Navigation, orENav, the autonomous driving algorithm of NASA’s Mars roverPerseverance. A unique challenge for the autonomous driving ofPerseveranceis to meet strict safety and performance requirements in a highly uncertain environment with only a single-core CPU with extremely limited computing resources. ENav overcame this challenge with a novel two-stage path selection approach that balances the path optimality and computational efficiency, combined with a unique collision checking algorithm that conservatively approximates computationally expensive kinematic settling (Otsu et al., 2020). In addition, ENav provides robustness against slip by expanding the bounding boxes for wheels used by the collision check. These new features, together with FPGA-accelerated vision processing, enabledPerseveranceto autonomously drive on substantially more rock-dense terrains and increased the average daily driving distance by an order of magnitude compared to its predecessors, theCuriosity, Spirit, andOpportunityrovers. Perseverance has set several new records for autonomous driving on Mars, breaking those previously held by the Opportunity rover. As of the 1312th Martian day since landing, or 28 October 2024 on the Earth calendar, ∼90% of the 32.1 km of driving has used ENav to evaluate the terrain. This paper provides detailed documentation of the ENav algorithm, as well as its implementation, testing, deployment, and driving results on Mars.}
}