Integrating formal methods with testing for reliability estimation of component based systems

Large scale complex software systems are usually built following component based modeling and design methodologies. For such complex software, system level reliability estimation is a non-trivial problem due to the intricate combinatorial relationships which may exist between component reliabilities and the overall system level reliability. A formal modeling of the interactions among components in terms of reliability thus becomes a desirable design attribute. The present work proposes a method for reliability estimation of such systems, by leveraging techniques from the domain of program analysis. The overall system behavior including the interactions with external components is modeled by high-level behavioral descriptions tagged with reliability assertions. These assertions act as preconditions guaranteeing successful execution of components. We present an efficient algorithm for system level reliability estimation at a desired time instant along with suitable case studies illustrating the usefulness of the proposed approach.