抄録
B-027
時間ペトリネットでモデル化されたGALSシステムを対象としたUPPAALによる自動検証手法
◎三輪陽介・横川智教（岡山県大）・宮崎　仁（川崎医療福祉大）・近藤真史・佐藤洋一郎（岡山県大）
本稿では，時間ペトリネット（TPN）でモデル化された大域非同期局所同期（GALS）システムの設計をモデル検査を用いて検証する手法を提案している． 検証にはモデル検査ツールUPPAALを用いる． 本手法では，TPNからUPPAALの入力形式である時間オートマトン（TA）への変換を行うことで検証を実現している． まず，各プレイスの振る舞いをTAで表現し，各トランジションの振る舞いをTA間の同期で表現することでTPN全体の振る舞いを表現している． さらに，GALSシステムが満たすべき特性をUPPAALのクエリ言語で表現している． 最後に，既存手法との比較実験を行っている．