社会を支える重要システムの
安全性・信頼性を
最先端の科学で
保証する
SCROLL
正しいソフトウェアの実現へ
我々が日常生活をしている今日の社会には、様々な所にソフトウェアが使われています。ソフトウェアはパソコンで動作させる物だけでなく、携帯電話、電化製品、自動車、飛行機などにも組込まれており、身の回りの製品、日々の生活に深く関わっています。そのため、ソフトウェアの誤りは日常生活や経済活動を混乱させ、莫大な時間的、金銭的損失を引き起こす可能性があり、実際、そのような事例が報告されてきています。なぜ、誤りを含むソフトウェアが市場に出回っているのか不思議に思う人もいるかもしれません。誤りのない正しいソフトウェアを実現することは現代の科学をもっても達成できておらず、現状では、製品に誤りが含まれてしまうことは不可避なのです。そこで、誤りのない、正しいソフトウェアを開発する方法を確立することは、挑戦的な研究であり、今後の社会の発展、および、安心した生活を送るためにとても重要です。
JST CRESTプロジェクト: 次世代車載基盤システムのための形式手法と検証ツールの創出
プロジェクトメンバを募集中です．興味のある学生さんは青木かプロジェクトメンバまで問い合わせてください．
安全・安心なシステムの
開発手法に関する研究
- 近代的システム：自動運転、AIシステム、スマートシティ、ブロックチェーン、量子プログラムなど
- Traditional→Modern：近代的システム開発への変遷期
計算機科学に基づいた開発と検証
- 科学的に安心・安全であることを保証
- 形式手法・形式検証、そしてその後
産業応用の実施
- 社会におけるソフトウェア・システム
- 自動車システム、宇宙システム、重要インフラシステムなど
チャレンジ
-
大規模・複雑
実際のシステムに適用することを目指す
-
決定不能
本質的に決定不能な問題を実践的に取り扱う
-
不確実性
人工知能システムを念頭に不確実性を扱う
-
品質保証
高い品質であることを説明する