Using lightweight formal methods to validate a key-value storage node in Amazon S3 By James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Ge ff en, Andrew War fi eld
Three views on durability 9 Section Sequential Crash-free “4 Conformance Checking” Sequential With crashes “5 Checking Crash Consistency” Concurrent Crash-free “6 Checking Concurrent Executions” Concurrent With crashes Out of scope