AWSにおける形式手法 - 前書き(1/4) 論文を書いた動機

AWSの技術者が形式手法を導入した経緯と成果を論文に発表しています. この論文を少しづつ読み進めていきます. 前書きの第１段落を読んで, 私が理解できたことは次の通りです.

2011年から, AWSの技術者はシステム設計に関する困難な課題を解決するために,
形式手法とモデル検査を使ってきた. この論文では, 著者たちの動機と経験, つまり, 著者たちが抱えている問題に於いて,  何が上手くでき, 何が上手くできなかったかを述べている. 個人的な経験を述べる時は, 著者のイニシャルによりそれを示している.

この論文では, 形式手法を使って上手くできたことだけでなく, 上手くできなかったことも書いてあるらしいので期待できます.