A Formal Verification Approach for Measures of Effectiveness Based on Satisfiability Modulo Theories

Model-Based Systems Engineering (MBSE) provides a formal and integrated framework for managing multidisciplinary information throughout the system design lifecycle. Within this framework, Measures of Effectiveness (MOEs) serve as the key quantitative metrics for evaluating whether a system design meets mission requirements. Current approaches for verifying MOE constraints in MBSE typically rely on mathematical relationships established through SysML parametric diagrams, with metrics analysis performed using built-in computational plug-ins or external specialized software. However, these approaches face challenges in unified representation of multitheory hybrid constraints, automated exploration for feasible solutions, and tool-level data consistency. This limits the reliability and completeness of verification results. This paper proposes a formal verification approach for MOE by integrating the multi-architecture modeling language KARMA with Satisfiability Modulo Theories (SMT). The approach provides a unified firstorder logic (FOL) representation of MOE-related metrics. It also automates the evaluation of SysML parametric diagrams through SMT solver, enabling constraint satisfiability checking and reverse derivation of optimal design solutions. A satellite electric power system (EPS) case study demonstrates the feasibility and effectiveness of the proposed approach. The results show that the approach ensures the consistency between system metrics and requirements, and improves automation and completeness of MOE verification within the MBSE framework.