Decompositional verification of component-based systems-a hybrid approach

Component-based software development has been increasingly adopted as a standard engineering practice to build large systems with prefabricated components. Although this development method enjoys the great benefits of reusing valuable software assets, reducing development costs, improving productivity, etc., it also poses serious challenges to the quality assurance problem of component-based systems, since prefabricated components can not be simply trusted and they could be a new source of system failures. Solving this problem is of vital importance to safety-critical and mission-critical systems. This paper introduces a decompositional verification approach for component-based systems through both formal analysis (model-checking) and traditional software testing