Interface Explorer: Automated Modular Verification of Complex Systems

Standard V&V techniques like code reviewing or testing provide insufficient guarantees on the reliability of critical software systems. The gap widens as the systems grow in complexity and the number of scenarios to consider is no longer tractable. Recently, automated analytic verification tools based on Abstract Interpretation have been successfully applied to the formal verification of large commercial software systems. While such tools work well for applications made of one block, they fail to analyze complex systems made of multiple interacting components, even at a small scale. There is an opportunity to leverage existing high-power Abstract Interpretation techniques and to develop a methodology that enables the automated verification of large complex systems. The approach we are proposing to investigate has two parts: (1) Instead of analyzing the whole system we use Abstract Interpretation techniques to analyze each component of the system together with a user-provided description of the interactions between the component and the rest of the system; and (2) The interactions between the subsystems are specified using a domain-specific language that is specially designed to model the external execution environment of a program in a simple yet effective way by the subject matter expert user.