CVS

center-name

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

System Design Verification Technique Research Consortium

システム設計検証技術研究会 平成20年度第4回講演会

平成20年度第4回目のシステム設計検証技術研究会を終了いたしました。講演者の小池様、矢野様、そしてご参加いただきました30名の皆様にお礼申し上げます。

●日 時:12月05日(金)16:00-18:00
●講演者: 小池隆氏(富士ソフト株式会社 技術本部 研究開発センター生産技術研究室室長)
 <デモ> 矢野恭平氏(同、生産技術研究室)
●演 題:モデル検査支援ツールとその導入事例の紹介
●概 要:モデル検査の利用にはモデル記述言語と時相論理の習得が必要であり、開発現場への導入は容易ではありません。そこで、状態遷移表からSPIN検査モデル(Promelaプログラム)を自動生成する、 モデル検査支援ツールを開発しました。本ツールは、状態遷移表と関連付けて表形式で入力した制約条件から、 Promelaプログラム内にassertを出力するため、線形時相論理(LTL)式を記述しなくても多くの 事項を検証することができます。また、状態遷移表からLTLを自動生成して、バッチ処理でLTL検査を実施することもできます。さらに、SPINモデル検査で得られた反例を状態遷移表上の動作シーケンスとして再現し、 状態遷移表のデバッグを支援します。本発表では、デモを交えてツールを紹介し、開発現場への導入事例について報告します。 
●会 場: 産業技術総合研究所 システム検証研究センター 千里オフィス6F会議室

Mr.Koike
小池氏
Mr.Koike
小池氏、矢野氏
Lecture
講演風景



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