D.: 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 crit-ical property. We report on a case study constructing a dependability case for the control software of a medical de-vice. The key novelty of our approach is a lightweight code analysis that generates a list of side conditions that corre-spond 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 am-bitious analyses that attempt to discharge all conditions au-tomatically (but which cannot even in principle handle envi-ronmental assumptions), and at the other, flow- or context-insensitive analyses that require more user involvement. The results of the analysis suggested a variety of ways in which the dependability of the system might be improved