User-centric Communication Middleware (UCM) is proposed to provide a high-level unified user-centric communication abstraction for upper-layer communication applications by separating and isolating the complexities of network-level communication control and media delivery from the diversity of application-dependent communication logic Due to the complexity of UCM, it is a major challenge to ensure its correct design and implementation In this paper we present our approach for designing UCM through formal modeling and analysis based on SAM, a general formal framework for specifying and analyzing software architectures We present the formal model for UCM using SAM and provide a method to analyze SAM architectural specifications using model checker SPIN.
