Towards Automated Design-Time Explainability of Assurance Cases and Trade Spaces

Formal methods for model-based systems engineering have matured significantly in recent years, with new tools and approaches successfully demonstrated in various safety-critical and real-time domains. However, a key remaining barrier to more widespread adoption of these tools and techniques is explainability. It is impractical to require a user of such tools to understand all of the details of model synthesis, analysis, transformation, and implementation, yet some level of understanding is required to make effective use of these tools. Furthermore, designers must be able to explain their use of the tools to each other and stakeholders to establish confidence in the overall results. This paper presents a vision of how different formal methods techniques for model-based systems engineering can be integrated to automate the production of explainable feedback regarding assurance and optimization at design time.