こんにちは、SWETの鈴木穂高（@hoddy3190）です。 現在SWETチームにて仕様の欠陥をなるべく早くみつける取り組みにチャレンジしています。 欠陥をみつけるタイミングが早ければ早いほど、開発中の手戻りに伴うコストを抑えられます。 たとえば、仕様作成フェーズ、実装フェーズ、QAフェーズの順で開発が進んでいくときに、仕様の欠陥が実装フェーズやQAフェーズでみつかると実装やQAのやり直しを引き起こしかねません。 そうした大きな手戻りを抑えるために仕様の欠陥をなるべく仕様作成フェーズでみつけることを目指します。 対象領域に出てくる要素をモデリングすることは、仕様に潜む欠陥を開発の早い段階でみつけるための、有効な手段のひとつです。 要素には、開発者がこれから作るシステムや、そのシステムのユーザー、そのシステムと直接的または間接的に相互作用する外部のシステムが含まれます。 単に図を書くというモ

Abstract 私（@hoddy）は形式手法の実用可能性についてDeNAで研究をしています。 形式手法を使うと、MySQLのdeadlockの検知や、非同期処理の設計ミスなど、 人間が考慮しづらい部分のバグに、設計段階で気づくことができます。 形式手法とは 形式手法とは、仕様を明確に記述したり、記述された設計の性質を機械的に検証する手法の総称です。 形式手法にもいくつか種類がありますが、いずれも数学に基づく科学的な裏付けを持ちます。日本での導入事例は多くはないですが、世界的に見ると多くの導入事例が観測できます。 解決できる課題 開発では、日本語で書かれる仕様の不備（考慮漏れ、記載漏れ、矛盾など）により、大きな手戻りにつながることが多いと思います。形式手法を使うと、仕様をより厳密に書けるようになるため、仕様不備が起きにくくなります。 また、システムがとりうる状態を網羅的に探索することができ

All slide content and descriptions are owned by their creators.