A (Proto) Logical Basis for the Notion of a Structured Argument in a Safety Case

摘要

The introduction of safety cases was a step in the right direction in regards to safety assurance. As presently practiced, safety cases aim at making a serious attempt to explicate, and to provide some structure for, the reasoning involved in assuring that a system is safe, generally in terms of so-called structured arguments. However, the fact current notations for expressing these structured arguments have no formal semantics and, at best, are loosely linked to goal structuring ideas and to Toulmin's notion of an argument pattern, is a crucial issue to be addressed. History clearly demonstrates that languages that have no formal semantics are deficient in relation to the requirements of a serious approach to engineering. In other words, one can only go so far with intuition, and certainly not far enough to justify the safety of complex systems, such as Cyber Physical Systems or autonomous cars. By rehearsing Gentzen's program for formalizing mathematical reasoning, his famous Calculus of Natural Deduction, we show how we can begin a program of formalizing safety reasoning by developing a working definition of a structured argument in a safety case and a calculus for safety reasoning.