Abstract
Satellite systems consist of multiple interdependent subsystems whose failure dynamics frequently deviate from the exponential assumption and are more accurately captured by Weibull distributions derived from empirical on-orbit data. However, these non-exponential behaviors are inherently incompatible with Continuous-Time Markov Chain (CTMC) models that underpin probabilistic verification tools such as PRISM. Although phase-type approximations (e.g., Erlang, hyper-exponential) provide a means to embed general lifetime distributions into CTMCs, existing applications typically target small-scale or domain-agnostic models and offer limited guidance for aerospace reliability analysis. This paper bridges Weibull-based reliability modeling and CTMC verification by introducing an automated, reproducible workflow for phase-type encoding of semi-Markov failure models into PRISM. Leveraging symbolic state-space reduction and modular model construction, the proposed framework embeds fitted phase-type distributions directly into CTMC-compatible models, preserving fidelity to empirical degradation data while maintaining computational tractability. We evaluate the approach across representative satellite subsystems, verifying time-bounded reliability properties under realistic mission profiles. Experimental results demonstrate accurate reliability estimation with substantially mitigated state-space explosion, providing a practical pathway for applying probabilistic model checking to large-scale, non-Markovian aerospace systems.