2018 journal article
Formal methods and finite element analysis of hurricane storm surge: A case study in software verification
SCIENCE OF COMPUTER PROGRAMMING, 158, 100–121.
author keywords: Formal methods; Model checking; Scientific computing; Earth and atmospheric sciences
TL;DR:
An ocean circulation model used in production and an extension made to it that offers substantial performance gains are looked at, and Alloy, a declarative modeling language with tool support and an automatic form of analysis performed within a bounded scope using a SAT solver is used.
(via Semantic Scholar)
UN Sustainable Development Goal Categories
11. Sustainable Cities and Communities
(Web of Science)
Source: Web Of Science
Added: August 6, 2018
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. • An application of formal methods in the context of scientific computing and large-scale physical simulation. • Development of models in Alloy for analyzing relevant parts of an ocean circulation model used in production. • Guarantees about soundness of an extension supported by the approach through experimentation and analysis.