Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Assignment
Read the paper
Use of Formal Methods at Amazon Web Services
by Newcombe et al.
This is the first of many research papers we will be reading in our class.
If you have not had experience reading research papers, you might find it
useful to read a short two-page paper called
How to Read a Paper. It will help you
get the most out of the papers in this class.
Why are we reading this paper?
-
This paper reports on real-world use of formal methods to find
subtle bugs in distributed systems protocols. Excellent motivation
for why formal methods can be useful in the real world.
-
The paper shows the value of checking the design, as opposed to going
all the way to fully machine-checked verification of implementations.
-
Extremely well-written paper.
What to learn from this paper?
-
Get a sense of what formal methods are.
-
Understand why formal methods can be useful.
-
Motivate the potential of formal methods in one domain; the rest of the
class is more focused on research results, but also looks at a broader
class of applications, and focuses on verification of implementations.
Answer this question
The Amazon paper describes the experiences of the individual authors
with different systems they built at Amazon and specifying their
behavior using TLA+ or PlusCal. What is the value for the authors to
write specifications? Why is there a value to specification, even
though the authors don't verify that their implementations meets their
specifications?
