Component Based Development - Where is the Place for Formalism?

A software component has a contract that specifies its properties and thus define conditions for its use. The contract is an obvious object for formalization. It could assist in conformance checking for manufactured components and in checking consistent use of them in a concrete system. However, our experience with development of a complex, software intensive system with heterogeneous components indicates thatstate of the art is a syntactical level of formalization with a little static type checking. More can be done, but it requires support from development tools and component frameworks. Here, we discuss, how invariant checking may be implemented, and how process calculus based frameworks may be very useful for checking communication patterns among components3