通信プロセスモデルによるAIBO OPEN-Rプログラムのデッドロックフリー解析手法

情報処理学会 Web Site 参考文献9件

書誌事項

タイトル別名
  • ツウシン プロセス モデル ニ ヨル AIBO OPEN R プログラム ノ デッドロック フリー カイセキ シュホウ
  • A Deadlock Free Analysis for AIBO OPEN-R Programs Based on Communicating Processes
  • 検証/テストとデバッグ

この論文をさがす

抄録

本論文ではAIBO プログラムの振舞いを通信プロセスモデルに基づいて表現し，デッドロックフリー解析を行う手法を提案する．AIBO プログラムの標準的開発環境OPEN-R で開発される並行オブジェクトは2 種の信号のやりとりによって同期される．この2 種の同期信号のやりとりをAIBOプログラムの抽象的な振舞いとしてとらえ，ソースコードの構造を保ったままπ 計算によってモデル化する．モデル検査器Mobility Workbench を用いて，ロボットにおける致命的な欠陥であるデッドロックの可能性を解析する．モデル検査時の状態爆発の問題に対応するため全体の振舞いを分割し，解析時の状態数を削減する．本論文における解析ではシステムのデッドロックを検出できるだけではなく，デッドロック発生の原因となるコンポーネントの特定が可能である．本論文ではヘッドセンサに反応してメッセージを表示するAIBO プログラムを用いた解析例を示す．

We propose a compositional analysis method to ensure deadlock freeness of AIBO programs based on communicating processes. Concurrent objects of AIBO programs with the OPEN-R API are synchronized by two types of signals: ready and notify. Focusing on these signals, we describe the abstract behavior of AIBO by the π-calculus along with the source code structure concerning synchronization between concurrent objects. We use the Mobility Workbench to check the deadlock capability. We present a decomposing method to reduce the combination of states of concurrent objects. When a deadlock possibility is pointed out, our method enables not only to detect deadlock of the whole system, but also to point out which component may cause the deadlock. We illustrate our method by an example of an AIBO program to display messages when its head sensor pushed.

収録刊行物

参考文献 (9)*注記

もっと見る

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ