Systematic composition and verification of abstract components

This paper proposes a systematic composition method for supporting both top-down and bottom-up approaches within the same frame. The method composes behavioral models of unit (abstract) components with respect to the services to be provided by the abstract component after the composition. Adapted from the standard operations in process algebra, two types of abstract techniques, synchronized abstraction and projection abstraction, are introduced to abstract the compositional behavior of components depending on their port connections and bindings. This method enables systematic extraction of high-level component behavior and reduces the complexity of composition and verification. Experiments show that performance improves when compositions are verified formally.