Towards Integrating Adaptation and Model Checking for Software Components

スポンサーリンク

概要

• 論文の詳細を見る

• This paper introduces a framework which converts adaptation for software components into a model checking problem so that one can design/generate adaptor and also perform verification with specifications. In this framework, software components are modeled by interface B?chi automata to capture the input/output protocol and continuous running behavior, and an adaptor is modeled by pushdown automaton to capture the infinite capacity of storing received messages. The adaptation with model checking includes two stages: mismtach detection and adaptor generation. On the first stage, system behavior of a composable components is computed by synchronous composition. LTL model checking is applied with given behavior mismatch property to detect whether mismtaches exist. On the second stage, a special adaptor called "coordinator" is build for the system to guide the adaptor generation with counterexample. Also, a simple example is used for demonstration.

• 一般社団法人情報処理学会の論文
• 2009-06-25

著者

• Takuya Katayama

  School Of Information Science Japan Advanced Institute Of Science And Technology

• Lin Hsin-hung

  School Of Information Science Japan Advanced Institute Of Science And Technology

関連論文

• Towards Integrating Adaptation and Model Checking for Software Components
• Towards Integrating Adaptation and Model Checking for Software Components

スポンサーリンク