Institute of Information Science Academia Sinica
Topic: Automated Adaptor Generation for Behavioral Mismatching Software Components Using Pushdown Model Checking
Speaker: Dr. Hsin-Hung Lin (JAIST, Japan)
Date: 2012-01-04 (Wed) 10:00 – 12:00
Location: Auditorium 106 at new IIS Building
Host: Dr. Bow-Yaw Wang


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.