The Component Substitution Problem for Software Systems

提案编号：CCF-0541245 PI：Edmund M.ClarkeCarnegie Mellon大学标题：软件系统的组件替换问题组件技术正在软件系统工程界作为快速组装复杂软件系统的有效工具获得认可。在初始部署期间以及更重要的是，在每次“组件替换”之后进行验证是至关重要的。基于组件的软件系统自然允许应用组合形式验证技术，例如假定-保证推理(AGR)。将AGR应用于工业系统的主要瓶颈是手动生成这些假设的难度。这项研究将专注于开发一种新的基于模型检查的框架，允许设计师按需更换零部件，并在本地重新验证新组装的正确性。这一框架将自动生成AGR的假设，并有效地重复使用上一次汇编的核查结果。将开发AGR技术来处理通过常规通信模式(如消息传递和共享内存)进行交互的组件。行业基准将被用来评估我们的研究成果。通过利用提出的方法的组合性，验证技术将能够扩展到更大的基于组件的设计。我们研究的更广泛影响包括通过有效的验证方法改善基于组件的软件的可靠性，以及在学术课程和出版物以及公开可用的工具中传播研究结果。

Proposal Number: CCF-0541245 PI : Edmund M. ClarkeCarnegie Mellon University Title: The Component Substitution Problem for Software SystemsComponent 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.