MARTE (abbreviated for Modeling and Analysis of Real-Time and Embedded systems) is a UML profile, used to facilitate the design and analysis of real-time and embedded systems. The Clock Constraint Specification Language (CCSL) is a formal language companion to MARTE, which is proposed to specify the constraint of the occurrences of events in systems. However, the language lacks efficient verification support to the formal analysis of temporal properties which are important to real-time and embedded systems. In this paper, we propose an SMT-based approach to model checking of the temporal properties specified in Linear Temporal Logic (LTL) for CCSL. We implement a prototype tool for the proposed approach and use the state-of-the-art tool Z3 as the underlying SMT solver. We model two practical cases including a traffic light controller and a power window system in CCSL, and verify LTL properties of the two systems using the proposed approach. Experimental results demonstrate the effectiveness of our approach.