CVS

center-name

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

第二回
システム検証の科学技術シンポジウム
基調講演・招待講演・チュートリアル紹介



基調講演

arrow10月20日

Kinoshita
木下佳樹(Yoshiki Kinoshita)
産業技術総合研究所 システム検証研究センター


タイトル 「システム検証の科学研究とフィールドワーク」


概要
システム検証研究センターでは研究活動を科学研究とフィールドワークに分けている。科学研究では、証明支援系Agdaに基づく統合検証環境の構築 を柱として、算譜意味論、自動検証、対話型検証などの研究を進めている。一方、フィールドワークと称する活動を展開し、技術移転をすると同時に、社会への 応用を観察することから新しい科学を生み、学術と一般社会の相互作用をおこす開かれたセンターとなるべく努めている。本講演では、以上のようなシステム検 証研究センターにおける科学技術研究を概観する。

招待講演

arrow10月20日

Takada
高田広章(Hiroaki Takada)
名古屋大学大学院 情報科学研究科

タイトル 
「組込みシステム開発の課題と検証技術」


概要
この講演では、まず、組込みシステム開発の現状と課題について整理する。次に、組込みシステムにおけるシステム検証の重要性と困難な点について、動作の再 現が難しい点、制御対象機器を動作させる必要がある点に着目して述べ、システム検証環境としてのシミュレーション環境について解説する。組込みシステム向 けの検証技術の例として、リアルタイムスケジューリング理論に基づいたリアルタイム性検証技術の概要と、それを自動車制御システムおよびネットワークに適 用した事例について解説する。


arrow10月21日

岸田孝一(Koichi Kishida)
株式会社SRA先端技術研究所(SRL-KTL)
タイトル  
「システムの検証とは?」

概要
現実世界のひとつのモデルにすぎないソフトウェアシステムについて、その正しさを検証するというのはいったいいかなる意味をもった作業なのでしょうか。多 くの人々は、与えられた仕様と具体化されたシステムとが一致するかどうかを問題にしているようですが、しかし、変転極まりないこの世界においては、仕様そ のものが絶えず変化し続けているのですから、論理の前提条件が成り立ちません。この講演では、20世紀アメリカ哲学界の異色の思想家ネルソン・グッドマン の所説を参照しながら、「正しさ」とは何か、「検証」とはいかなる作業かについて考えてみたいと思っています。


arrow10月21日

Ono
小野寛晰 (Hiroakira Ono)
北陸先端科学技術大学院大学 情報科学研究科

タイトル 「論理的方法と代数的方法」


概要
論理学の研究においては、論理の形式化に伴う証明論的方法および集合概念を使う意味論的方法が用いられる。代数的な意味論は、Booleによるプール代数 の導入に始まり、TarskiやJonssonなどがそれを大きく発展させた。しかし60年代になり、直感的に理解しやすくまた扱いやすいということによ り、Kripke流の意味論が非古典論理の意味論研究の主流になっていった。そしてそれまでの代数的研究の関心はuniversal algebraなどに向かっていった。
最近になり論理における代数的方法が大きな注目を浴びるようになってきた。実際、論理とuniversal algenra、abstract algebraic logic、代数構造などの間の深い関連性についての理解が進み、それがもらたす豊かな手法が一般性のある成果を生み出している。この講演では、代数的方 法と論理的方法、とくにシンタクティカルな方法、を対比させながら、それぞれの特徴や相互の関連などについて述べ、あわせて最近の成果のいつくかを紹介す る。

チュートリアル

arrow10月20日
Sato

佐藤雅彦 (Masahiko Sato)
京都大学大学院 情報学研究科
知能情報学専攻 

タイトル
「計算と論理をコンピュータ上に実現するための自然枠組」


概要
計算と論理をコンピュータ上に実現するための自然枠組NF(Natural Framework)の理論的背景とNFをコンピュータの上に実装したシステムCAL(Computation and Logic)の紹介をする。

数学者の行う数学的活動を観察すると計算と論理が自然に融合した活動であることがわかる。これに対して、20世紀初頭以降に提案されてきた「形式的数学」 の体系はいずれも論理的推論に重点が置かれており、体系の中で具体的な計算を行うことは困難である。また、構成的数学や計算機科学の発展とともに近年提案 されている様々な定理検証のためのシステムについても同様の難点がある。

本講演で紹介するNFは、上記の困難を克服し、コンピュータの上での自然な数学的活動の支援を可能にすることを目標に設計された計算と論理のための枠組み である。


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