Software Project Effort Estimation Using Formal Method and Model Checker

Software project effort estimation is a critical component of software development, as it determines the time and financial resources required to complete a project. Existing estimation techniques—ranging from empirical models and algorithmic methods to heuristic and expert-based approaches—struggle with inconsistent accuracy due to the inherent complexity, subjectivity, and contextual variability across software projects. Although earlier formal methods aimed to reduce confusion by being very precise, they usually don't allow for automated logical analysis or check if the assumptions used for estimation are consistent with one another. To address these limitations, this study introduces a novel formal modeling framework that integrates Z-Specification with the Z3 SMT solver to both formalize and computationally verify effort estimation models. The use of Z notation guarantees the meaning is precise and unambiguous. Furthermore, SMT (Satisfiability Modulo Theories) reasoning adds powerful new abilities that older methods lacked. These new capabilities include automatically finding constraint violations, confirming how parameters depend on one another, and determining feasible estimation ranges under clearly defined conditions. This integration not only reduces ambiguity but also provides a verifiable, machine-checkable basis for evaluating, refining, and comparing diverse effort estimation methods, thereby offering a more robust foundation than traditional or solely formalized models.