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.
Abstract
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.
PDF
Slides
PDF
BibTeX Entry
@INPROCEEDINGS{Rushby:AAA13,
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