您的瀏覽器不支援JavaScript語法,網站的部份功能在JavaScript沒有啟用的狀態下無法正常使用。

中央研究院 資訊科學研究所

活動訊息

友善列印

列印可使用瀏覽器提供的(Ctrl+P)功能

學術演講

:::

Automated Adaptor Generation for Behavioral Mismatching Software Components Using Pushdown Model Checking

  • 講者林信宏 博士 (JAIST, Japan)
    邀請人:王柏堯老師
  • 時間2012-01-04 (Wed.) 10:00 ~ 12:00
  • 地點本所新館一樓106演講廳
摘要

Software adaptation is a promising solution for behavioral mismatching software components by introducing a special component that controls interactions of components by exclusively synchronizing with components.

Current approaches of adaptation focus on behavioral mismatches based on automata modeling. Adaptors can be automatically generated by given behavior interfaces of components represented by automata model, and adaptor contracts designed by developers.However, two issues of current approaches have to be addressed. First, behavioral mismatches may result in the need of a non-regular behavioral adaptor, which is not supported by automata modeling. Second, adaptation contracts are manually designed with limited tool support.

 

This work tempts to solve the two issues of adaptation by a novel approach of adaptor generation. The approach uses pushdown systems model as behavioral interfaces of adaptors so that non-regular behavior is able to be expressed. The idea of adaptor generation is letting algorithms of pushdown model checking search for the negation of necessary properties of an over-behavioral pushdown system and generate counterexamples satisfying the properties. These counterexamples, which are correct traces, are then used to build behavior interfaces of adaptors.

Thus, the approach can achieve fully automated adaptor generation. In order to automatically capture necessary properties, behavior interfaces of components are remodeled with additional constraints to force the revelation of implicit information. The effectiveness of the approach is shown by generating a non-regular behavioral adaptor for a system of behavioral mismatching web service. Also, signature mismatches and branchings are taken into consideration for supporting general cases of adaptation.