University of Minnesota
Software Engineering Center

You are here

Resolute: An Assurance Case Language for Architecture Models

Date of Publication: 
April 2016
Associated Research Groups: 
Publication Files: 
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 represented with a graphical interface, that presents and supports 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 assurance cases based on 1) a system model specified in an architectural 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 automatically generated assurance cases exceeds those of traditional assurance case arguments because of their more formal logical foundation and direct connection to the architectural model.
Appeared at the International Conference on High Integrity Languages and Tools, Portland, Oregon, October 18-21, 2014.
@inproceedings{Gacek:2014:RAC:2663171.2663177, author = {Gacek, Andrew and Backes, John and Cofer, Darren and Slind, Konrad and Whalen, Mike}, title = {Resolute: An Assurance Case Language for Architecture Models}, booktitle = {Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology}, series = {HILT '14}, year = {2014}, isbn = {978-1-4503-3217-0}, location = {Portland, Oregon, USA}, pages = {19--28}, numpages = {10}, url = {}, doi = {10.1145/2663171.2663177}, acmid = {2663177}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {aadl, architecture models, assurance case, avionics}, }