An incremental verification framework for component-based software systems
Kenneth R. Johnson, Radu Călinescu, Shinji Kikuchi · 2013
We present a tool-supported framework for the efficient reverification of component-based software systems after changes such as additions, removals or modifications of components. The incremental verification engine at the core of our INcremental VErification STrategy (INVEST) framework uses high-level algebraic representations of component-based systems to identify and execute the minimal set of component-wise reverification steps after a system change. The generality of the INVEST engine allows its integration with existing assume-guarantee verification paradigms. We illustrate this integration for an existing technique for the assume-guarantee verification of probabilistic systems. The resulting instance of the INVEST framework can reverify probabilistic safety properties of a cloud-deployed software system in a fraction of the time required by compositional assume-guarantee verification alone.