Hierarchical Contract-Based Synthesis for Assurance Cases

An automatic synthesis problem is often characterized by an overall goal or specification to be satisfied, the set of all possible outcomes, called the design space, and an algorithm for the automatic selection of one or more members from the design space that are provably guaranteed to satisfy the overall specification. A key challenge in automatic synthesis is the complexity of the design space. In this paper, we introduce a formal model, termed hierarchical contract nets, and a framework for the efficient automatic synthesis of hierarchical contract nets, based on a library of refinement relations between contracts and contract nets. We show, via the application of automatic synthesis of assurances cases, that hierarchical contract-based synthesis can mitigate the design space complexity problem. We also show that the approach can bring both the benefits of automating the creation of assurance cases and ensuring that the knowledge from the argumentation experts is captured and reflected in the synthesized assurance cases.