A dependability case is an explicit, end-to-end argument, based on
concrete evidence, that a system satisfies a critical property. We
report on a case study constructing a dependability case for the
control software of a medical device. The key novelty of our 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
analyses that attempt to discharge all conditions automatically (but
which cannot even in principle handle environmental 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.