Critical infrastructures in several domains, such as power, medical, and finance, are becoming increasingly dependent on software systems. Effects of faults and intrusions on these systems can be disastrous. Survivability is defined as the ability of a system to maintain a set of essential services in the presence of faults and intrusions. In this talk, I will address the problem of analyzing survivability properties of specifications of systems. My methodology enables one to make important decisions related to survivability at the design phase. I am implementing a tool Trishul to automate the analysis. I will briefly describe some case studies I have finished using Trishul, and discuss some larger case studies that are on going. One of the case studies is a model of a trading floor of a major investment bank. I will also discuss some interesting results from that case study.

My methodology allows a software designer to incorporate accidental and malicious faults into a specification of a system and visualize their effect. This is similar to fault-injection-based testing albeit at the specification level. However, at the specification level, completeness is achieved by using exhaustive state-exploration based techniques, such as model checking. Visualization information is provided to the designer as a scenario graph, a structure that is automatically generated using model checking. Intuitively speaking, a scenario graph encapsulates all executions of a system that lead to an undesirable or unsafe state. I will also demonstrate how various kinds of analysis, such as reliability, expected latency, cost-benefit, and sensitivity analysis, can be performed on the scenario graphs. One of the unique features of my methodology is that it uses ideas from various areas, such as model checking and optimal control of stochastic processes. Additionally, independence of various events is not assumed. Independence assumption is quite common in the existing literature, but is not true in most realistic settings.