《表1 Velus、L2C和SCADE的特性比较》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《Lustre语言可信代码生成器研究进展》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

清华大学L2C项目组于2010年开始着手研究Lustre到Clight的可信代码生成器（简称L2C），经过形式化验证的L2C单时钟版本[29]已经实现了开源，在此基础上又为国内某核电企业开发了多时钟版本[30]。Velus和L2C都是参考了CompCert成功的技术路线，在Coq中利用定理证明技术来进行形式化的开发。它们的目标语言Clight的形式化定义也都是借鉴CompCert的定义。因此，L2C（开源版本）的架构跟Velus非常相似，这里不再赘述。但它们还是存在许多的不同，主要体现在支持的Lustre语言特性上。为了结合实际工业控制领域的需要，L2C、SCADE等工具在前述的Lustre语言特性的基础上，为了满足工业控制的需要，又增加了一些如用于处理数组的高阶算子等特性。如表1所示，为Velus、L2C（开源版本）和SCADE特性上的比较。