Resolute: An Assurance Case Language for Architecture Models

Arguments about the safety, security, and correctness of a complex system are often made in the form of an assurance case. An assurance case is a structured argument, often rep-resented with a graphical interface, that presents and sup-ports claims about a system’s behavior. The argument may combine different kinds of evidence to justify its top level claim. While assurance cases deliver some level of guarantee of a system’s correctness, they lack the rigor that proofs from formal methods typically provide. Furthermore, changes in the structure of a model during development may result in inconsistencies between a design and its assurance case. Our solution is a framework for automatically generating assur-ance cases based on 1) a system model specified in an archi-tectural design language, 2) a set of logical rules expressed in a domain specific language that we have developed, and 3) the results of other formal analyses that have been run on the model. We argue that the rigor of these automati-cally generated assurance cases exceeds those of traditional assurance case arguments because of their more formal log-ical foundation and direct connection to the architectural model