数学で設計する「形式手法」で、バグのないシステムを

世の中はコンピュータシステムで動いている

現代社会はコンピュータシステムで動いています。こうしたシステムに「バグ」、つまり誤りがあると、時には人々の財産や命を失わせる危険性もあります。最近ではシステムが大規模で複雑になり、かつ社会に対する影響も大きくなっているため、そのシステムを動かすソフトウエアに厳密な正確さが求められています。

早い段階でシステムの安全性を証明

一つのソフトウエアをつくるとき、まず必要な要素を分析し、「仕様書」を作成します。例えば「ある条件でこのボタンを押したら口座AからBに送金する」のような記述です。プログラマーはその仕様書に従って、コンピュータにその動作をさせるプログラムを書きます。
きちんと仕様書通りにプログラミングできても、仕様書に誤りがあると間違って送金されるかもしれません。プログラムのバグは比較的簡単に修正できますが、仕様書の段階で誤りがあると、やり直しの手間が大きくなります。特に社会的な影響が大きいシステムの場合、仕様書でのミスを防ぐために、数学的な裏付けを持つ「形式手法」という開発手法で、そのシステムを検証し、安全性、信頼性を証明しています。

数式で説明する「形式手法」

形式手法では、人の話す自然言語ではなく数式で仕様書を記述します。自然言語にある「曖昧さ」がないため、ミスを防ぐことができます。形式手法のベースには各種の数学の概念が応用されています。例えば代数を使った国産の仕様記述言語「CafeOBJ」では、等式で仕様を表します。それらの等式を使って別の等式を証明することで、システムの正しさを一種の「定理」として証明できます。
形式手法は数学モデル上で論理を積み上げて正解を導く「モデル駆動」というアプローチですが、大量のデータから正解を推測する「データ駆動」という方法もあります。最近では、モデル駆動とデータ駆動を融合して弱点を補い合うような新しい試みも研究されています。

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

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

先生情報 / 大学情報

富山県立大学情報工学部データサイエンス学科（※2024年4月設置）教授中村正樹先生

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

情報工学、ソフトウェア工学、数学

先生が目指すSDGs

メッセージ

学生の頃、数学の定理を証明するのが大変で、「面倒だな、コンピュータがやってくれないかな」と思ったものです。それが今では大学で情報工学分野の教員になり、数学の証明をコンピュータがやってくれるような手法、ツールを研究しています。社会で使うシステムの問題を数学で表現して、自分で定理を作って、それをコンピュータに証明させるような仕事です。研究にとどまらず、自分が勉強したことが社会に役立っていくことは大きな喜びです。数学好きにぜひおすすめの分野です。

富山県立大学に関心を持ったあなたは

本学は、1990年の建学以来、創造力と実践力を兼ね備えた人材育成や高度な研究開発、産業界との連携による地域貢献を果たしながら、最適な教育・研究環境を整えてきました。
2024年4月には、「情報」を軸とする工学の専門知識と、データサイエンスの専門知識を兼ね備え、デジタルの力を活用して社会の潜在的課題の解決策を導き出す能力を持った人材を育成する、「情報工学部」を新設しました。新しい校舎も建設予定です。
「ドンドン　マスマス」成長する富山県立大学で、一緒に成長しよう！