Incorporating Constraints to Software System Survivability Specification and Proof

In component-based and model-driven approaches for software engineering, any software components or subsystems acquired from external sources must meet a user´s criteria to ascertain that they will not compromise the survivability properties of the existing systems. In this paper, we study survivability compliance specification and verification in a proof-carrying scenario: a user defines survivability requirements for a software system to be acquired or linked to the existing systems. The system provider compiles a proof, which is sent to the user who simply needs to check it. We present a new formalism, i.e., a constraint annotated logic in which arbitrary user requirements and constraints for system survivability features can be represented and reasoned. We provide a formal design of a constraint domain and extend a proof-carrying survivability logic so that user-defined constraints can be enforced by prohibiting logical inferences that would violate these constraints. In our model, the interplay between a constraint domain and the logical reasoning process is directly supported by the logic rules. Experiments and analysis show that the proposed model is a powerful formalism in reasoning hybrid domains between users´ constrained requirements and system survivability properties.