AIST

center-name

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

第二回
システム検証の科学技術シンポジウム
プログラム(参加者専用ページ)

Logo

【2005年10月20日(木)】
 9:50-10:00 ●開会挨拶●
10:00-10:30 ●基調講演●
  システム検証の科学研究とフィールドワーク
木下佳樹(産業技術総合研究所)
10:40-11:55 ●一般講演● 25分×3
  状態遷移表のモデル検査
松本充広(福岡県産業・科学技術振興財団福岡知的クラスター研究所および九州大学大学院)、穴田啓樹、上島大輔
渡辺政彦(キャッツ株式会社)、福田晃(九州大学大学院)
  ISO/IEC15408に基づく定理証明とモデル検査による情報セキュリティ仕様の検証技法
森本祥一、重松真二郎、後藤祐一、程京徳(埼玉大学大学院 )
  ソフトウェアの安全性/機能安全規格に基づくソフトウェアの設計と認証
吉岡律夫(日本環境認証機構・技術部および日本システム安全研究所)、植木克彦(東芝・ソフトウェア技術センター)
11:55-13:00 昼食
13:00-14:00 ●チュートリアル●
計算と論理をコンピュータ上に実現するための自然枠組
佐藤雅彦(京都大学大学院)
14:10-15:25 ●一般講演● 25分×3
A Static Analysis using Tree Automata for XML Access Control ⇒スライドpdf
Isao Yagi, Yoshiaki Takata, and Hiroyuki Seki(Graduate School of Information Science Nara Institute of
Science and technology)
Mullerオートマトンを用いたリアクティブシステムの仕様検証法とその完全性 ⇒スライドpdf
萩原茂樹、米崎直樹(東京工業大学大学院)
From Safety Analysis to Formal System Specification and Verification with OTS/CafeOBJ
⇒スライドpdf

Jianwen Xiang(Japan Advanced Institute of Science and Technology(JAIST)), Kazuhiro Ogata(Japan Advanced
Institute of Science and Technology(JAIST), NEC Software Hokuriku, Ltd.), Weiqiang Kong,
Kokichi Futatsugi(Japan Advanced Institute of Science and Technology(JAIST))
15:35-16:50 ●一般講演● 25分×3
モデル検査の実用化に向けた取り組みと事例報告 ⇒スライドpdf
早水公二(メルコ・パワー・システムズ(株))、篠崎孝一(関西電力(株)電力技術研究所)、星野光勇(メルコ・パワー・
システムズ(株))
鉄道信号システムの連動図表と連動装置のモデル検査 ⇒スライドpdf
越村三幸(九州大学大学院)、川村正(三菱電機(株))、大神茂之(西日本電信電話(株))、清水亮((株)デンソー)
藤田博、長谷川隆三(九州大学大学院)
同期型言語を用いたクルーズコントロールシステムの検証 ⇒スライドpdf
足立正和(大阪大学大学院)、富永孝、佐野範佳(豊田中央研究所)、潮俊光(大阪大学大学院)
17:00-17:50 ●招待講演1●
組込みシステム開発の課題と検証技術 ⇒スライドpdf
高田広章(名古屋大学大学院)
18:00-20:00 ●懇親会●
【2005年10月21日(金)】
 9:30-10:20 ●招待講演2●
システムの検証とは? ⇒スライドpdf
岸田孝一((株)SRA先端技術研究所(SRA-KTL))
10:30-11:20 ●一般講演● 25分×2 
モジュラーな代数仕様言語のための項書き換えシステム ⇒スライドpdf
中村正樹、二木厚吉(北陸先端科学技術大学院大学)
高階書換えシステムのモジュラ性 ⇒スライドpdf
岩見宗弘(島根大学)
11:30-12:20 ●一般講演● 25分×2 
モデル作成にもとづくレビュー手法の提案-Webアプリケーションの基本設計に対して- ⇒スライドpdf
渡邊宏(産業技術総合研究所)、河本貴則(奈良先端科学技術大学院大学)
Formal Modeling and Verification of Workflows with Security Considerations
⇒スライドpdf

Weiqiang Kong(Japan Advanced Institute of Science and Tachnology(JAIST)), Kazuhiro Ogata(Japan Advanced
Institute of Science and Tachnology(JAIST) and NEC Software Hokuriku, Ltd.), Kokichi Futatsugi(Japan
Advanced Institute of Science and Tachnology(JAIST)
12:20-13:20 昼食
13:20-14:10 ●招待講演3●
論理的方法と代数的方法 ⇒スライドpdf
小野寛晰(北陸先端科学技術大学院大学)
14:20-15:20 ●ポスターセッション●
Kleene category as a model of calculation
Takeuti Izumi(National Institute of Advanced Industrial Science and Technoogy(AIST) )
抽象化検証ツールTLATの構築に向けて ⇒スライドpdf
田辺良則、関澤俊弦、湯浅能史(産業技術総合研究所および科学技術振興機構)、高橋孝一(産業技術総合研究所)
宇宙機搭載ソフトウェアにおけるモデル検査技法の適用について
石濱直樹、片平真史(宇宙航空研究開発機構)、星野伸之(有人宇宙システム)
OTS/CafeOBJメソッドにおける検証譜生成・表示のためのツールキット
清野貴博(北陸先端科学技術大学院大学)、緒方和博(北陸先端科学技術大学院大学、NECソフトウェア北陸)
二木厚吉(北陸先端科学技術大学院大学)
モデル検査ツールUppaalによるJAVA仕様記述支援
田辺誠(宇部工業高等専門学校)
抽象時間モデルのもとでのプロトコルのDoS攻撃耐性解析
池田立野、日高武尊、西崎真也(東京工業大学大学院)
P2Pファイル配布システムにおけるピア欠損修復アルゴリズムに関する検証
高木理、山田修司、安田豊(京都産業大学)
形式的技法の便益性評価のためのデータ収集実験-Webシステムの上流設計工程において-
⇒スライドpdf
古澤仁、渡邊宏(産業技術総合研究所)、河本貴則(奈良先端科学技術大学院大学)、崔銀惠(産業技術総合研究所)
車載メータへのモデル検査適用 ⇒スライドpdf
古橋隆宏(矢崎総業(株))
15:35-16:50 ●一般講演● 25分×3 
A Framework for Description and Verification of Integrated Services of Home Network Systems
⇒スライドpdf
Pattara Leelaprute(Graduate School of Information Science and Technology, Osaka University)
Masahide Nakamura(Graduate School of Information Science, Nara Institute of Science and Technology)
Tatsuhiro Tsuchiya(Graduate School of Information Science and Technology, Osaka University)
Ken-ichi Matsumoto(Graduate School of Information Science, Nara Institute of Science and Technology)
Tohru Kikuno(Graduate School of Information Science and Technology, Osaka University)
時間論理タブロー証明器のMPIによる実装 ⇒スライドpdf
安藤崇央、大滝大輔、米崎直樹(東京工業大学大学院)
リアクティブシステムを対象とした様々な実行時検証概念の形式化とその判定アルゴリズムの完全性
島川昌也、萩原茂樹、米崎直樹(東京工業大学大学院)
16:50-17:00 ●閉会挨拶●

(独)産業技術総合研究所 システム検証研究センター
Copyrights (C) 2005-2006 AIST Research Center for Verification and Semantics, All Rights Reserved.