Using Lightweight Formal Methods to Validate a Key-value Storage Node in Amazon S3
pdf
| Abstract: This talk reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By “lightweight formal methods” we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time. Our approach decomposes correctness into independent properties, each checked by the most appropriate tool, and develops executable reference models as specifications to be checked against the implementation. |
Our work has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems, and has been extended by non-formal-methods exp
erts to check new features and properties as ShardStore has evolved.
James Bornholt is an assistant professor of computer science at the University of Texas at Austin and a visiting researcher at Amazon Web Services, where he works on automated reasoning for Amazon S3.
Tags:
License: CC-BY-NC-3.0
Submitted by Katie Dey
on