Formal Assurance Arguments: A Solution in Search of a Problem?

An assurance case comprises evidence and argument showing how that evidence supports assurance claims (e.g., about safety or security). It is unsurprising that some computer scientists have proposed formalising assurance arguments: most associate formality with rigour. But while engineers can sometimes prove that source code refines a formal specification, it is not clear that formalisation will improve assurance arguments or that this benefit is worth its cost. For example, formalisation might reduce the benefits of argumentation by limiting the audience to people who can read formal logic. In this paper, we present (1) a systematic survey of the literature surrounding formal assurance arguments, (2) an analysis of errors that formalism can help to eliminate, (3) a discussion of existing evidence, and (4) suggestions for experimental work to definitively answer the question.