研究背景・目的

　社会生活の多くの部分が計算機システムによって支えられている今日、計算機を制御するソフトウェアの品質を高め、高い信頼性を保証することは重要な課題になっています。これまでソフトウェアが誤動作を起こさないことを数学的に保証する方法として「形式手法」が研究されてきました。しかし、複雑さが増す今日のソフトウェアに形式手法を厳密に適用するには高い専門性が必要となり、多大なコストがかかることが知られています。本研究では、一般にソフトウェアの誤りを全て検出することを目的とした形式手法を少し「緩める」ことで、現実的なソフトウェアに適用することをめざします。

研究内容

　本研究では、特に「静的型システム」と呼ばれる形式手 法の一つについて研究を行っています。静的型システムはすでにJava、C++、OCaml、Haskellといった多くのプログラミング言語に採用されており、ソフトウェアを実行することなく誤りを検出することが可能です。しかし、静的型システムが誤りだと判断しても、実際には誤りではなかったという場合もあります。このような問題は静的型システムの表現力が豊かになればなるほど、より顕著に現れてきます。本研究では、実行時に検査を行う「動的型システム」を静的型システムと組み合わせることで、必要に応じて検査能力を選択できる型システムの研究に取り組んでいます（図）。

産業応用の可能性

　ソフトウェアは一般的な計算機システムだけではなく、航空機制御や自動車制御などのミッションクリティカルな部分にも使われています。そういった高信頼なシステムが求められていますが、形式手法などによる厳密な品質保証が困難な場合に、本研究を応用することができます。