CVS

center-name

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

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



基調講演

arrow10月30日(10:45-11:15)

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


タイトル 「システム検証研究の現状」


概要
主として国内におけるシステム検証研究およびその周辺の現状について、我々が掌握している範囲において紹介する。大学をはじめとする学術機関における研究活動および、政府機関や業界団体による規格制定の動き、人材育成のための啓発活動や教育活動、学会その他の団体による会議や集会などについて紹介する。 あわせて、我々の研究センターが進めていくべきだと考えている活動の方向と、その実施策などについても述べたい。

招待講演

arrow10月30日(11:15-12:15)

Takada
玉井哲雄(Tetsuo Tamai)
東京大学 大学院総合文化研究科 教授

タイトル 
「形式手法の好き嫌い」


概要
システム検証に形式手法が有効でありうることは多くの人が認めるだろうが、形式手法が好きか嫌いかとなると、人によって大きく分かれるようだ。それもかなり極端に分かれて、一部の人びとは偏愛し、一部の人びとは毛嫌いする傾向がある。これはなぜだろうか。
筆者の形式手法に関連したあまり豊かとはいえない個人的経験から、形式手法の功罪と感覚的な好き嫌いについて考えてみたい。


arrow10月30日(13:45-14:45)

futagami
二上貴夫(Takao Futagami)
株式会社東陽テクニカ ソフトウェア・システム研究部 技術主幹

タイトル  
「組込みソフトウェアの高信頼化技術の現状」



概要
組込みソフトウェアを高信頼化するための方法として
1.開発工程に沿った技術的な取り組み
2.開発者、チーム、業界という集団の規約としての取り組み
3.開発技術者のスキルアップ教育からの取り組み
などがあげられます。

本講演では、これら複数の視点からみた高信頼化の努力を紹介します。
また、現在の組込みソフトウェア開発は、一般ソフトウェアの開発と比べると仕様記述や時間制約など高信頼性要求に関して特徴的な問題をかかえています。こうした問題群の指摘を行いたいと思います。


arrow10月31日(09:30-10:30)

yamaura
山浦恒央 (Tsuneo Yamaura)
東海大学 情報理工学部 ソフトウェア開発工学科 助教授

タイトル 「短納期ソフトウェア開発プロジェクトにおける残存バグ数の予測」


概要
西暦2000年を境に、Web系や組込み系プログラムが世の中に急速に浸透したため、ソフトウェア開発プロジェクトは、急速に納期が短くなり、また、バージョンアップの頻度が著しく増えた。一方、ソフトウェアは、社会の根幹部を支援する重要な要素であり、常に高品質を要求される。短期間に高品質ソフトウェアを開発するという社会的な要求を満足させる方法の一つとして、サンプリング法による残存バグ数の予測を取り上げる。この方式は、あらかじめ設計、作成したテスト項目の中から10%程度をサンプリングし、サンプリングしたテスト項目を段階的に実行することで、動的にプログラム中の残存バグ数を予測し、品質管理を実施するものである。


arrow10月31日(13:45-14:45)

Higashino
東野輝夫 (Teruo Higashino)
大阪大学 大学院情報科学研究科 教授

タイトル 「豊かで高信頼なアンビエントネットワークの構築をめざして」


概要
近年、ユビキタスネットワーク技術の発展に伴い、ユーザを取り巻くさまざまな情報機器がユーザの状況を理解し、快適な居住環境を創出するためのサービスを提供しようとしている。社会システムとしてそのようなサービスを提供するには、自律的に最適なネットワークを構築していくアンビエントネットワークの構築技術やネットワークアプリケーションの設計手法の開発が重要である。豊かで高信頼なアンビエントネットワークシステムを開発するには、シミュレーションや経験に基づく設計にとどまらず、実時間システムの設計検証技術や相互接続性試験技術などの形式記述技法を応用していく必要がある。本講演では、アンビエントネットワークシステムの構築に関連する設計検証技術や試験技術について解説する。


arrow11月01日(9:30-10:30)

Ono
田辺安雄 (Yasuo Tanabe)
株式会社日本機能安全 取締役 上級コンサルタント

タイトル 「IEC 61508の基本的枠組み」


概要
IEC 61508(JIS C 0508)が制定されて、すでに6年が経過した。IEC 61508は、システムのリスクを評価し、これを軽減するために設置される電気・電子・プログラマブル電子安全関連系の設計の要求事項を規定しているが、同時に適合のためのマネージメント規格としても位置づけられている。対象とする産業界を特定していない上、難解であるという指摘も多い。ドイツや英国では、製品や組織認証など規格の趣旨に従った適合認証が開始されており、輸出産業を中心に国内企業にも影響が出始めている。ここ数年、国内においても、規格の重要性についての認識が深まるとともに、規格に対する理解への要望も多い。本講演では、機能安全の基本的な考え方について解説する。

チュートリアル

arrow10月30日(17:15-18-15)
takai

高井利憲 (Toshinori Takai)
産業技術総合研究所システム検証研究センター 

タイトル
「クリーニ代数によるプログラム解析入門」


概要
クリーニ代数は、正則表現の代数系である。正則表現がコンピュータの世界でいたるところに現れることから、クリーニ代数はそれだけで重要であるといえるが、クリーニ代数の拡張であるテスト付きクリーニ代数は、プログラム解析にも使える非常に便利な道具である。本チュートリアルでは、クリーニ代数およびテスト付きクリーニ代数について簡単に紹介した後、いくつかの例を用いて、プログラム解析への応用について説明していく。なお、本講演の内容は、コンピュータソフトウェアVol.23, No.3, pp.14-34(2006年6月号)、クリーニ代数入門(古澤仁、高井利憲)に基づく。

arrow10月31日(16:45-17:45)
aist_tanabe

田辺良則 (Yoshinori Tanabe)
産業技術総合研究所システム検証研究センター 

タイトル
「形式的体系の定理証明支援系上での実現法」
著者: 木下佳樹、高橋孝一、田辺良則、湯浅能史(産業技術総合研究所)

概要
本チュートリアルでは、形式的体系を符号化し、定理証明支援系によって実現するための基本的な手法を解説する。例として、Martin-Loef型理論に基づく定理証明支援系Agdaをとりあげ、これによってホア論理の符号化を行い、その健全性の証明を実行する。Agdaについてもホア論理についても、特段の予備知識を仮定しない。ホア論理を知っている読者にとっては、Agdaによる符号化の解説になり、Agdaを知っている読者にとっても、ホア論理の解説になるよう試みる。


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