Abstract
Complex systems must be analyzed in smaller pieces.Analysis must support both bottom-up (composition) and top-down (refinement) development, and it must support the consideration of several critical properties, e.g., functional correctness, fault tolerance and security, as appropriate. We describe a mathematical framework for performing com-position and refinement analysis and discuss some lessons learned from its application. The framework is written and verified in PVS.