Abstract
Survivability is an essential requirement of the networked information systems analogous to the dependability. The definition of survivability proposed by Knight in [16] provides a rigorous way to define the concept. However, the Knight's specification does not provide a behavior model of the system as well as a verification framework for determining the survivability of a system satisfying a given specification. This paper proposes a complete formal framework for specifying and verifying the concept of system survivability on the basis of Knight's research. A computable probabilistic model is proposed to specify the functions and services of a networked information system. A quantified survivability specification is proposed to indicate the requirement of the survivability. A probabilistic refinement relation is defined to determine the survivability of the system. The framework is then demonstrated with three case studies: the restaurant system (RES), the Warship Command and Control system (LWC) and the Command-and-Control (C2) system.
| Original language | English |
|---|---|
| Pages (from-to) | 2356-2370 |
| Number of pages | 15 |
| Journal | IEICE Transactions on Information and Systems |
| Volume | E97-D |
| Issue number | 9 |
| DOIs | |
| State | Published - Sep 2014 |
Keywords
- Probabilistic refinement
- Probability programs
- Survivability
- Survivability specification