Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy

Abstract

We describe an Alloy model that helps check the correctness of a discrete wet-dry algorithm used in a system for hurricane storm surge prediction. Derived from simplified physics and encoded with empirical rules, the algorithm operates on a finite element mesh to allow the propagation of overland flows. Our study is motivated by complex interactions between the algorithm and a recent performance enhancement to the system that involves mesh partitioning. We briefly outline our approach and describe safety properties of the extension, as well as directions for future work.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{BaughA16,
  author       = {John W. Baugh Jr. and
                  Alper Altuntas},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in
                  Alloy},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {256--261},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_18},
  doi          = {10.1007/978-3-319-33600-8\_18},
  timestamp    = {Sat, 30 Sep 2023 09:34:45 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BaughA16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}