基于时钟约束建模语言CCSL的实时嵌入式系统形式化验证与分析

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.

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

时钟约束建模语言CCSL是模型驱动的实时嵌入式系统开发方法MARTE的核心建模语言之一，用于描述系统中和时间相关的行为。它同时支持逻辑时钟和物理时钟的定义，具有强大的表达能力。本项目研究了基于CCSL的系统可调度性建模与分析方法。通过该方法可实现事件之间依赖关系的一致性证明以及实际系统与模型的相符性验证，证明了CCSL的形式化验证问题是NP完全的这一理论结果，基于该结果提出了基于SMT等高效求解技术的验证与分析算法，开发了统一验证与分析工具，并在轨道交通领域的案例种进行了应用，说明了方法的可行性与有效性。本研究的结果对设计开发高可靠且强实时的嵌入式系统具有重要的理论与实践意义。依托本项目，课题组共发表高水平论文13篇(其中9篇为CCFA/B类推荐会议论文)，申请并获批相关专利1项，软件著作权4项，相关成果获得第26届亚太软件工程国际会议唯一最佳论文奖，培养硕士研究生7人，协助培养毕业博士研究生2人，举办了形式化方法领域国际知名会议3次。