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. 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 contextinsensitive 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. Categories and Subject Descriptors D.2.9 [Software Engineering]: Design—Methodologies General Terms Software dependability...

• Type: Journal
• Year: 2011
• Where: ICSE
• Authors: Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang, Daniel Jackson
• Keywords: Design Methodologies, ICSE 2011, Problem Frames, Software Engineering, Software Engineering Design