いまさら聞けない 形式手法入門：品質向上技術解説（1/3 ページ）

ソフトウェアの品質向上手段として注目されている形式手法。今回は、厳密な仕様定義を目的とした「形式仕様記述」を中心に、分かりやすく解説する

[阿部 功二 CSKシステムズ，MONOist]

　ソフトウェアの品質を確保するため、誰もがレビューとテストを行います。しかし、一般的に行われているレビューやテストにおいて、システムが正しく動作することをどの程度保証できているのでしょうか。優秀なエンジニアによる小規模ソフトウェア開発であれば、設計・テスト・検証における細心の注意とノウハウにより高品質のシステムを実現することが可能です。では、50人を超えるようなチームではどうでしょうか。

　ここでは、ソフトウェアの品質と安全性向上のために、「プログラムの正しさ」に関する研究から生まれた「形式手法（Formal Method）」を簡単に紹介します。

形式手法とは

　形式手法とは、1970年代から始められたプログラム開発手法の1つで、論理学や離散数学などが基礎になっています。プログラムの正しさに関する数学的な証明体系として整理された理論をベースとし、形式仕様記述やモデル検査へと研究対象を発展させてきています。最初は取りあえず、「品質向上のための手法（ツール）」ととらえてもよいでしょう。

　形式手法は、システムの大規模化・複雑化から、上流工程での品質改善手段として最近日本でも注目を集めるようになりました。また、海外では規格・標準において形式手法を推奨もしくは必須とするものが現れ、日本企業も真剣に取り組まざるを得ない状況になってきました。

　形式手法には多種多様な側面があります。本稿では、形式手法の最も重要な要素である

• 仕様を厳密に記述することを主目的にする仕様記述部分
• モデルを検証することを主目的にする形式検証部分

を簡単に紹介した後、仕様記述部分である形式仕様記述について説明します。

形式仕様記述（形式的仕様記述）

　「形式仕様記述」は、仕様の厳密な定義を目的としています。

　システムが「仕様」として定義され、これが開発のベースとなる現在の開発スタイルにおいて、仕様作成者の意図を正しくシステムに反映させるには、仕様作成者がシステムを直接開発・検証するか、正しい仕様と対比してシステムを開発・検証する必要があります。しかし、仮に仕様作成者がすべての開発・検証を行ったとしても、仕様自体に矛盾や未定義事項があれば、システムが正しく振る舞うことを保証できません。

　そこで、矛盾がなく論理的に正しい仕様を作成するために考案されたのが形式仕様記述です。形式仕様記述を行うための「仕様記述言語」には、VDM-SL、VDM++、RAISE/RSL、Z、B、Clear、OBJ、CafeOBJ、CASL、LOTOSなどがあります（注）。

※注：

VDM-SLは1996年に、Zは2002年にISOにて標準化されています。

　主な仕様記述言語の1つである「VDM-SL（Vienna Development Method - Specification Language）」は、もともとプログラミング言語の研究であるウィーン定義言語（Vienna Definition Language）の流れをくみ、欧州では現在まで40年以上も研究・実用が継続されています。日本ではようやく大規模な事例が出てきたという段階であり、かなり後れを取っています。

形式検証

　「形式検証」は、モデルの論理的な検証手法です。

　ソフトウェアを勉強した人であれば、オートマトンやペトリネットなどの言葉を耳にしたことがあると思います。今日の形式検証技術はこれらの研究を基礎にしています。

　一般に、設計したモデルの検証はレビューにより実施されます。しかし複雑なシステムの場合、取り得る状態が莫大になり、すべてのケースを想定することが困難になります。プログラムによる検証においてもC2レベルのカバレッジを実現することは難しく、計算機の性能向上により部分的に実現できるようになったというのが現状です。

　形式検証は、プログラムの状態をモデル化することで仕様が正しいことを検証する方法です。通信や並行処理システムにおける複雑な状態を検証する方法として、レビューだけで検証するよりも、ツールによるモデルの自動検証は有効な手段です。

　組み込みソフトウェアでは、並列処理において複雑な状態モデルのデッドロック検知などを行う手法が研究されています。モデルが正しく構築されなければ意味を成さない点で、形式仕様記述に比べ扱いが難しいものになっています。

　形式検証技術としては、SMV、SPIN、LTSA、CWB、FDR、SAL/PVSなどがあります。