{"id":2643,"date":"2011-09-23T12:28:27","date_gmt":"2011-09-23T16:28:27","guid":{"rendered":"http:\/\/www.easterbrook.ca\/steve\/?p=2643"},"modified":"2011-09-29T14:19:03","modified_gmt":"2011-09-29T18:19:03","slug":"formal-verification-for-climate-models","status":"publish","type":"post","link":"http:\/\/www.easterbrook.ca\/steve\/2011\/09\/formal-verification-for-climate-models\/","title":{"rendered":"Formal Verification for Climate Models?"},"content":{"rendered":"

Valdivino, who is working on a PhD in Brazil, on formal software verification techniques, is inspired by my suggestion<\/a> to find ways to apply our current software research skills to climate science. But he asks some hard questions:<\/p>\n

1.) If I want to Validate and Verify climate models should I forget all the things that I have learned so far in the V&V discipline? (e.g.\u00a0Model-Based Testing (Finite State Machine, Statecharts, Z, B), structural testing, code inspection, static analysis, model checking)
\n2.) Among all V&V techniques, what can really be reused \/ adapted for climate models?<\/p><\/blockquote>\n

Well, I wish I had some good answers.\u00a0When I started looking at the software development processes for climate models, I expected to be able to apply many of the [edit<\/span>] formal<\/span><\/em> techniques I’ve worked on in the past in Verification and Validation (V&V) and Requirements Engineering (RE). It turns out almost none of it seems to apply, at least in any obvious way.<\/p>\n

Climate models are built through a long, slow process of trial and error, continually seeking to improve the quality of the simulations (See here for an overview of how they’re tested<\/a>). As this is scientific research, it’s unknown, a priori<\/em>, what will work, what’s computationally feasible, etc. Worse still, the complexity of the earth systems being studied means its often hard to know which processes in the model most need work, because the relationship between particular earth system processes and the overall behaviour of the climate system is exactly what the researchers are working to understand.<\/p>\n

Which means that model development looks most like an agile software development process<\/a>, where the both the requirements and the set of techniques needed to implement them are unknown (and unknowable) up-front. So they build a little, and then explore how well it works. The closest they come to a formal specification is a set of hypotheses along the lines of:<\/p>\n

“if I change <piece of code> in <routine>, I expect it to have <specific impact on model error> in <output variable> by <expected margin> because of <tentative theory about climactic processes and how they’re represented in the model>”<\/p><\/blockquote>\n

This hypothesis can then be tested by a formal experiment in which runs of the model with and without the altered code become two treatments, assessed against the observational data for some relevant period in the past. The expected improvement might be a reduction in the root mean squared error for some variable of interest, or just as importantly, an improvement in the variability (e.g. the seasonal or diurnal spread).<\/p>\n

The whole process looks a bit like this (although, see Jakob’s 2010 paper<\/a> for a more sophisticated view of the process):<\/p>\n

\"\"<\/a>And of course, the central V&V technique here is full integration testing. The scientists build and run the full model to conduct the end-to-end tests that constitute the experiments.<\/p>\n

So the closest thing they have to a specification would be a chart such as the following (courtesy of Tim Johns at the UK Met Office):<\/p>\n

\"\"<\/a>This chart shows how well the model is doing on 34 selected output variables (click the graph to see a bigger version, to get a sense of what the variables are). The scores for the previous model version have been normalized to 1.0, so you can quickly see whether the new model version did better or worse for each output variable – the previous model version is the line at “1.0” and the new model version is shown as the coloured dots above and below the line. The whiskers show the target<\/em> skill level for each variable. If the coloured dots are within the whisker for a given variable, then the model is considered to be within the variability range for the observational data for that variable. Colour-coded dots then show how well the current version did: green dots mean it’s within the target skill range, yellow mean it’s outside the target range, but did better than the previous model version, and red means it’s outside the target and did worse than the previous model version.<\/p>\n

Now, as we know, agile software practices aren’t really amenable to any kind of formal verification technique. If you don’t know what’s possible before you write the code, then you can’t write down a formal specification (the ‘target skill levels’ in the chart above don’t count – these aspirational goals rather than specifications). And if you can’t write down a formal specification for the expected software behaviour, then you can’t apply formal reasoning techniques to determine if the specification was met.<\/p>\n

So does this really mean, as Valdivino suggests, that we can’t apply any of our toolbox of formal verification methods? I think attempting to answer this would make a great research project. I have some ideas for places to look where such techniques might be applicable. For example:<\/p>\n