An Approach to Refining Active Components Based on Component Calculus
一种基于构件演算的主动构件精化方法

Modern component-based systems consist of active components that execute in parallel,which brings great difficulties in verifying correctness.By extending component calculus,a theory concerning refinement of active components is proposed.For interfaces,contracts are introduced which give functional specifications for both public methods and active action in terms of guarded designs.Then,a contract's dynamic behavior is defined by a pair of divergences/failures sets.The refinement relation between contracts is defined as the set inclusion of their divergences/failures sets.The theories applying simulation techniques to assure the refinement relation are proved. By defining the semantics of a component as a mapping from the contract of its required interface to the contract of its provide interface,component refinement can be proved in terms of contract refinement.When the component- based systems are being constructed in a bottom-up manner,the application of the refinement method together with the composition rule can guarantee their correctness.