Bridging Weibull Failure Models and CTMC Verification: Automated Phase-Type Encoding for Satellite Reliability Analysis in PRISM

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.