情報産業における数学・論理・計算
Mathematics, Logic and Computation in Information Industry
Keynote Lecture
近代形式手法の確立を目指して - Towards Modern Formal Methods
北陸先端科学技術大学院大学
Abstract
我々は，これまでに，車載システムを主な対象として，形式手法の実践応用に関する研究を行ってきた．また，自動車分野の企業と共同研究も実施しており，これらを通じて，現在，ソフトウェアの開発と検証は転換期にあると実感している．AIが脚光を浴びており，エンターテイメントや事務処理のみならず，自動車の自動運転などの高安全システムにも応用され始めている．このような先進的なソフトウェアは従来のソフトウェアとは異なる性質を持つため，従来からの開発・検証手法では取扱が困難であると考えられる．そこで，我々は，形式手法を発展させ，近代的形式手法として確立し，このようなソフトウェアの信頼性と安全性を科学的に保証することを目指している．本講演では，まず，我々のこれまでの活動について紹介する．そして，その後，先進的なソフトウェアの特徴や問題点を整理し，近代的形式手法の確立を目指した取り組みについて紹介する．
