mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
10 lines
372 B
TeX
10 lines
372 B
TeX
\section{Layer 6: Model Checking (TLA+)}
|
|
|
|
|
|
Covered in our companion paper on TLA+. In the testing pyramid, model checking sits
|
|
above fault injection because it reasons about the protocol \emph{design}, not the
|
|
implementation. It catches bugs that exist in every correct implementation of a flawed
|
|
protocol.
|
|
|
|
%% ============================================================
|