Verification of Component-Based Software Application Families

We present a novel approach which facilitates formal verification of component-based software application families using model checking. This approach enables effective compositional reasoning by facilitating formulation of component properties and their environment assumptions. This approach integrates bottom-up component verification and top-down system verification based on the concept of application family architectures (AFA). The core elements of an AFA are architectural styles and reusable components. Reusable components of a family are defined in the context of its architectural styles and their correctness properties are verified in bottom-up component compositions. Top-down system verification utilizes architectural styles to guide decomposition of properties of a system into properties of its components and formulation of assumptions for the component properties. The component properties are reused if already verified; otherwise, they are verified top-down recursively. Archit...

• Type: Conference
• Year: 2006
• Where: CBSE
• Authors: Fei Xie, James C. Browne
• Keywords: Architectural Style, Bottom-up Component, CBSE 2006, Component Properties, Software Engineering