CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コース ・ニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

研究体制・研究テーマ

産業技術総合研究所システム検証研究センター(CVS)は大阪府豊中市(千里中央)に拠点をおいて活動しております。現在、常勤研究員10名を含む32名の研究員やサポートスタッフがCVSに参加しており、プロジェクト毎に「班」を構成しています。班はヒエラルキー型ではなく、各メンバーが複数のグループに属し得るネットワーク型の構成をとっています。また、各班にリーダを置き、リーダシップを明確にしています。 CVSでは、科学研究とフィールドワークの二つのアプローチで研究活動を行っています。

科学研究
CVSで行っている科学研究は、システム検証のための抽象化技法、モデル検査技法、定理証明技法などに関するものです。

抽象化技法
chushokagiho システムの仕様や実現の記述は、システムの規模が大きくなるにしたがって爆発的に増大し、それを直接かつ正確に取り扱うことは人知を超えます。この問題を記述量爆発の問題と呼んでいます。CVSで研究している抽象化技法は、記述量爆発の問題を解決するためのアプローチです。 抽象化技法では、与えられたシステムCに関して検証したい性質PCに着目し、この性質に関しては同等だが他の性質は無視するなどして記述量を減らしたシステムAを設定します。このとき、CとAの関係Rを明確にしておけばPCをAの世界に翻訳したPAが自動的にでてきますが、「CがPCを満たすには、AがPAを満たせば十分」となるようにします。記述量が多くて検証することが困難なPC を示す代わりに、記述量の少ない世界でPAを示せばよいようにするわけです。このような方針で記述量爆発の問題を解決しようとするのが抽象化技法です。どのようにしてRやAを見つけるか、RやAにどのような条件が必要なのか、などが研究の課題です。 CVSは、抽象化技法に関する研究プロジェクトを科学技術振興機構(CREST制度)から委託されて遂行しています。抽象化の一般的な数理構造を明らかにして、抽象化技法支援ツールの設計に役立てるのが目的です。 CVSでは数理モデル班、数理的技法班、モデル検査班などで抽象化技法の研究を進めています。数理モデル班は、一般化された代数構造やファイブレーション、層などを用いた抽象化の数理的モデル(意味論)構築を目指しています。数理的技法班では、分配則のマップの概念などを用いて抽象化の研究を行っています。モデル検査班では東京大学などと、ポインタを扱うシステムに対象を限定して、具体的な抽象化技法を考案しています。

モデル検査技法
モデル検査技法は、オートマトンとして記述した情報処理システムを計算機の中に実現し、全数検査をすることによってシステムに求められる性質が成り立つかどうかを調べる検証法です。性質が成り立たないときには、必ず反例が一緒に出てくるので実用上便利ですが、オートマトンの記述が巨大になりがちなのが問題です。90年代にはハードウェアの検証に実用されはじめました。ソフトウェアは、ハードウェアよりも扱うデータの構造が複雑で検証も困難なため、モデル検査技法のソフトウェア検証への適用が現在の大きな研究課題となっています。ここでの本質的な問題は、記述量爆発問題だと考えて、CVSのモデル検査班での研究は、上記のようにモデル検査を前提とした抽象化技法に重点を置いています。また、後述するフィールドワークに用いる具体的な技法として、主にモデル検査技法を広く用いており、この技法に関するノウハウを蓄積する役割も、モデル検査班が果たしています。

定理証明技法
teirishomeigiho 定理証明技法は、情報処理システムが要求される性質を満たすことを、推論規則を適用する推論によって証明しようとする方法です。推論を計算機に完全に任せて自動的に証明を行おうとするアプローチと、推論過程の記述を計算機によって支援し、より強力な証明を行おうとするアプローチに分れます。検証技術者を対象とする高度な研修が必要なこと、証明の過程が大変長くなって扱いきれなくなってしまうことなどが定理証明技法の問題です。 定理証明班では、後者のアプローチに基づく定理証明支援系Agdaシステムの開発・保守を、イェーテボリ(スウェーデン)のシャルマース工科大学(Chalmers University of Technology)のグループと共同ですすめています。また、定理証明技法は通常、会計システムやコンパイラなど、入力出力型の情報処理システムの検証に向いているとされますが、定理証明班ではリアクティブシステムに定理証明技法を適用するための論理体系や証明技法を研究しています。 CVSは項書換系などの計算論に関する研究を、自動証明技法の基礎理論を提供するものとして重要視しています。科学技術振興機構PRESTO制度などによって等式付木構造オートマトンに関する研究を行っています。


共通知識基盤
CVSの研究員の専門分野は数学、情報科学、情報工学のさまざまな分野にわたっています。分野が違うと、同じアイディアも異った形で表現されることが多く、また話し方の厳密さが要求される方向も分野によってちがいます。いわゆる研究の蛸壷化を避けて研究情報をうまく流通させるために、CVSでは共通の知識基盤をつくる努力をしています。複雑な概念を定式化するために有用な圏論、論理と計算の記述に有効な構成的型理論(Martin-Lof型理論)、プログラミング言語 Haskell の三つをCVSの共通知識基盤として設定し、これらの枠組を使ってアイディアを交換することをメンバーに奨励しています。

フィールドワーク
フィールドワークは、企業などと共同してシステム開発の現場に参画し、システム検証に関する問題点を取材する研究活動です。開発のどの段階にどの技法をどんな道具を用いて適用していくべきか、を考察することが目的です。フィールドワークの重要な副次的効果の一つは、数理的技法の適用に際して必要な細かなノウハウまで産業界へ移転できることです。また、開発現場に通用する技術をCVSで保持し、技術を科学的に分析して、必要に応じて新たな科学を生み出すべく努めています。 企業との共同研究については、秘密保持のため、相手先も研究対象もここに明示できないのが残念です。企業との共同ばかりでなく、産総研内部の先端計算機センター(TACC)と共同でのフィールドワークも2004年度より開始しました。これは産総研自身のイントラシステムの検証がテーマです。 フィールドワークの個々の事例で得たノウハウを抽出し、他の事例に適用できる形に一般化して、各種研修コースを開発しています。モデル検査法に関する初級、中級コースを開発しており、現在、初級コースの無料試行を実施しています。

計量器情報化と法定計量
CVSは、国家標準計量機関としての産業技術総合研究所の業務である、計量法にもとづく法定計量システムの開発・整備にも関わっています。対象となる法定計量機器の情報化は急速に進んでおり、それに合わせて法定計量制度も変えていく必要があります。CVSは、経済産業省計量行政室の国際法定計量調査研究委員会や産業技術総合研究所計測標準総合センター(NMIJ)と協力して、法定計量情報化の技術基盤を構築する活動を進めています。

産総研ホーム > 組織 > 研究センター > システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.