Property Testing for Ocean Models. Can We Specify It? (Invited Talk)

Basic Information

• Paper ID: 2510.13692
• Title: Property Testing for Ocean Models. Can We Specify It? (Invited Talk)
• Author: Deepak A. Cherian (Earthmover PBC)
• Classification: cs.SE
• Conference: International Workshop on Verification of Scientific Software (VSS 2025)
• Journal: EPTCS 432, 2025, pp. 48–59
• Paper Link: https://arxiv.org/abs/2510.13692

Abstract

Drawing inspiration from the property testing literature, particularly the work of Professor John Hughes, the author explores how these ideas can be applied to ocean numerical models. Specifically, the research investigates whether geophysical fluid dynamics (GFD) theory can be expressed as property testing to address the oracle problem in ocean model correctness testing. The author proposes a series of simple idealized GFD problems that can be framed as property tests, clearly demonstrating how physics naturally lends itself to specifying property tests.

Research Background and Motivation

Core Problems

1. The Oracle Problem: The fundamental challenge in testing ocean/climate models is the lack of an "oracle" to determine the correctness of numerical solutions
2. Model Complexity: Earth system models are extremely complex, containing multiple coupled components including atmosphere, ocean, and land
3. Testing Method Limitations: Existing testing primarily relies on regression testing and reference solution comparison, suffering from "compensating errors" problems

Research Significance

• Climate model predictions form the scientific basis of IPCC reports
• Model correctness directly impacts climate change adaptation and mitigation strategies
• The uniqueness of solutions to ocean model governing equations (Navier-Stokes equations) remains unproven

Limitations of Existing Approaches

• Heavy reliance on regression testing and bit-for-bit reproducibility
• Reference solution methods limited to specific initial value problems
• Compensating errors may mask real bugs
• Lack of systematic dynamical correctness verification

Core Contributions

1. Theoretical Framework: First systematic application of property testing concepts to ocean model verification
2. Physical Property Mapping: Transformation of geophysical fluid dynamics theory into testable property specifications
3. Testing Classification System: Construction of an ocean model testing framework based on John Hughes's five categories of property testing guidance principles
4. Practical Test Cases: Proposal of multiple specific GFD problems as property testing instances
5. Interdisciplinary Methodology: Bridging computer science property testing with geophysical theory

Methodology Details

Task Definition

Transform the correctness verification problem of ocean numerical models into property testing problems based on physical laws, with inputs being model configurations and initial conditions, and outputs being boolean judgments satisfying specific physical properties.

Core Methodological Framework

The author follows John Hughes's five categories of property testing guidance principles:

1. Invariant Testing

Physical Conservation Laws:

• Mass (volume) conservation
• Energy conservation
• Angular momentum conservation
• Potential vorticity conservation

Symmetry Testing:

• Galilean invariance: Solutions remain unchanged under constant velocity frame translation
• Rotational symmetry: Solutions remain invariant after 90° multiple domain rotations
• Scale invariance: Solution invariance under specific parameter scaling

Balanced Flow Preservation: Geostrophic balance relationship:

f u = -1/ρ ∂p/∂y
f v = 1/ρ ∂p/∂x

where f is the Coriolis parameter, u,v are velocity components, p is pressure, and ρ is density.

Wave Solution Dispersion Relations: Internal waves in rotating stratified fluids satisfy:

ω² = (f²m² + N²(k² + l²))/(k² + l² + m²)

where ω is frequency, (k,l,m) are wavenumber vector components, and N is the buoyancy frequency.

2. Postcondition Testing

Resonant Frequency Response:

• Energy input at resonant frequencies should produce strong motion
• Non-resonant frequency input should decay rapidly

Boundary Asymmetry Response: On the β-plane, energy input at western and eastern boundaries should produce wave responses of different scales, reflecting the east-west asymmetry of Rossby waves.

3. Metamorphic Relation Testing

Parameter Dependency Relations:

• Doubling the β parameter should double Rossby wave phase speed
• Changes in stratification parameter N should affect wave speed according to dispersion relations

Dynamical Similarity: When the control parameter λ = Uk/β remains constant, different combinations of U, k, β should produce similar solutions.

4. Model-based Properties

Using simplified analytical or numerical models as references:

• Analytical dispersion relation verification
• Exact solutions in simplified geometries
• Known solutions for idealized configurations

Technical Innovations

1. Systematization of Physical Constraints: Systematic transformation of complex GFD theory into verifiable properties
2. Multi-scale Testing Strategy: Hierarchical testing from simple equilibrium states to complex transient processes
3. Transient Process Handling: Addressing complex dynamics through balanced flows and known transient characteristics
4. Cross-domain Methodology: Deep integration of computer science testing theory with geophysics

Experimental Setup

Theoretical Verification Framework

The author proposes a conceptual framework without specific numerical experiments, but describes implementation strategies:

Test Domain Configuration:

• Simplified geometry: rectangular ocean basin, flat bottom
• Idealized boundary conditions
• f-plane or β-plane approximation

Initial Condition Generation:

• Geostrophically balanced flow fields
• Analytical wave solutions
• Specific equilibrium configurations

Verification Metrics:

• Relative errors in conserved quantities
• Deviations in balance relationships
• Consistency of wave characteristics with theoretical predictions

Current Model Testing Status

The paper surveyed testing methods of major ocean models:

• MIT General Circulation Model (MITgcm)
• Regional Ocean Modeling System (ROMS)
• Modular Ocean Model (MOM6)
• Coastal and Regional Ocean Community Model (CROCO)

Experimental Results

Theoretical Analysis Results

Identification of Existing "Novel Tests": Two property tests already implemented in MOM6:

1. Dimensional consistency assertions
2. Domain rotation invariance testing

Physical Property Richness: Identification of numerous GFD theories convertible to property tests, including:

• Multiple types of balanced flows
• Wave solutions of varying complexity
• Various conservation laws and symmetries

Feasibility Analysis

Advantages:

• Physics naturally provides rich property specifications
• Many proposed tests already exist as example problems in existing models
• Solid theoretical foundation with analytical solutions

Challenges:

• Complexity in handling transient motion
• Computational cost control
• Difficulty in designing shrinking strategies

Related Work

Current Climate Model Testing Status

• Regression Testing: Strict bit-for-bit reproducibility requirements
• Reference Solution Comparison: Standard testing cases for atmospheric models
• Model Intercomparison: Comparative verification across different models

Formal Methods Applications

• Altuntas and Baugh using hybrid theorem provers for KPP parameterization testing
• Lightweight formal methods beginning to be applied to climate model subcomponents

Property Testing Development

• Proliferation of QuickCheck libraries
• Application of metamorphic testing in scientific computing
• Use of Hypothesis library in scientific Python ecosystem

Conclusions and Discussion

Main Conclusions

1. Feasibility Confirmation: Geophysical fluid dynamics theory naturally lends itself to expression as property tests
2. Rich Testing Sources: GFD provides abundant dynamical properties convertible to tests
3. Practical Value: Many proposals already used as example problems in existing models
4. Systematization Requirements: Need to systematize scattered physical knowledge into testing frameworks

Limitations

1. Transient Handling: Processing of complex transient motion remains a core challenge
2. Computational Cost: Computational overhead of long-term integration is limiting
3. Shrinking Strategies: How to design test case shrinking methods that preserve physical assumptions
4. Implementation Complexity: Requires modular code architecture supporting subcomponent testing

Future Directions

1. Concrete Implementation: Development of actual property testing suites
2. Cost Optimization: Exploration of strategies to reduce computational costs
3. Shrinking Algorithms: Design of test case shrinking methods suitable for physical systems
4. Effectiveness Evaluation: Determination of which tests are most effective at finding bugs

In-Depth Evaluation

Strengths

1. Strong Innovation: First systematic introduction of property testing to ocean model verification
2. Solid Theoretical Foundation: Based on mature GFD theory and property testing methodology
3. High Practical Value: Addresses the actual oracle problem in ocean model testing
4. Interdisciplinary Vision: Successfully bridges computer science and geophysics
5. Strong Systematicity: Complete framework following Hughes's five guidance categories

Weaknesses

1. Lack of Empirical Verification: Paper is primarily theoretical, lacking actual implementation and effectiveness validation
2. Operability Unverified: Feasibility of proposed methods in actual large-scale models remains unknown
3. Insufficient Cost Analysis: Shallow analysis of computational overhead and implementation complexity
4. Limited Coverage: Primarily focuses on dynamical core, with limited coverage of parameterizations and subcomponents

Impact

1. Academic Value: Provides new perspectives for scientific computing software verification
2. Practical Guidance: Provides testing methodology for ocean model developers
3. Cross-domain Contribution: Promotes application of formal methods in earth sciences
4. Long-term Significance: Contributes to improving credibility of climate models

Applicable Scenarios

1. Ocean Model Development: Verification testing during new model development
2. Model Upgrade Verification: Correctness checking after existing model modifications
3. Cross-model Comparison: Consistency verification across different models
4. Teaching and Research: Comparative learning of GFD theory and numerical implementation

References

The paper cites 41 references, primarily including:

• Property Testing Foundations: Claessen & Hughes (2000) QuickCheck original paper
• GFD Theory: Classic textbooks by Gill (1982), Pedlosky (1987), Vallis (2017)
• Ocean Models: Technical documentation and testing protocols of major ocean models
• Formal Methods: Applications in climate models by Altuntas & Baugh (2018)

Overall Assessment: This is a groundbreaking paper that successfully introduces property testing, a computer science concept, to ocean model verification. While lacking actual implementation, it provides a solid theoretical foundation and clear implementation pathway, with significant value for advancing formal verification of scientific computing software. The paper's interdisciplinary perspective and systematic thinking are commendable and establish a good foundation for subsequent research.