AWSにおける形式手法の適用 ― 2015年10月21日 10:56
Communications of the ACM、2015年4月号から。AWSで形式手法(Fomal Methods)を適用して成果を上げているとの記事の寄稿。

クラウドのサービスを利用することがあたりまえになってきた中、それらのサービスの品質が満足行くものか、一抹の不安を抱えながら、ということはよくある。本稿は、AWSでS3やDynamoDBなどの構築に携わった面々が、形式手法を適用して、簡単には見つからない設計バグの解消に取り組んだ事例を報告する。
バグを解消する、というと、幾多のレビューを受け、考えられるだけのテストケースと負荷試験を十分な時間を掛けて実施し、というのがよくあるが、AWSのように同時並行で多数の処理が動き、それぞれが複雑に作用し合うサービスでは、それだけでは十分でなかった。その解決を模索する中で、形式手法にたどりつき、DynamoDBのプロジェクトで成果を上げてから、S3をはじめ、他のプロジェクトに普及していったという。
トラブルが発生すると、どれだけの人と時間を投入して改善した、ミスを発生させた人員にはペナルティを課す、監視システムを充実させた、などの対応策を説明されることがあるが、これらで本当にトラブルがなくなるのか、納得するのは難しいのが本当のところ。その点、本稿にあるようなAWSの取り組みは本質に迫り、安心感を高める。
なお、Amazonが、自社のプロジェクトに適していると判断したのは、TLA+とそれを元にしたアルゴリズム記述言語のPlusCal。ちょっと見た感じ、記号論理学で習った記述に近しいやり方で、処理のロジック(アルゴリズム)を書き下している。
※TLA+の解説
コメント
トラックバック
このエントリのトラックバックURL: http://c5d5e5.asablo.jp/blog/2015/10/21/7859278/tb
※なお、送られたトラックバックはブログの管理者が確認するまで公開されません。
コメントをどうぞ
※メールアドレスとURLの入力は必須ではありません。 入力されたメールアドレスは記事に反映されず、ブログの管理者のみが参照できます。
※なお、送られたコメントはブログの管理者が確認するまで公開されません。