Component technologies are gaining acceptance in the software systems engineering community as effective tools for quickly assembling complex software systems. Verification during initial deployment and, more importantly, after each "component substitution" is crucial.
Component-based software systems naturally allow scope for applying compositional formal verification techniques, e.g., assume-guarantee reasoning (AGR). The prime bottleneck in applying AGR to industrial systems is the difficulty of manually generating these assumptions. The research will focus on developing a new model checking-based framework that allows designers to replace components on-demand and locally re-verify the correctness of the new assembly. This framework will automatically generate assumptions for AGR and efficiently reuse the verification results from the previous assembly. AGR techniques will be developed to handle components interacting via general modes of communication like message-passing and shared memory. Industrial benchmarks will be used to evaluate our research accomplishments. By exploiting the compositionality of the proposed method, the verification techniques will be able to scale to larger component-based designs.
Broader impacts of our research include improvement in dependability of component-based software via efficient verification methods and dissemination of research results in academic courses and publications and publicly available tools.
