Earth orbit is becoming increasingly crowded as commercial and governmental actors deploy large satellite constellations, raising challenges in verifying system-level requirements such as coverage, collision avoidance, and rendezvous reliability. These challenges are driven by uncertainty arising from orbital perturbations and limitations in sensing, estimation, and control, which result in a range of possible system behaviors rather than a single defined trajectory. While high-fidelity simulations and Monte Carlo methods are effective for validation, they are computationally expensive and ill-suited for rapid design exploration or formal guarantees.

This work proposes a contract-based framework for reasoning about space systems under uncertainty using assume-guarantee contracts. By modeling subsystems as composable components defined by assumptions and guarantees, the approach enables formal verification of system-level properties without reliance on exhaustive simulation. A key focus is the incorporation of orbital perturbations, specifically using the J2 model, into this framework. The paper introduces the necessary foundations in both contract-based design and astrodynamics, demonstrates contract synthesis using the Pacti library, and develops a perturbation-aware contract for orbital systems. Applications to representative mission scenarios illustrate how the method supports rigorous, scalable analysis of satellite system performance under uncertainty.

Currently pursuing my Master’s in Space Systems at the University of Michigan, I am also a researcher at the Complex Engineering Systems Laboratory (CESL). My work focuses on the development of formal systems engineering practices to solve the architectural challenges of next-generation space missions. I have industry experience in automotive where my expertise was in EV battery design.