本文へジャンプ

社会を支える重要システムの
安全性・信頼性を最先端の科学で実現する

青木研究室 AOKI Laboratory
教授:青木 利晃(Aoki Toshiaki)

E-mail:toshiakijaist.ac.jp
[研究分野]
ソフトウェア工学、ソフトウェア科学、形式手法、形式検証、テスト
[キーワード]
モデル検査、定理証明、形式仕様記述、組込みシステム、車載システム、産業応用

研究を始めるのに必要な知識・能力

「ソフトウェア=プログラム」ではないので注意すること。プログラミング能力よりは、論理的思考能力、抽象化能力が重要です。たとえば、物事を三段論法的に考えたり、複雑な問題をシンプルな枠組みで説明する能力などです。

この研究で身につく能力

現在の社会において使われているシステムや開発されているシステムを対象に、その問題を識別、問題の根本的な原因を明らかにし、理にかなった科学的な解決策を提案できるようになります。日々のニュースや新聞で見聞きするように、現在の産業界では、安全性・信頼性に関する、とても大きな問題を抱えています。この問題を解決するためには、机上だけの科学技術では不十分であり、実際に実践できる科学技術が必要です。企業に入ってしまうと目の前の製品開発で手一杯になりますが、その前に、現実的なシステムの問題を科学的に解決できる上記のような能力を身につけることはとても重要です。そして、これにより、社会において安全、安心を科学技術で支える人材になることが期待されます。

【就職先企業・職種】 製造業、情報通信業、ITコンサルティング会社

研究内容

[正しいソフトウェアの実現へ]

我々が日常生活をしている今日の社会には、様々な所にソフトウェアが使われています。ソフトウェアはパソコンで動作させる物だけでなく、携帯電話、電化製品、自動車、飛行機などにも組込まれており、身の回りの製品、日々の生活に深く関わっています。そのため、ソフトウェアの誤りは日常生活や経済活動を混乱させ、莫大な時間的、金銭的損失を引き起こす可能性があり、実際、そのような事例が報告されてきています。なぜ、誤りを含むソフトウェアが市場に出回っているのか不思議に思う人もいるかもしれません。誤りのない正しいソフトウェアを実現することは現代の科学をもっても達成できておらず、現状では、製品に誤りが含まれてしまうことは不可避なのです。そこで、誤りのない、正しいソフトウェアを開発する方法を確立することは、挑戦的な研究であり、今後の社会の発展、および、安心した生活を送るためにとても重要です。

[形式手法・形式検証]

正しいソフトウェアを実現する研究は計算機科学の歴史において、比較的長く行われています。代表的なものとして形式手法(Formal Methods)、形式検証(Formal Verification)があります。形式手法・形式検証では、数学を基礎とした言語やツールを用いて、対象となるソフトウェアを記述し、検証を行います。これにより、なんとなくソフトウェアを開発するのではなく、数学に基づいた解析や正しさの保証を行うことができます。ここでの正しさは理論的な観点のものであり、実製品での正しさ、安全性、信頼性とはギャップが大きいです。それでも、現在のところ、実製品としての正しいソフトウェアを実現するための有望なアプローチであると言えます。また、このような手法を用いて、ソフトウェア自身を科学することも重要です。ソフトウェアがこれからの社会や世界の構成要素であり続けるのであれば、他の自然科学の学問分野と同様、その本質や原理を明らかにして、事実を積み上げ、共有し、発展させる必要があります。そこで、本研究室では、形式手法・形式検証を用いて正しいソフトウェアを開発する手法、および、ソフトウェア開発の原理に関する研究を行っています。

[産業応用への挑戦]

現在の社会においてソフトウェアは重要な構成要素です。本研究室の研究対象は、「社会におけるソフトウェア」です。そのため、企業との共同研究を積極的に行っています。これまでに、主に、自動車(車載システム)を対象として、共同研究を行ってきました。現代の自動車は、多くの部分が電子制御されており、ECU (Electronic Control Unit)と呼ばれるコンピュータが多く使用され、ネットワークで接続されて協調動作しています。ハイエンドの自動車では、100個を超えるECUが使われており、非常に複雑なシステムになっています。一方で、自動車は我々の身近にある危険な乗り物であり、毎年、多くの人命が交通事故などで失われています。そこで、ソフトウェアを用いて正しく制御することはもちろん、高度な安全性の実現への挑戦がなされています。自動車において、ソフトウェアの役割は、非常に重要なものとなっているのです。我々は、車載システムメーカや研究所と共同研究を行い、実製品の検証に成功している世界的にも数少ない研究室の1つです。今後も、様々な分野で、社会を支える重要システムの安全性・信頼性を最先端の科学で実現し、安全・安心な社会を目指して研究を行っていきます。

主な研究業績

  1. Jiang Chen and Toshiaki Aoki: Conformance Testing for OSEK/VDX Operating System Using Model Checking, 18th Asia-Pacific Software Engineering Conference(APSEC), pp.274-281, 2011.
  2. Kenro Yatake, Toshiaki Aoki: Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling, International Colloquium on Theoretical Aspect of Computing(ICTAC), pp.183-197, 2012.
  3. Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, and Toshiaki Aoki: Checking the Conformance of a Promela Design to Its Formal Specification in Event-B, Third International Workshop on Formal Techniques for Safety-Critical Systems(FTSCS), 2014.

研究室の指導方針

本研究室では、1)問題の本質を学生自身で理解する、2)科学的に問題を解決する、ように指導を行います。研究を学生自身で遂行するためには、まず、研究対象を学生自身の問題として捉えることが必要です。研究の初期には、具体的な事例を題材として、頻繁に議論を行います。次に、科学的な問題の解決のためには、じっくりと問題を学生自身で検討することが必要です。研究の中期~後期では、ある程度期間の間隔がある定期的なゼミで検討結果を報告、議論します。これらの一連の研究活動を行えば、社会における問題を科学的に解決できる人材を輩出できると考えています。

[研究室HP] URL:http://www.jaist.ac.jp/is/labs/aoki-lab/

ページの先頭へもどる