近年来，物联网和人工智能技术的发展使得实时嵌入式系统成为诸多安全攸关领域设备的核心控制系统，如轨道交通系统、汽车无人驾驶系统等。这些系统大幅节省了人力成本，且更加安全、精准、高效。强实时性与高可靠性是这类系统的关键特征。保证系统的高可靠性和强实时性，并最大程度提高系统资源利用率是设计与开发这类系统的核心要求，如轨道交通系统中缩短列车进站时间间隔以提高车站利用率等。时钟约束建模语言CCSL是模型驱动的实时嵌入式系统开发方法MARTE的核心建模语言之一，用于描述系统中和时间相关的行为。它同时支持逻辑时钟和物理时钟的定义，具有强大的表达能力。针对该语言，研究如何利用形式化的方法严格、自动地分析系统的可调度性等重要性质，证明事件之间依赖关系的一致性，检验实际系统与模型的相符性，设计高效的验证与分析算法，开发统一验证与分析平台，对设计开发高可靠且强实时的嵌入式系统具有重要的理论与实践意义。

In recent years, with the fast development of Internet of Things and Artificial Intelligence, real-time embedded systems become the central control systems in many safety-critical domains such as rail transport control systems and vehicle unmanned systems. Such systems would save huge labor cost, and meanwhile are safe, precise and efficient. Strong real-time performance and high reliability are the two key features of such systems. In the design and implementation of such systems, the central requirement is to guarantee the two features and meanwhile to fully utilize system resources, such as shortening the time interval between two consecutive trains arriving at stations. CCSL is a new modeling language, designed for specifying the timed behaviors of real-time embedded systems. It is the key technique in the model-driven development method called MARTE (Modeling and Analysis of Real-Time Embedded Systems). It is expressive by supporting both logical clocks and physical clocks. As for CCSL, a central and badly-demanded work is to investigate efficient approaches for the scheduability analysis and property verification. The mission of this proposal is to design efficient verification algorithms and to develop a unified platform to provide tool support, which would have both theoretical and practical significance to the design and development of highly dependable and strong real-time embedded systems.