Mechanized Support For Assurance Case Argumentation

John Rushby

Presented at The 1st International Workshop on Argument for Agreement and Assurance (AAA 2013), Kanagawa Japan, October 2013; proceedings published as Springer LNAI vol. 8417 Y. Nakano, K. Satoh, and D. Bekki (Eds), pp. 304-318.


An assurance case provides an argument that certain claims (usually concerning safety or other critical properties) are justified, based on given evidence concerning the context, design, and implementation of a system. An assurance case serves two purposes: reasoning and communication. For the first, the argument in the case should approach the standards of mathematical proof (though it may be grounded on premises--i.e., evidence--that are equivocal); for the second it must assist human stakeholders to grasp the essence of the case, to explore its details, and to challenge it. Because of the scale and complexity of assurance cases, both purposes benefit from mechanized assistance. We propose simple ways in which an assurance case, formalized in a mechanized verification system to support the first purpose, can be adapted to serve the second.




BibTeX Entry

	AUTHOR = {John Rushby},
	EDITORS = {Yukiko Nakano and Ken Satoh and Daisuke Bekki},
	TITLE = {Mechanized Support for Assurance Case Argumentation},
	BOOKTITLE = {New Frontiers in {Artificial Intelligence:
		  {JSAI-isAI 2013 Workshops, LENLS, JURISIN, MiMI,
		  AAA, and DDS}, Revised Selected Papers},
	YEAR = 2013,
	PUBLISHER = {Springer-Verlag},
	ADDRESS = {Kanagawa, Japan},
	MONTH = oct,
	SERIES = {Lecture Notes in Artificial Intelligence},
	volume = 8417,
	pages = {304--318}

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page