Assuring evolving large-scale systems (i.e., systems with multiple subsystems) can be a bottleneck in deploying capabilities with the speed and confidence needed for current Department of Defense (DoD) missions. There is no easy way to automatically integrate the complex web of interacting assurance techniques (i.e., for control stability, timing, security, logical correctness, and more) from multiple interacting subsystems in a system. In addition, without awareness of assurance interdependencies and effective reuse of prior assurance, the cost and time required for re-assurance can skyrocket.

Re-assurance remains an unresolved challenge in realizing almost all DoD initiatives aimed at rapidly delivering combat system capabilities. To address this problem, our project will use the concept of formal argument architecture: an artifact that imparts structure to the set of interacting assurance analyses needed to show that a system is ready for fielding and allows reasoning over the composition of those analyses.

Our objective is to develop the representations, algorithms, and associated tooling for automatically capturing and evaluating an argument architecture for a system from the argument architectures of its subsystems. This will accelerate assurance by reusing verification results of subsystems to assure global system properties and increase assurance confidence by using formal proof techniques. Achieving this objective requires developing a vehicle for composing assurance techniques with varying levels of trust in a manner that preserves the soundness of the results. We have developed a logic that supports rely-guarantee reasoning even when different levels of trusts are involved. We believe this is key to formally integrating different kinds of analysis results. The sound reuse of assurance results will remove one of the barriers to achieve the capability to deliver speed that the DoD needs.