- ホーム
- 会議・シンポジウム
- 国際会議・シンポジウム
- シンポジウムのお知らせ
シンポジウムのお知らせ
北陸先端科学技術大学院大学 21世紀COEシンポジウム
「検証進化可能電子社会」概要
数理的技法普及のために求められる技術と教育
木下 佳樹（ＡＩＳＴ）
数理的技法によるシステムの開発と検証は、どのような手順でおこなわれると
想定しているのかをのべ、各手順に必要な技術およびその基盤を与える科学的
知識を説明する。その上で、特に基盤を与える科学的知識についての教育が十
分になされているかを検討してみたい。
組込みソフトウェアを対象としたモデル検査による検証事例
高井 利憲（ＡＩＳＴ）
数理的検証法の一つであるモデル検査を，実際の組込みソフトウェアに適用し
た事例をいくつか紹介する．ソフトウェアをモデル検査で検証する場合，状態
爆発問題とよばれる問題によって，うまくいかない場合が多い．発表では，状
態爆発をいかに回避するかを中心に，検査対象のモデル化，モデル検査の実際，
発見したバグなどを説明する．
業務フロー図の検証
竹内泉（ＡＩＳＴ）
業務フロー図の検証は業務システムの要求仕様を記述するために
用いられている。業務フロー図を形式化することにより各種の検証
が可能になる。本研究では、形式化された業務フロー図に対し事象
独立性という概念を提示し、事象独立性を用いて業務フロー図のグ
ラフ構造の整合性の検証、及び、添付書類の出現の整合性の検証を
行なう。
CVS 教程に基づくモデル検査研修コース構築への取り組み
西原 秀明（ＡＩＳＴ）
産総研では，技術者向けのモデル検査教育のためのカリキュラム(CVS 教程)を策定し
それに沿って研修コースの作成を行っている．講演では CVS 教程の目標や内容を
説明し，コース作成の状況を紹介する．また今後の展望や作成の過程で得られた
フィードバックについても触れる予定である．
代数仕様言語による電子商取引プロトコルの解析
緒方和博（JAIST）
iKP (i = 1,2,3) 電子商取引プロトコルの解析に関する事例研究について報告
する。解析の目的は、iKPがある性質 (支払合意性) を満たすか否かを検査す
ることである。使用した記述言語および解析ツールは、代数仕様言語およびそ
の処理系である Maude である。
形式的手法の新展開-離散と連続の融合
平石邦彦（JAIST）
離散状態に対する形式的手法は，連続時間を含むリアルタイムシステム，離散状態と
連続状態を含むハイブリッドシステムへと発展してきている．さらに，大規模な離散
状態の集合上の状態遷移を流体の流れで近似する手法も提案されている．本講演では
離散と連続を融合した形式的手法，および，その応用分野について紹介する．
定理証明によるファイアウォールサーバの検証
矢竹健朗（JAIST）
オブジェクト指向モデル検証ツールObjectLogicを用いて
ファイアウォールのUMLモデルの検証を行った旨を述べる。
ファイアウォールの振る舞いをシーケンス図で定義し、
それがクラス図に付加されたOCL制約を満たすことを
定理証明により検証する。
マルチタスクソフトウェアの検証法
青木利晃（JAIST）
組込みソフトウェア開発ではμITRONのような優先度付きマルチタスクが扱え
るRTOS(Real-Time Operating Systems)を用いる場合が多い．この場合，並行
処理を直接的にプログラムできるが，その反面，動作やタイミングなどの検証
が困難になる．このような振舞の検証はモデル検査手法が得意とするところで
ある．そこで，この発表では，RTOSに基づいたソフトウェアをモデル検査手法
を用いて検証する手法について紹介する．
モデル検査手法の普及に関する取り組み
青木利晃（JAIST）
ソフトウェアの信頼性を向上させる技術として形式手法が注目されている．形
式手法には様々なものがあるが，その中でも，モデル検査手法に注目して普及
活動を行っている．形式手法を普及させるのが目的であるが，そのファースト
ステップとしては，モデル検査手法が適していると考えたからである．この発
表では，これまでの普及活動の概要と感触を紹介すると共に，今後の普及活動
の展開について述べる．
検証ツールの展開とそのカリキュラムでの利用
小川瑞史（JAIST）
近年、産業界においてもモデル検査の利用が散見されるようになってきたが、
ほとんどの場合がSPINである。ここでは、非標準的だが新たな展開の可能性
を持つ検証ツールの紹介、またモデル検査以外でも、充足検査器や定理証明
系の検証ツールの展開の状況を概観し、さらにここ数年、JAISTにおいて強
化してきた検証分野のカリキュラムへの取り組みについて紹介する。
