数学を使って安全なソフトウエアを作る

その仕様で大丈夫？

スマートフォンから社会インフラまで、あらゆるところにソフトウエアが組み込まれています。そこにバグやセキュリティホールがあれば、大きな経済的損失や大事故にもなりかねません。
ソフトウエア制作では、「どういうものを作るか」を明文化した仕様書に従ってプログラミングを行い、システムを作っていきます。仕様書に欠陥があれば、欠陥があるまま作られてしまい、最悪の場合は一から作り直すことになります。仕様書の段階で欠陥がないかを十分に検査しておくことが大切なのです。

仕様の正しさを自動検証

仕様の安全性を担保する方法の一つに、「形式仕様」と呼ばれる、数学的な記述方法を使うアプローチがあります。形式仕様のメリットは、あいまいさのない厳格な仕様が得られることと、その仕様の正しさを、コンピュータを使って自動で検証できることです。
エレベーターのようにボタンを押すだけのシステムであっても、ボタンがN個あれば、入力パターンは2ⁿ個になり、そのすべてについて正常に動作するかのチェックが必要です。より複雑なシステムで入力パターンが膨大になると、人力のチェックは不完全であり、コンピュータで見落としなくチェックできることが望まれるのです。

普及の鍵は検証の効率化

形式仕様は、既にNASAや自動車メーカーなどに導入されています。しかし、コンピュータを使っても検証作業は大変なため、広く一般のシステム開発に使われるようになってはいません。そこで、検証作業をさらに効率化するための研究が進められています。具体的には、データ構造を工夫してデータを圧縮する方法や、システムをモジュール化して小分けし、モジュールごとに検証を行う方法などが提案されています。関連性の強度を判断し、それを考慮して適切にモジュール化することがポイントです。
検証だけではなく、形式仕様の記述をサポートするための研究も行われています。数学という道具を使って、社会の堅牢（けんろう）性を高めていくのです。

※夢ナビ講義は各講師の見解にもとづく講義内容としてご理解ください。

※夢ナビ講義の内容に関するお問い合わせには対応しておりません。

先生情報 / 大学情報

拓殖大学工学部情報工学科准教授島川昌也先生

興味が湧いてきたら、この学問がオススメ！

情報科学、情報工学

先生が目指すSDGs

メッセージ

いろいろなことにアンテナを張って、少しでも疑問を持ったり、興味を引いたりするものがあったら、そのままにせず、少しでいいので自分で考えてみたり調べたりしましょう。そしてもしも「これだ！」というものに出会えたら、今度はそれをぜひ突き詰めてみましょう。そういった経験は、一生ものの財産になります。その経験を通して、将来のビジョンが描けるようになると思いますので、ぜひ頑張ってください。

先生への質問

先生の学問へのきっかけは？
先輩たちはどんな仕事に携わっているの？

拓殖大学に関心を持ったあなたは

拓殖大学がテーマに掲げるのは「世界で、自分を拓く」。短期・長期でさまざまな国・地域に留学できる海外研修をはじめ、国内においても外国語を専門とする大学に匹敵する14の言語科目、多くの国・地域から集まった多数の留学生との交流など、国際社会の明日を担う人材の育成をめざして、拓殖大学ならではのグローバルな教育環境を用意しています。