Quantitative Validation of Formal Domain Models

Application of formal methods to verification of well-formedness and semantic correctness of data sets from a particular domain becomes increasingly practical with the advances in automated verification tools. However, it is difficult for domain experts to understand and formulate formal verification constraints (VCs), yet much trust is invested in their validity and completeness. The paper discusses a novel validation approach based on statistical testing of VCs against pre-validated data sets. We illustrate the proposed technique using a synthetic railway example and also relate our experience of integrating the approach within a large-scale industry-based project.