A Lightweight Code Analysis and Its Role in Evaluation of a Dependability Case
A dependability case is an explicit, end-to-end argument, based on concrete evidence, that a system satisfies a critical property. The authors report on a case study constructing a dependability case for the control software of a medical device. The key novelty of their approach is a lightweight code analysis that generates a list of side conditions that correspond to assumptions to be discharged about the code and the environment in which it executes. This represents an unconventional trade-off between, at one extreme, more ambitious analyzes that attempt to discharge all conditions automatically (but which cannot even in principle handle environmental assumptions), and at the other, flow- or context-insensitive analyzes that require more user involvement.