形式手法を使って、発見しにくいバグを一網打尽にしよう accepted

Abstract

私(@hoddy)は形式手法の実用可能性についてDeNAで研究をしています。

形式手法を使うと、MySQLのdeadlockの検知や、非同期処理の設計ミスなど、
人間が考慮しづらい部分のバグに、設計段階で気づくことができます。

形式手法とは

形式手法とは、仕様を明確に記述したり、記述された設計の性質を機械的に検証する手法の総称です。 形式手法にもいくつか種類がありますが、いずれも数学に基づく科学的な裏付けを持ちます。日本での導入事例は多くはないですが、世界的に見ると多くの導入事例が観測できます。

解決できる課題

開発では、日本語で書かれる仕様の不備(考慮漏れ、記載漏れ、矛盾など)により、大きな手戻りにつながることが多いと思います。形式手法を使うと、仕様をより厳密に書けるようになるため、仕様不備が起きにくくなります。

また、システムがとりうる状態を網羅的に探索することができるため、再現させにくいバグをシステムを実行せずに検知することができます。

私が考える適用可能性

そんな形式手法をアプリ開発やweb開発など、よりソフトな領域にも適用できないかを、今私は研究をしています。いくつか種類がある形式手法の中でも、モデル検査と呼ばれる技術に注目しています。

モデル検査とは、システムを有限個の状態を持つモデルで表現し、モデルが取りうるすべての状態を機械的かつ網羅的に検査することで、システムが仕様を満たすことを確認する手法です。

例えば、MySQLのdeadlockの検知は、モデル検査と相性がよいと思います。
システムが投げうるクエリを複数プロセスから投げ、クエリが投げられる順番やDBの状態を網羅的に探索し、deadlockが起きるパターンはないかを探索します。これを実装ロジックを書かずに、モデリングするだけで可能にするのがモデル検査です。

さいごに

話が難しいと思われてしまったかもしれませんが、
本セッションではこれを噛み砕いてわかりやすくご説明します。
もし興味を抱いてくださる方がいたら幸いです。

2019年3月に別の勉強会で「形式手法について調べてみた」というタイトルで発表もしています。
ある程度の雰囲気はこの資料で掴むことができるかなと思います。
当然、その頃に比べ、研究は進んでいるので、さらに踏み込んだ内容をお話することができると思います。

Video
Session Information
Confirmed confirmed
Starts On 8/30/19, 1:50 PM
Room Seminar Room 1204
Session Duration 20 min session
Spoken Language Japanese
Interpretation Unavailable
Slide Language Japanese