さて、どこから勉強するか……

何から勉強したものか分からなかったので、とりあえずググってみて、以下のサイトを発見。

形式手法に関する様々な情報が集約されているようなので、まずはここを足掛かりに勉強してみます。しかし、ニュース&トピックの更新されてなさを見ると、あんまり活性化していないサイトなのかな。まあいいか。とっかかりだし。

サイトを探してみると「フォーマルメソッド導入ガイダンス」という、ガイダンス感あふれるドキュメントを発見。技術の背景から適用方法まで書いてくれていて、なんかとっかかりに良さそうです。PDFをダウンロードしてみると256ページもあって一瞬心がくじけたのですが、p115以降は付録とのことなので、まずはざっと流し読みしてみます。前記事であげたような疑問点が解消されると良いな。

※ちなみに「形式言語＝フォーマルメソッド」とのことです。

第１部意識啓発編（まとめ）

何を解決する技術なの？

ポイント（要約）

ソフトウェアの大規模化、複雑化が進んでいる。
そのような中でソフトウェア事故を起こさないため、ソフトウェアの安全性・信頼性を確保する技法が求められている。
その対策アプローチの一つが、フォーマルメソッド（＝形式言語）
フォーマルメソッドは、ソフトウェアの要求や設計仕様を、数学的に意味づけられた言語を用いて記述する。
ツールを用いて論理的な検証を行うことにより、従来のソフトウェアテストでは困難であった正式の保証や不具合の検出などに利用される技術。

感想

フォーマルメソッドは、大規模化・複雑化していくソフトウェアの品質を、上流工程でかっちり確保しましょうというアプローチと理解しました（ウォーターフォールでは定番の品質確保の考え方ですね）
「複雑化」に対する他のアプローチとしては、まっさきにアジャイルが思い浮かびました。しかし、アジャイルはどちらかといえば「仕様の複雑さ」というより、「要求の複雑さ（不確定さ？）」への対策という側面の方が強く、別の課題に対するアプローチなのかなと思いました。

フォーマルメソッドが国内の開発現場で導入が進んでいない理由は？

ポイント（要約）

従来のソフトウェア開発手法を利用する開発者にとって、馴染みの無い概念やスキルが必要となり、新たな取組みのきっかけが得にくい。
実績に関する情報が得にくく、また、コストと効果に対する評価が難しいため、導入の意思決定が難しい。
導入初期の障壁を乗り越えるための組織としての導入ノウハウや留意点を示したガイダンスが少ない。

感想

知りたかったことの一つ。でも上記の理由は、技術特性によらず、大半の新技術に当てはまるものなので、あまり参考になりませんでした。
この記事自体は2011年のものなので、状況はまた変わっているはず。別の記事で探してみます。

フォーマルメソッドの種類は？

ポイント（要約）

フォーマルメソッドは、基礎とする数学理論などによって異なる多数の手法の総称。100以上の異なる手法が提案されている。
それぞれ記述する対象範囲や検証目的等の適性に違いが
ある
実践でよく利用されるフォーマルメソッドには、Bメソッド、Event-B、VDM++、SPIN、NuSMV、Zなどの例がある
ProVerifのように、プロトコル検証など特定の目的に対応した専門家向けのフォーマルメソッドなどにも有用なものがある

感想

100以上も手法があるのは、汎用的な規格を作るのが難しかったから？　それとも単に、黎明期にいろんな手法が乱立したから？

従来のソフトウェアテストとの違い

ポイント（要約）

ソフトウェアテストは、完全な網羅性を持たない。不具合を発見する目的で利用されるが、不具合が存在しないことを示すことはできない
フォーマルメソッドは、ソフトウェアがある性質を満たしていることを論理的に検証するため、一定の不具合が存在しないことを保証できる。

感想

フォーマルメソッドは、あくまで「仕様」に関して不具合が存在しないことを示すことができると理解しました。
この仕様をもとに実装されたソフトウェアが「仕様通りに実装されているか」は、ソフトウェアテストで検証する必要があると思います。
またそのソフトウェアテストの仕様書に網羅性があるかは、フォーマルメソッドで記述されたルール（？）をもとに検証する必要があると推測しました。

フォーマルメソッドを適用した開発プロセス（設計検証の場合）

ポイント（要約）

要求仕様（何を実現するか）をもとに、「検証の基準（検証性質）」を形式仕様言語を用いて記述する
設計仕様（どのように実現するか）をもとに、「検証の対象（設計仕様）」を形式仕様言語を用いて記述する

　これらをツールに入力し、「整合性はとれているか」、「検証対象が検証基準を満たしているか」「反例は存在するか」を検証する。

感想

検証のイメージが少しだけできた。

フォーマルメソッドの適用レベル

ポイント（要約）

【レベル0】形式仕様記述：形式仕様記述言語を用いて、仕様を記述する。要求仕様の厳密な定義ができる。
【レベル1】形式的開発および検証：形式仕様を詳細化することでプログラムを開発・またはプロゴラムの性質を証明する。
【レベル2】自動検証：プログラムの性質を自動的に検証する

感想

レベル0は要求仕様のみ形式仕様言語で記述、レベル1は設計仕様を形式仕様言語で記述（整合性チェックができる）、レベル2では設計仕様が要求仕様を満たすかを検証する……ということ？

形式検証のアプローチ

ポイント（要約）

【モデル検査】対象システムを状態遷移系によりモデル化し、検証したい性質を、論理的な式で記述し、状態遷移系の状態を網羅的に探索し、論理式が満たされるかを検査する。
【定理証明】　システムを論理式の集合などにより記述し、小売りと推論規則に基づく証明を行う。

感想

良く分からない。
モデル検査は、設計仕様が要求仕様を満たすかを網羅的に探索し、検査すること？
定理証明は、「こういう状態は真か？」みたいなチェックができるということ？

フォーマルメソッドの期待効果

ポイント（要約）

設計仕様が検証性質を満たすことを「保証」できる。これはセーフティクリティカル・システムなど人命にかかわるシステムにおいては、極めて重要な意味を持つ。
開発の上流工程で、早期に不具合を発見できる　⇒　工数増大、納期遅延のリスクを抑える
フォーマルメソッドに基づく言語を用いて設計し、自動コード生成を活用することにより、コーディング、レビュー、テスト工程の7～9割の工数が削減された実例がある（航空分野）。
設計から製造に至るまでの工程を、フォーマルメソッドを用いた検証を徹底することにより、自動生成されたコードの単体テストを全く行わない事例などもある（鉄道分野）

感想

自動コード生成がどこまで実現できるかは気になります。単体テストを全く行わなくて良くするためには、業務ロジックも自動生成する必要がある（人手によるミスを入り込む余地をなくす）はずです。あくまで「自動生成されたコードの範囲において（入力チェック等？）」単体テストを行わなかっただけだと推測します。事例の論文をざっと流し見したところ、以下のような記述を見つけたので、多分そんな感じだと思います（間違っていたらすみません）。「これで設計から実装まで完結するじゃん！フゥー！」みたいな、過度な期待はダメそうです。

The process was the following one:
1. the functional software requirements were re-written in a formal language;
2. the software source code, written in Modula 2 language, 
    was completed withpre-assertions and post-assertions and checked with
    a partially automated program proof activity;
3. a check between formal specification and code assertions was manually performed.

ちなみに、設計から製造まで完結させる手法は「超高速開発ツール」と呼ばれるツールの領域になります。設計情報をリポジトリに入れていくと、リポジトリと整合性のとれたプログラムが生成されます（厳密にはリポジトリを使わない超高速ツールもありますが）。プログラム生成にバグがないと仮定すると、単体テストを省略できてしまうというメリットがあります。なので、そういうことをやりたければこっちですね。フォーマルメソッドの主眼はあくまで、設計品質を確保することだと理解しました。

「第１部意識啓発編」を読んだ感想

フォーマルメソッドの概要は、なんとなく理解できた気がします。ただ情報が古いので、ここから先もさらっと読んでいきたいと思います。
形式手法をどのように記述するか、どのように検証するかが、やっぱり興味深いです。早く実装したいです。