Many software systems are not verified because it is expensive – both financially and temporally – to show a system is 100% correct. Additionally, many systems do not need total correctness; some systems may tolerate property violations as long as they eventually recover. If a property requires that an invariant holds at all times during execution, it may be more important for the system to recover from the invariant violation than for the violation itself to be removed. We analyze systems to compute their recoverability – if an invariant is violated in the system, is it possible to return to a safe state from that violation. Addtionally, we examine different categorizations of recovery; if an invariant is violated multiple times, it may be possible to return to a safe state after some violations, but not others. The actions required to return to safety are also in question, especially if some actions require human intervention to return to safety. A system that can always recover from an invariant violation may be less safe than a completely correct system, but we explore the possibility that it is easier to guarantee recoverability than correctness of a system.
Unpredictable changes to the environment of a cyber-physical system introduce the potential for unsafe operating conditions. Should components of an architecture be subject to cyber attacks, hardware failures, or adverse environmental conditions, it is important the safety-critical features still be functional to avoid dangerous conditions for users. Graceful degradation refers to systems where some components may experience failure, but the system maintains safety-critical features. The trust boundry of a system refers to the minimal set of components required before safety-critical features are sacrificed. Identifying trust boundaries and building systems with graceful degradation allow systems to prioritize select components to maintain safety, instead of focusing on all components.
We examine charging stations for electric vehicles as a case study on graceful degradation and trust boundries. EV charging station have a large, modular architecture with a minimal interaction between local stations. Identifying the trust boundry for this system can show that graceful degradtion is applicable to real world systems and provides details of improvement regions to fulfillment of safety-critical requirements.