********************************************************************** SWEST/DAS合同パネルテーマ：システム検証の現実と理想と将来座長：中村祐一（NEC）パネラ：石塚真一（サイバネットシステム）　　　　荒木大（インターデザイン・テクノロジー）　　　　山郷成仁（デンソー）　　　　中島震（国立情報学研究所）日時：9/3 13:00-14:30 参加人数：約80人 ********************************************************************** ○発言者の略称 N氏：中村祐一氏 I氏：石塚真一氏 A氏：荒木大氏 Y氏：山郷成仁氏 S氏：中島震氏その他：出席者 ○議事録本文 N氏：オープニングトーク　背景説明　　設計と検証の割合は設計が2，3割、検証が7，8割　　検証やデバッグの方が時間かかる　検証の問題点　　なぜシステム検証が複雑か？　　　システム事態が複雑化　　　ハードとソフトの協調動作　　　マルチコア、マルチタスク　　　ソフトウェアのソースコードのライン数　　　出荷後の回収を防ぐ　　検証の準備が複雑　　　シミュレーションの実行時間が何日かかるか　　　何を検証するか、どういう戦略で検証するかを考えないといけない　　人間の問題　　　スキルのある検証エンジニアの不足　　　何を勉強すればいいか分からない　　　ツールが使いこなせない　　マネジメントの問題　討論項目案　　現在のシステム検証の問題の認識　　今後必要とされる検証技術などについて考える　パネリストの紹介　　荒木さん　　　ハードとソフト協調設計の検証について　　石塚さん　　　モデルベース設計の有効性について　　山郷さん　　　デザインコベリフィケーションについて　　中島さん　　　抽象化の重要性について　進め方　　パネリストのポジショントーク約13分×4人　　会場からのQ&A 　　会場からの意見に対するパネル討論 13:08〜 A氏：システムレベル設計を中心に説明 V字で開発を説明する人が多い　設計はトップダウン、検証はボトムアップに進める　多くの場合、実機を使って試験するモデルベース設計　設計検証をできるだけ前倒しして設計生産性を向上することが狙い　モデルを使ってV字の前の方で試験をする監視カメラの設計例　アルゴリズム設計（Matlab/simlink）　C言語でアルゴリズム設計　ハード／ソフトの分割　　ソフトは組込み用に書き直す　　ハードは動作合成　SoCでテストする　これらの工程をできるだけツールを使って行うハード／ソフトの分割　あるブロックはプロセッサに割り当て、あるブロックは専用ハードにする　どうハード／ソフトに分割するかを考えていく　アーキテクチャ探索ツールでいろんなパターンを簡単に試せるシステムレベル設計における検証　検証の精度について　　アルゴリズムの検証　　仕様レベルの検証　　ハード／ソフトの分割についての検証（SILS）　　サイクル制度のシミュレーション（PILS）　　実機やエミュレータによるシミュレーション（HILS）何が問題か　テストをするためには設計対象のモデルだけでなく外部のモデルも必要で　ある　　ソフトをテストする人には、ハードやメカが必要で、逆もまた然り　モデルの抽象度を設計の抽象度に合わせないといけない　設計はいろんなツールにより簡単化されているが、テストをするための環境　をつくることが問題　どの精度の検証をどこからどこまで使うか例えば、消費電力などは下の方の検証を使わないとだめ（モデルベース検証だけですべてカバーできない）将来　検証環境はプラットフォームを提供する人が提供すべき（Androidの例）　モデルの流通や使い回しにより、モデルを作るのが簡単になるのでは　ないか 13:24〜 I氏：高速・高精度なMBDシミュレータをめざして自己紹介　昔は情報機器、制御系の会社　現在はサイバネットシステム　　数値解析、CAE技術、数式処理ツール目指すもの　専門ツールの融合　　離散シミュレータ（制御アルゴリズム）　　連続シミュレータ（制御対象）　CASEツールが今日たくさんできているが、トレーサビリティを確保する　ツールも必要組込みの制御対象物のモデルを作るようなツールの紹介　制御する側のモデルを読み出せるようになっている　制御対象のモデルと制御のモデルが同期して動く　特徴　　専用ツール同士の融合　　MapleSIm->数式モデルによる高速シミュレーション　　ZipC->状態遷移図と状態遷移表　MapleSim 　制御対象のモデリングになれていない人でも直感的にモデル化できる数式モデルだと何が嬉しいか　計算コストの削減による高速化ができる　　精度は減るけれども、それ以上に無駄な計算を省ける　本当に微分できる　　数値解析だと誤差がたまる　モデルのカスタマイズが可能　非線形制御にも展開でできる課題　ツールのギャップは埋まった　存在するギャップは、　　制御系設計エンジニアと組込みエンジニアのギャップ　　組織間のギャップ　解決策は、　　エンジニアリング　　トレーニング 13:36〜 Y氏：システム設計現場からみた検証技術への期待自己紹介　システムエンジニア（先行開発）　　製品の企画から実装、改造、試験走行　ドライバの支援システムを担当　検証技術との関わり　　形式手法の調査を過去3年していた検証のとらえ方　検証はvalidationとvelificationの2つ　　validation：お客さんが望んでいるものを本当に作れているのか　　velification：バグがないか、各工程で正しいものが作れているのか　　　<-今回はvelificationについて説明　検証の目的と対象　　目的は開発ステージによって違う　　　研究は10年後に実現可能かということを考える　　　先行開発5年のスタンス　　　量産1年、2年のスタンス　　対象は設計対象すべてだが、どこに比重をおくかは開発ステージにより　　変わる検証がなぜ必要か　企業の存亡に関わる　　検証できないシステムを作ってはいけない　人海戦術型から検証技術型へ　　人海戦術は小規模なら大丈夫だが、大規模・複雑になると総当たりでは　　無理　検証できないシステムは世に出せない　　Windowsなら止まっても大丈夫だが、車では止まるのは大丈夫でない　　いいシステムを作っても正しさを示せないとだめ検証はすごく難しい　現場の人が使うには難しいけど、検証ツールがあればある程度楽になる　　ツールが正しいことを示さないとだめ　検証ツールを100％信頼することはできない　　ツールベンダに責任を押しつけられない　　使う側がちゃんとチェックすべき　　検証の判断基準を決めるのが難しい　検証を正しく使うのは難しい　　とりあえず使えば大丈夫というものではない　　問題が起きる場合の多くは設計が悪い　　　検証をしやすいような設計をしないといけない検証の難しさの原因　検証を考えた設計がなされていない　　大規模複雑にならないように構造化されていない　　　人間が把握できる適度な大きさでないと混乱する　検証方法を考えた構造化がなされていない　　ここは数式テスト、ここはシミュレーション、ここは実機テスト　　ということを考えないといけない　　形式検証は作るのが大変　そもそも何を検証すべきかが考えられていない　　要件が明確でない　　設計に事前事後条件や検証項目をつけるべき検証の理想　検証しやすい設計しか許さない　　システムアーキテクチャで縛る　　教育、ツールで実現する　設計と同時に検証を終わらせる　　わざわざ検証してあげるという手間を減らしてあげるとモチベーショ　　ンがあがる　後工程の見積もりができる検証の将来に向けて　産学がこれまで以上に連携する　専門教育を充実させる　　上流工程の教育を充実すべき　企業の努力　　積極的に学に打ち明ける　　設計者と検証技術者を両立すべき 13:54〜 S氏：抽象化の重要性について自己紹介　国立情報学研究所の教授　関心事　　形式手法、形式検証全般　　産学連携プロジェクト：DSFやSSR 形式手法の40年　ソフトウェア開発全体を検証する技術　　非現実的でほとんど使われない　formal method liteにより、実用的にする　その後2つの方向に分化　　　表現力は高いが自動検証はしない　　表現力は低いが自動検証する<- 今回はこちら実用化にむけて　形式仕様言語（ロジックで表現）　形式手法（アルゴリズム）モデルチェッキング　有限の状態遷移を網羅的に探しまわる技術　　状態空間が大きくなるとできなくなる　　→ 抽象化が必要（要らない情報をすてて、状態空間を小さくする）　　抽象化の方法　　　人手で行うアドホックな方法　　　理論的な基盤のあるモデル化技法抽象化の悪影響　過小近似　　本来あるバグが見つからない　過大近似　　ツールが間違って不具合を報告する　　余分な不具合かどうかを判断しないといけない抽象化の例　振る舞い仕様の検証　　複数の状態を1つの状態と思う　　　本来通らないパスも考えてしまう　　　見かけの不具合ができる　　　抽象化により、自己遷移が発生して、無限ループになるかもしれない　　　　ループが無限にならないという条件をうまく見つけてあげる工夫が　　　　必要だけど、一般的には難しい問題組込みシステムはハイブリッドシステム　制御系が外界の変化を予測しないといけない　　物理法則を抽象化　　網羅的な検証は多くの場合決定不能　　表現できたとしても、検証は抽象化しないと不可能モデリングと抽象化　もともと、人間は自然に抽象化する　モデリングは抽象化の固まり　最後に判断するのは抽象化した人間今後の展望　適切なモデリング　　人間がちゃんとしないといけない　　正しいモデリング技術を身につける　自動検証アルゴリズム　　問題構造からのヒューリスティックス　自動デバッグ　　不具合を見つけたら、位置を特定して自動で直す　　　今日の話では、不具合を見つけることしかできない　　　位置を特定することができればよいのではないか 14:08〜パネル討論： N氏：　検証は人間の問題に最後落ちることが多い　人間の問題に落ちると、文化の問題になる　検証をうまくいかせるには人と技術と文化が重要になると思う　その点について意見を頂きたい A氏：　製品を使っていただく方との関係が問題　組織として取り組む動きが重要　　検証は特に問題が大きい　クライアントや作った人との関係を考えながら行うことが重要 I氏：　方法論は日本では特に変わりにくい　　いい技術が受け入れられるわけでない　　タイミングも重要　抽象度をあげるのはモデリングの基本で、重要だけど、怖い　抽象度を上げた世界でみること、もとの世界に戻すことは怖い Y氏：　日本の技術者は言われた以上の品質を目指す　検証はコストが非常にかかるので、コストも考えてやらないといけない S氏：　どのくらいの信頼性をシステムに求めるべきかがユーザにある　100％の信頼性はおそらくない　　対象システムがどの程度の信頼度を達成すべきか　その信頼性が達成できているかをどう客観的に示すか　アセスメント、信頼性を高める、アカウンタビリティの3つが重要　そうしないと、過剰コストになってしまう　2007年アメリカのデータをみると、信頼性のアセスメントが不足している　　日本だけでなく、世界的にも信頼性に対するものの考えかたは発展途上 N氏：　発注者からはコストや品質が見えない　どう説明すれば分かってもらえるか Y氏：　品質を説明するのはすごく難しい　ちゃんとテストしましたと説明してもお客さんがピンときているか不明　車の場合、何回走らせてどれくらい不具合がでたかは説明しているが　客観的に説明できているかは悩ましい I氏：　規模が大きくなると、ツール開発者側とすると検証できない　　ある仮定のもとで成り立つことを示して品質を保持するしかない　　自動生成された何千万行のコードを保証しろといわれてもすみません　　というしかない A氏：　費用対効果を説明する　ツールの導入コストなどで設計生産性を説明する　シミュレーションを動かした結果をどう分析するかはお客さんの文化　　具体的に、東芝などは品質に厳しい　テストツールがどのくらいデータをとるべきかを考えていかないといけない　業種によって品質の基準が変わるので、業種によって変える N氏：　お客さんに品質に対する理解があれば説明しやすいのですか A氏：　お客さんにはお客さんの文化がある　検証には第三者の視点が必要　　ツールはある意味で第三者の視点 M社のH氏：　設計と検証を同時に行うことについて、　現実では難しいと思うが、具体的な方策はあるのか　我々では、設計と検証の工程を分けて、設計が終わってから検証をしている Y氏：　設計をやって検証をするというサイクルを早く回すことが重要　　検証をツールによってサポート・高速化することが理想 M社のH氏：　ユニットの検証を短時間で回すようにすればよいのか Y氏：　細かいロジックは設計者自身、大きい全体の動きは設計者以外が検証する　というのもあり N氏：　イメージとしては、検証ツールがコンパイルエラーを出してくれる感じ　だと思う　実際問題としてそういう製品はあるのか S氏：　多くはEclipseベースの形式仕様言語　Event-Bがおもしろい　　Bメソッドを上流で使えるようにしたもの A社のM氏：　自動車関係の機能安全で形式手法を導入しないといけない　小さい改善を積み重ねるのは慣れているが、大きい改善をするのは　難しい　形式手法のような大きい変化を段階を踏んで変えることはできるのか S氏：　形式仕様言語は、開発上流工程　オブジェクト指向でも同じことがあった　オブジェクト指向は考え方が重要である　開発上流工程の形式手法はロジックである　ベースになる頭の切り替えは重要　形式検証はボタン一発で自動検証できるツールを目指す　　モデルチェッキングは有限状態の検証　形式仕様言語はモデリングであり、厳密に理解しないと書けない　モデリングの難しさは形式手法の有無によらない　それを誤解してはいけない　形式手法はボタン一発のツールをめざす　 N氏：　最後に検証で重要なことについて一言ずつ A氏：　個人の取り組みよりも組織の取り組みの方が効果が大きい　　 I氏：　100％の正しさを示すには論理的にやるしかない　論理的な思考が役に立つという教育を浸透させることが重要 Y氏：　何をいつどの程度検証すればうれしいかを考えることが大切 S氏：　モデリングや数式が難しい　検証ツールの支援がないと無理　　フィードバックなしで正しいプログラムを作るのは難しい　　 ○まとめ大規模・複雑化している組込みシステムの開発において、検証は重要な役割となっている。検証を行う際には、どの程度の精度で行うべきかを考えることが重要であり、また、ツールによる支援が必要である。今後の課題は、技術者や組織の考え方、教育方針を変えていくこと、自動検証ツールを作成すること、モデリングをどう行うかなどが挙げられる。以上。