Formal methods and finite element analysis of hurricane storm surge: A case study in software verification

Used to predict the effects of hurricane storm surge, ocean circulation models are essential tools for evacuation planning, vulnerability assessment, and infrastructure design. Implemented as numerical solvers that operate on large-scale datasets, these models determine the geographic extent and severity of coastal floods and other impacts. In this study, we look at an ocean circulation model used in production and an extension made to it that offers substantial performance gains. To explore implementation choices and ensure soundness of the extension, we make use of Alloy, a declarative modeling language with tool support and an automatic form of analysis performed within a bounded scope using a SAT solver. Abstractions for relevant parts of the ocean circulation model are presented, including the physical representation of land and seafloor surfaces as a finite element mesh, and an algorithm operating on it that allows for the propagation of overland flows. The approach allows us to draw useful conclusions about implementation choices and guarantees about the extension, in particular that it is equivalence preserving.