A Lightweight Code Analysis and its Role in Evaluation of a Dependability Case

Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang, and Daniel Jackson
Massachusetts Institute of Technology, USA

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 complex medical device. The key novelty of the approach used is a lightweight code analysis that generates a list of side conditions, corresponding 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 dependability might be improved.