刊行物
｜ ENGLISH ｜
末永 幸平
コンピュータが動作するには、コンピュータを構成する機械（ハードウェア）とともに、その機械がどのように動作すべきかを指定する台本（ソフトウェア） が必要です。この台本たるソフトウェアを人間が書くためにプログラミング言語という人工言語が使われます。C 言語や Java や OCaml や Haskell などといったプログラミング言語を使ったことがある方も多いでしょう。
人間が作るものには常に誤りがつきまといます。ソフトウェアについてもそれは例外ではなく、私達はしばしばソフトウェアの誤動作（バグ）に出くわします。 パソコンのフリーズなどはソフトウェアのバグが一因となって起こることも多いようです。パソコンならば再起動すればすみますが、これが企業の基幹システム等で起こったら大問題です。もちろん、このようなことが起こらないように、技術者はソフトウェアに対するテストを重ねて、できるだけバグがないことを確認します。しかしそれでもテストをすり抜けるバグはあるもので、そのようなバグが問題を引き起こすことは実際によくあります。
計算機科学の国際会議で無限小プログラミングについて発表する筆者
プログラムの形式検証は、バグに対処するために数学を使う分野です。定理に間違いがないことを数学的に証明するが如く、ソフトウェアにバグがないことを数学的に証明します。そうすれば、数学の定理と同様に信頼して使うことができます。おそらくこの説明だけではピンと来ないと思いますが、「数学を使ってソフトウェアの信頼性を上げる形式検証という手法がある」程度に思っていただければ良いです。
私は今この形式検証をハイブリッドシステムという比較的新しいタイプのシステムに適用するための研究を行っています。ハイブリッドシステムとは、ソフトウェアが制御に関わる飛行機のように、デジタルな動作とアナログな動作が両方入り混じったようなシステムのことを指します。このようなシステムに対しては、デジタルとアナログの混在のために従来の形式検証がそのまま適用できませんでした。このデジタルとアナログの壁を乗り越えるために、私と東京大学の蓮尾 一郎講師は最近「無限小プログラミング」という手法を提案しました。直観的にはプログラムに無限小値を記述できるようにすることで、アナログな動作をデジタルな動作で置き換えるという手法です。数学の分野で研究されてきた超準解析という手法によって、この直観に厳密なバックボーンを与えることができ、さらに従来の検証手法がそのままハイブリッドシステムに適用できることが示せます。
2 年前から始めた研究なので、まだまだ実システムへの適用とはいきませんが、将来的には自動車が安全に動く等の性質を検証できるくらいの手法にまで育てたいと研究を進めているところです。
（すえなが こうへい）
