Component Substitutability Behavior Consistency Verification Based on Architecture-driven Development

Component-based software development (short for CBSD) is to develop software systems by choosing appropriate components in the distributed environment to assemble a dependable software architecture, which satisfies requirements. This new paradigm plays a key role in the software engineering and also brings new challenges to the dependable software architecture design. In this paper, firstly we introduce an architecture description language-π-ADL to specify the software architecture based on component. Secondly based on Higher-Order π-calculus, we give a formal method to verify the behavior consistency of component substitutability. In this way, we can forecast errors and enhance the semantic correctness of the software architecture from the design stage.