国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍

为了满足国内某安全攸关领域的需求, L2C编译器的开发始于2010年9月, 其目标是设计实现一个经过形式化验证的可信编译器, 其源语言是面向领域的同步数据流语言Lustre*(Lustre语言的一个变种, 参考下一节), 目标语言是C, 最终可用作相关领域数字化仪控系统的安全级代码生成器.国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译步骤及其设计与实现。国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍

1、L2C编译器简介

L2C编译器的发展进程可归为3个里程碑.一个是面向Lustre的一个核心子集, 设计实现了L2C编译器的一个原型系统, 于2013年6月完成验收.另一个里程碑是已实现除嵌套时钟外Lustre全部特性的一个单时钟L2C编译器版本, 完全能够满足国内该安全攸关领域目前的实际应用需求, 并于2015年4月完成严格的企业级验收, 这些工作的相关技术和代码已在实际应用中发挥作用.

在上述第2个里程碑之后, 项目组对L2C编译器的设计框架进行了较大程度的优化调整, 目标是拓展应用领域以及开源系统的建设.目前, L2C编译器进入了第3个里程碑的发展阶段, 其目标是在目前面向企业的版本 (不开源) 基础上裁减并适当改造, 形成了覆盖Lustre V6^[19]全部特性的可开源版本.目前, 这一L2C编译器的单时钟版本 (L2C-MC) 已经开放源码 (https://github.com/l2ctsinghua/l2c/releases/tag/version-0.8), 支持嵌套时钟的版本处于测试与完善的周期, 其源码不久也将开放.

2、源语言的特性

L2C编译器的不同版本, 其源语言 (Lustre*) 可能有所不同, 本文以目前支持的最多特性为准.Lustre*覆盖了Lustre V6的全部特性, 并且根据实际应用的需求在此基础上有许多扩展, 特别是在高阶运算方面比Lustre V6更加丰富.

图1展示一个简单的Lustre程序, 可见, 一个Lustre程序 (program) 由多个节点 (node) 组成, 节点中包含输入参数 (parameters)、输出参数 (returns) 和函数体 (body), 其中函数体又由局部变量 (local variables) 和等式 (或语句) 序列组成, 结构清晰.

下面以图1示的Lustre程序为例来阐述Lustre的某些重要语言特性, 并且在图2中给出图1中主节点Main的一组合理输入与输出来直观展示Lustre*语言的这些特性.

(1) 流数据对象.图 2展示的输入输出很直观地体现了Lustre程序区别于C语言程序的一个很重要的特性, 即在Lustre中每一个变量都是一个无穷长的流 (stream) 数据对象, 而不仅仅是一个单个的值.每一个周期 (cycle), 变量都可能会有不同的值或者没有值, 其中图 2截取了输入输出前10个周期的值, 后面还有无穷个周期.虽然每个周期的值可能会变化, 但处理逻辑每个周期都一样, 如图 1所示的主节点Main的代码逻辑, 每个周期都一样.Lustre*是同步语言的一种, 所有同步语言均满足同步假设:当前周期的输入时间出现时, 系统能够在下个周期的输入时间出现之间计算出当前周期的输出.这一重要的同步假设使得同步语言在嵌入式实时控制系统中得到大规模应用.

(2) 数据流并发性.不同于C程序, Lustre程序具有数据流并发性, Lustre节点中的等式 (相当于语句) 虽然在书写时有先后顺序, 但都是并发执行的.更复杂的情况是, Lustre程序中的等式 (或语句) 之间存在因果关系, 所以在并发执行时还需要考虑等式 (或语句) 间的拓扑关系.如图 1中第7行~第8行所示, 这两行就存在因果关系.第7行k*的赋值依赖于第8行执行的结果, 所以第7行应该在第8行之后执行.这里拓扑关系的具体含义可参见第4节.

(3) 高阶算子.Lustre支持如map, re等10多个高阶算子, 这些高阶算子可以很方便地操作数组对象, 在编写程序时会更加便利.如图 1中第10行所示的map算子, 以节点 (或称函数) Max以及两个数组x1和x2作为参数, 返回另一个数组p*.语义上, 相当于并行执行“p[i]=Max (x1[i], x2[i])”(i从0变到1).

(4) 时态与时钟算子.由于Lustre的流数据对象特性, 语言提供了时态算子, 比如pre, fby, arrow (→) 等, 可以对流数据进行操作.另外, Lustre还支持嵌套的时钟, 提供了可改变时钟快慢的算子, 如when使时钟变慢形成下一层嵌套的时钟, 而current与merge使时钟变快, 回到上一层嵌套时钟.如图 2所示, 使用when算子后, 主节点中y1的时钟相对于x3的时钟变慢了 (根据布尔量b取值为true时进行采样); 使用了fby算子之后, 主节点中s相对于y1时钟周期不变, 但每个周期的值向后shift了1个周期 (注意, 这里指相对于y1时钟的shift, 即对应于b取值为true时的时钟周期).

3、L2C编译器的主体翻译框架

随着源语言 (Lustre*) 特性的增加以及不同开发阶段的不同理念, L2C可信编译器的翻译框架也在不断变化, 先后出现过接近10个稳定的框架图, 图 3是其中最近的一个.国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍

如图 3所示, Lustre源程序经过词法、语法以及静态语义分析 (类型检查), 翻译到类型良好的抽象语法树 (abstract syntax tree, 简称AST) 形式的高级中间语言Well-typed Lustre AST代码. Well-typed Lustre* AST代码经过一些简单的预处理变换 (LustreSGen) 生成一种具有规范形式的中间语言LustreS代码.预处理变换主要包括全局常量和类型的合并、拆分表达式列表、通过引入新变量提升某些特殊表达式 (如call和fby表达式) 至等式 (或语句) 级别等.

对于这部分的翻译过程, 目前我们没有去进行形式化验证, 故在图 3中用虚线箭头来表示.词法和语法分析算法或者相关的工具是比较成熟的, 比较可信, 但若要验证它们的正确性却是很困难的, 因此目前的可信编译器 (包括CompCert) 基本上不验证这一部分工作.此外, 其余的翻译工作 (包括类型检查) 相对比较简单, 也比较容易验证, 同时也因为它们是受Lustre*变化影响较大的部分, 所以我们在整个L2C可信编译器的实现中将这部分验证工作放在了最低的优先级.另外, 这些翻译过程的翻译确认程序是比较容易实现的, 这也是我们不急于完成这部分验证工作的重要原因之一.

高性能嵌入式仿真软件SkyEye

随着科技的发展，系统工程的设计体量逐渐庞大起来，尤其是对于轨道交通、航空航天、核电站等安全关键领域中，如何在复杂度逐年变大的同时保证其安全性和可靠性，是近年来各大公司需要研究的课题。最近比较火热的基于模型的系统工程（MBSE）技术则给大家提供了一种全新的技术方向，分享一种全数字实时仿真的安全关键领域解决方案，提供一种新的解决思路。国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍，提供高效的运算速度，提高研发效率和安全性。

新一代全数字仿真平台SkyEye

基于模型的全数字研发解决方案MBSE工具软件SkyEye是能够满足模拟或仿真外部硬件行为进行软件运行和测试需求的工具。该工具运用国际流行的仿真、测试脚本语言来编写外部硬件逻辑行为所产生外部激励事件以构成嵌入式软件的外部信号激励或数据输入，从而满足软件在全数字仿真运行环境下无须人的干预而闭环运行的要求。国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍

作为基于嵌入式应用的特点，嵌入式软件全数字仿真测试支撑平台SkyEye要为嵌入式系统提供全数字仿真测试环境或测试平台，实现对嵌入式系统进行实时、闭环的系统测试。在该平台上完成被测软件的分析、运行和测试，最重要的是要实现嵌入式系统外部事件的全数字仿真平台，使得嵌入式软件就像在真实硬件环境下连续不中断地运行。

本文标题：国产主可控的嵌入式仿真测试软件SkyEye与可信编译器L2C的核心翻译介绍

本文链接：http://www.digiproto.com