Lucia Cloth, "Model Checking Survivability"

Survivability is the ability of a communication system to provide essential services in the presence of external attacks or internal failures, and recover full service in a timely manner. This is not the only available definition of survivability, but we choose it as a starting point for assessing system survivability by means of model checking. We represent a communication system as a continuous-time Markov chain. Survivability as defined above is phrased as a formula in the logic CSL. We can then automatically check the validity of the survivability formula for the CTMC model. Care has to be taken when defining the model: we might include the random occurrence of failures and repairs. This allows us to include constraints on the long run behaviour of the system into our survivability formula. But we can also opt for a model where we assume failures to have already happened. In this case we can only reason about the recovery of full service.