ソフトウェアプログラム内の中核的なコミュニケーションと状態管理が論理的に100%正しいことを証明する手段として，コンピュータチェックモデルを利用する方法がある。同じようなモデルは，100%正確なソースコードの作成にも応用できる。このような形式的手法を利用することにより，市場提供のためのコストと時間を削減し，より信頼性の高いソフトウェア製品の提供が可能になる。
Wayne Lobb氏はBits&Chips Software Engineeringカンファレンスで，正当性立証可能(provably-correct)なソフトウェアについて，ビジネス的側面から講演を行う予定だ。
InfoQは氏にインタビューして，ソフトウェアが複雑である理由，正当性立証可能なソフトウェアを開発する上で形式的手法やモデルのもたらすメリット，形式的手法を用いることによるビジネス上のアドバンテージ，セーフティクリティカルないしビジネスクリティカルなソフトウェアのためのアジャイル開発プラクティスなどについて話を聞いた。
InfoQ: ソフトウェア開発はなぜ複雑なのか，バグのないソフトウェアを作るのがなぜ難しいのか，意見を聞かせてください。
Lobb: ソフトウェアが難しい理由のひとつは，それが簡単そうに見えるからです。簡単なプログラムならば小学生でも書けますが，回路の設計ではそうはいきません。デジタル回路の形式をとるハードウェアは，ロジックを物理化したものであって，それを製作するのは簡単ではありません。ソフトウェアのロジックは固まっていませんが，“製作”や変更は簡単です – 入力したり，編集したりすればよいのですから。しかしながらロジックとは，本質的に複雑で難しいものです。ソフトウェアであってもハードウェアであっても，この点には変わりありません。ハードウェア技術者はこの難しさを何十年も前から知っています。今日の回路設計者やテスタは，バグフリーなICの開発や検証，出荷といった作業を，自動化された数学的ツールやアルゴリズムに大きく依存しています。ソフトウェア開発者やテスタも同じ理由で同じことを行ってもよいはずです。すなわち，バグフリーなソフトウェアを開発，検証，出荷するために，数学的な形式的手法を適用するのです。
InfoQ: 正当性立証可能なソフトウェアについて，詳しく説明して頂けますか？
Lobb: ソフトウェアのソースコードは，３つのカテゴリに分類することができます。コンフィギュレーションおよびデータ，通信と状態のロジック，そしてアルゴリズムです。アルゴリズムが数学的であることは明らかですから，証明も可能です。 通信や状態のロジックも同じように証明可能ですが，アルゴリズムほどの明確さはありません。マルチコンピュータネットワーク，マルチコアコンピュータ，マルチスレッドソフトウェアはすべて，“Commuication Sequential Process”すなわちCSPを具現化したもので，人類の知る最も強力な計算論理と数学的に等価です。現在では，ソフトウェアのコアコミュニケーションと状態管理が100%論理的に正しいこと，すなわち，メッセージの無視，２つのプロセスが互いを恒久的に待つデッドロック，競合状態など，内在的な論理的欠陥のないことを，コンピュータチェックモデルを使った形式的手法によって証明することが可能になっています。ここで言う論理的エラーとは，配列のオーバーフローのような実装(開発)エラー以上のものです。これらのエラーは，通信や状態ロジックのエラーとは違って，CodeSonarやCoverity，Klocwork，Parasoftといった静的解析ツールで検出および修正可能なものです。
InfoQ: 形式的手法とモデルが，正当性立証可能なソフトウェア開発にどのように役立つのか，いくつか例を挙げて頂けますか？
Lobb: たくさんあります。最近の例でいうと，ネットワーク上でピアノードを検出するChord分散ハッシュテーブルプロトコルが挙げられます。MITのChordプロトコルは10年に渡って研究され，集中的な運用が続けられてきましたが，2009年のMITのAlloyモデルチェッカによる簡単な検査で，いくつかの論理エラーが発見されました。詳しい情報は，“zave chord”(引用符付き，またはなしで)をGoogleで検索してください。また，NASAでは，火星探査車の制御ソフトウェアの開発と検証にSpinモデルチェッカを使っています。こちらは“mars code”で検索できます。Camryで意図に反した加速という問題を起こしたToyotaでは，信頼性の高いソフトウェア開発のためにAltranのSPARKフォーマルメソッドツールを採用しました (toyota ada sparkで検索)。Amazonでは，“徹底的テストの可能な擬似コード(amazon tla+)”を通じてクラウドデータのセキュリティと整合性を確保するために，MicrosoftのTLA+モデルチェックを使っています。さらに航空関係の企業は，MathWorks StateFlowなどのツールを使って，航空機ソフトウェアの設計と検証を行っています(do-333ケーススタディ)。
InfoQ: 形式的手法によって期待できる，ビジネス上のメリットについて説明して頂けますか？
Lobb: 広く知られていることですが，ソフトウェア開発のできる限り早い段階でバグを見つけて修正できれば，コストが低くなりますし，修復によるスケジュールの混乱も一般的に少なくて済みます。実装前にバグの発見と修正を行う場合の費用は，テスト中や出荷後に発見と修正を行う場合に比べて，10分の1から100分の1になると言われています。通信設計や状態設計でモデル検査を行えば，1行のプログラムも書かない時点でバグを発見することさえ可能なのです。さらに，Verum DezyneやQuantum Leapsといったツールを使えば，中核的なコミュニケーションや状態管理のソフトウェアにおいても，100%正確なC, C++, Javaなどのソースコードを生成することができますし，コストや時間の節約にもなります。ASMLやPhillips Healthcareといった企業は，信頼性の高いソフトウェア管理製品の提供に形式的手法を利用することで，40%以上コストと市場提供時間の削減を実現できたと報告しています。このようなメリットは当然ながら無償で手に入るものではなく，チームとして活発に行動する必要があります。ただし，一度実行してしまえば，そのメリットは何度となく感じられることでしょう。
InfoQ: セーフティクリティカル，あるいはビジネスクリティカルなソフトウェアの開発にアジャイル開発プラクティスを用いることについては，どのように思われますか？
Lobb: “アジャイル”の本当の意義は，プロトタイプに対するユーザの反応を通じて，本当の要件を反復的に見つけ出すプロセスにあると思っています。この意味から見れば，アジャイルには，(例えば)優れたインターフェースの設計は絶対的な条件となります。セーフティクリティカルあるいはビジネスクリティカルなソフトウェア製品もその例外ではありません。しかし実際の要件を確認できてしまえば，次に必要なのは，要件とそれを実現する設計を，可能かつ合理的な期間と範囲で詳細に，かつ文書で定義することです。そこにおいては，チームが極端に小規模でもない限り，費用対効果の最も高いアプローチをまず考えるべきだと思っています。それが終われば，関係するすべてのスタッフが，自信と相応の独立性を持って作業に当ります - ソフトウェア技術者，テストおよび検証技術者，ドキュメント担当者，マーケティング，規制関連の調査担当，デプロイメント技術者，アプリケーションエンジニアリング関係者，といった人たちです。次に考えなくてはならないのは，短いイテレーションの連続という意味での“アジャイル”において，いかなる時でも実装がベストの状態を維持することです。イテレーションは数週間の単位で，それぞれ明確に定義された機能を提供しますが，機能の難易度によって期間を変更する場合もあります。
InfoQ: ソフトウェア開発での形式的手法の利用について，より詳しく知りたい人たちのために，推薦できるリソースが他にあれば紹介してください。
Lobb: Amazonのデータセキュリティと整合性，NASAの極限的な環境での制御ソフトウェア，Chordのプロトコル検証，MathWorks StateFlowの航空機制御といった実例を見ることから始めるとよいでしょう。 www.event-b.org，www.spinroot.com，www.verum.com，あるいはWikipediaのList_of_model_checking_toolsで紹介されているサプライヤやベンダのサイトも参考にしてください。モデル検証などの形式的手法に関しては，技術論文や記事もたくさんあります。これらの技術は数十年にわたって研究が続けられていますから，成熟していますし，堅牢です。もっともそれは，ソフトウェア技術者が学術的な環境以外でも，形式的手法のために，強力で高度なコンピューティングを日常的に利用できるようになった，ここ最近のことです。回路技術がずっと昔に通ったのと同じように，ソフトウェア技術は今まさに，真のエンジニアリングとしての成熟の道へ入ろうとしているのです。