A bidirectional graph transformation approach to analysis of concurrent software models

The application of model driven software development still faces strong challenges. One challenge we focus on here is analysis of concurrent software systems for detecting potential defects such as race conditions or atomicity violations. We adopt a BiG (Bidirectional Graph Transformation) approach to analysis of concurrent software models. The essential idea of our approach is that we choose labeled transition systems as the behavior model of the concurrent system, and then conduct model transformation and extract a labeled partial order view from the labeled transition systems for software analysis. The potential of BiG in this work is that model transformation is effectively supported based on queries, and models before and after transformation can also be synchronized automatically. This research is expected to benefit model-driven software development in that analysis of state models is lightweight and can be automated. It also provides the engineers with an interesting example about the application of bidirectional transformation to software analysis, which will encourage the improvement of BiG and its practical applications.