Towards Modelling and Verification of Coupler Behaviour in Climate Models
summary
Argues for inserting dynamic runtime contracts at coupler boundaries to catch unit mismatches, timing and routing errors before they propagate; extracts verifiable modules (configuration, field registration, grid manager/interpolation, time synchronization, data-routing) and encodes pre/post/invariant checks. Prototype retrofits Fortran via ISO_C_BINDING to a C runtime-verifier, targets the Oasis coupler, demonstrates how one real bug would have been detected, cites Los Alamos $15M migration estimate, and measures an estimated 2–4x runtime overhead.
AI-written summary · about
chapters (8)
- 0:00Climate model couplers intro
- 3:11Verification critical for couplers
- 6:40Coupler design tasks
- 9:08Modular contracts for verification
- 12:38Dynamic contract verification
- 15:09Benefits of verifiable modules
- 16:36Next steps for frameworks
- 18:00Questions and discussion
related talks
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
22mFormal Runtime Error Detection During Development in the Automotive Industry
01h 01mNetwork Verification: Past, Present, and Future
22mVerification Modulo Tested Library Contracts
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
01h 16mPolymorphism, Cohesion, and Coupling in C++
30mTrustworthy Runtime Verification via Bisimulation
38mThe Verification of a Distributed System