記号モデル検査によるスマートオブジェクトの近接連携シナリオの効率的な検証

蓑田 玲緒奈  湊 真一  
(学生論文特集秀逸論文)

誌名
電子情報通信学会論文誌 D   Vol.J101-D   No.3   pp.470-480
発行日: 2018/03/01
Online ISSN: 1881-0225
DOI: 10.14923/transinfj.2017PDP0037
論文種別: 特集論文 (学生論文特集)
専門分野: ソフトウェアシステム
キーワード: 
ユビキタスコンピューティング,  触媒反応ネットワーク,  形式検証,  記号モデル検査,  スマートオブジェクト,  

本文: FreePDF(1.1MB)


あらまし: 
ユビキタスコンピューティング(UC)シナリオの検証は,UCの様々なアプリケーションを設計する際に,設計上の問題を実装の前段階で発見できるため有用である.本論文では,Context Catalytic Reaction Network (CCRN)で記述されたUCシナリオの記号モデル検査による検証を提案する.具体的には,CCRNを記号モデル検査問題に変換することで,筆者が過去に提案した素朴な手法では検証が困難であった大規模なUCシナリオの検証を現実的なコストで可能になることを実験的に示す.また,同じ枠組みでUCシナリオの有界モデル検査による欠陥検出の有用性についても実験的に示す.