制御と形式手法：物理情報システムの品質保証に向けた包括的取り組み

第61回自動制御連合講演会
特別企画2　制御と形式手法：物理情報システムの品質保証に向けた包括的取り組み

■日時: 2018/11/17(土) 13:00〜14:30

■場所: 南山大学名古屋キャンパス

■会場: 第5室　S56

■企画： JST ERATO 蓮尾メタ数理システムデザインプロジェクト
  豊田理化学研究所特定課題 「制御工学研究者と応用数学研究者の連携による革新的な制御理論構築」

■オーガナイザ：　脇隼人（九州大学）・蓮尾一郎（国立情報学研究所）

■概要：
近年，自動車などの工業製品にデジタル制御が盛んに導入され，動作の効率化のみならず，自動運転などの全く新しい機能が実現されています．しかしその結果，物理情報システムの品質保証という大きな課題が現れており，制御理論・制御工学のみならず計算機科学（特にソフトウェアの品質保証のための形式手法とよばれる諸手法）の成果をも統合した包括的取り組みが求められています．この課題に対して，制御・形式手法の両面からアプローチし，機械学習やソフトウェア工学による実践的技術も包含しつつ，さらに（メタ）理論と産業応用の両方をカバーしながら研究を行う私達の取り組みを紹介し，議論や協働のきっかけを提供すべく，本セッションを企画しました．

• 13:00-13:30
  物理情報システムの検証手法：制御と形式手法の相互理解，そして協働へ
  蓮尾 一郎（国立情報学研究所）
  物理情報システムの品質保証においては，連続ダイナミクスの解析を担う制御理論と，計算機制御による離散ダイナミクスの解析を担う計算機科学（特に形式手法），この二分野の協働が欠かせません．ここ10年余りの物理情報システム研究の高まりを通じて，両分野の内容の数学的相似性が次々に明らかになってきたと同時に（たとえばLyapunov関数とランク関数の間の相似性），各分野の手法の相互乗り入れが盛んになってきました（たとえばシステム制御における時相論理式や双模倣関係の活用）．加えて最近は，機械学習の急速な進歩を受けて，上記二分野と統計的最適化・機械学習との関わりがホットな話題となっています．これらの動向について，発表者の最近の結果を具体例として用いながらお話します．
• 13:30-14:00
  品質保証における発見的・経験的アプローチの活用：ソフトウェアテスティング分野からの知見
  石川 冬樹（国立情報学研究所）
  ますます複雑になるソフトウェアの品質保証に対しては，形式手法など理論に基づいた保証だけでなく，テスト，すなわち「いろいろ動かしてみる」ことによるアプローチが盛んに研究・活用されています．本講演では，進化計算を用いるサーチベースドテスティングなど，テスト自動生成に関する近年の技術やその成果を紹介します．また，理論に基づくアプローチとの連携，そして制御システムや自動運転システムへの活用について論じます．
• 14:00-14:30
  半正定値計画問題のプログラム検証への応用
  脇 隼人（九州大学）
  ソフトウェアが正しく動作するか調べる方法の一つとして,NelsonとOppenによるinterpolantと呼ばれる論理式に基づく判定法が知られています.DaiらとOkudonoらは,半正定値計画法を利用したinterpolantに基づく判定法を提案しその有効性を主張しています. 簡単にいうと,多項式の等式や不等式で記述された相反する二つの集合に対してそれを分離する多項式不等式を見つける問題に帰着しPositivestellensatzを使っています.この講演では, これらの仕事に対して係数の少ない(いわゆる疎な)多項式を見つける方法を紹介したいと思います.

■第61回自動制御連合講演会ウェブサイト：
https://rengo61.iscie.or.jp/program/