基于GALS的多核体系结构安全攸关实时系统设计与验证方法研究

It is an important trend to use multi-core architecture in design of Safety-Critical Real-Time System now. From the view of multi-clock synchronous model, this project is concentrated on the method of multi-core system design and verification in Globally Asynchronous Locally Synchronous (GALS) based on the theories of Model- Driven development. The study will include: the extension of AADL standard for globally asynchronous modeling of multi-core architecture, the definition of semantics model called concurrent kernels for synchronous model to describe the model’s locally behavior’s deterministic and constraints in synchronous execution and to give the formal definition of concurrent structure abstract semantics model to support from synchronous model to multi-core platform, and the method of model transformation from the AADL-X model to synchronous model and proof of validity. The code generation from Signal model to OpenMP will be partly implemented based on the clock calculus and equation partition to complete a perfect technology chain. Based on the development flow, a prototype of platform for software design and verification of multi-core architecture will be established and a case study of typical avionics system will be demonstrated.

在安全攸关实时系统设计中，引入多核体系结构是当前一种重要趋势。本课题基于模型驱动的理论和方法，从多时钟同步模型视角，研究适应多核环境的全局异步局部同步（GALS）模式的系统设计与验证方法。通过对AADL体系结构语言标准进行多核属性的扩展，支持多核体系结构的全局异步建模；通过定义语义模型同步并发核，研究同步模型多核下的局部并发行为约束性和确定性，并对并发结构进行抽象语义形式化描述，以支持同步模型到多核平台的转换映射；然后，研究模型转换方法，将扩展的AADL-X模型转换到同步模型，并对转换的语义保持进行证明；最后，研究同步语言多时钟演算及同步方程并行划分方法以支持同步语言SIGNAL到并发结构实例OpenMP的代码自动生成，形成较完整的技术链。在此研究基础上，拟集成构建一个可支持多核体系结构软件设计与验证的原型平台，选取典型安全攸关实时系统案例进行验证性应用。

本项目针对安全关键系统软件，采用形式化理论与方法，深入地研究了多核环境下全局异步局部同步模式（GALS）的系统设计与验证方法，包括AADL体系结构语言标准扩展、同步语言并发核与并发结构、多核模型转换方法等。并扩展研究视野，把形式化方法应用在云服务验证和智能合约等新安全关键应用软件的验证中，取得了多个创新性成果。. 研究了AADL的多核扩展属性方法，增加了多核平台下任务分配与调度、通信与同步等内核描述；提出携带时钟信息的同步自动机模型，扩展了定时和同步行为的语义模型，是对AADL附件重要的多核扩展。. 研究了同步并发核模型，给出了基于SIGNAL的行为和时间转换语义，提出了多核并发结构的概念和语义模型，用于支持描述应用程序的并发行为；给出了基于模板的AADL代码跨平台自动生成方法，可支持AADL多核扩展转换为同步语言模型。. 研究了多核并发模型转换方法，创新性提出了基于布尔方程解析的多时钟演算方法，给出了SIGNAL到多核并发结构实例OpenMP代码自动生成方法；此外，还研究了SIGNAL到嵌入式语言Verilog的自动转换方法，给出了转换正确性的证明方法。成果集成进了SIGNAL的开源编译器,具有重要的实用价值。. 提出了形式化验证的中间件，可部分解决语言对平台依赖的问题；提出服务验证组合的代数优化方法，节省了验证过程的时间和成本；研究给出了基于Event-B形式语言的智能合约自动建模与验证方法，可有效解决智能合约的潜在漏洞和提高开发的效率。. 研发了系列模型验证与自动转换工具，已应用在航天多个安全关键系统领域，取得了显著的社会和经济效益，其中“天地一体化信息系统设计验证与仿真”获得2018年中国产学研创新成果二等奖；发起成立了中法联合实验室，在该领域每年与法国权威单位都有师生短期访问和交流，培养的研究生多人获学校和北京市优秀毕业生称号；首次在国内举办了项目负责人为主席的形式化方法领域著名的ACM/IEEE MEMOCODE 2018国际会议，增强了国内形式化方法研究在国际上的影响力，项目组成员也多次参加国际学术会议并作学术报告。