L2C中Lustre语义的环境定义

随着计算机技术越来越多地应用于航空航天、核电、高速铁路等安全关键系统(SCS，Safety-Critical System)，对计算机技术的安全性要求也越来越高。安全关键系统中的丝毫错误都可能引发巨大的灾难。如何为安全关键系统构造一个基础的安全软件环境是需要面对的首要问题，尤其是对操作系统、编译器等基础软件。

Lustre是一种同步数据流语言，主要用于航空航天、核电等高可信要求的程序设计领域。由我司自主开发的ModelCoder是一款支持同步数据语言Lustre以及状态机等嵌入式模型并可以自动生成高安全可靠的C代码的软件设计和开发工具。L2c作为ModelCoder的核心代码生成器，其从模型生成代码的过程经过了形式化验证，以保证生成过程的正确无误性。使得ModelCoder能够用于飞机的飞控，飞机的航电，核电的DCS等多个安全关键领域的嵌入式软件的设计和开发。L2C利用交互式定理证明器COQ开发，通过分层翻译的方式完成Lustre到C的翻译，并定义Lustre到C相关层的形式化语义，证明翻译前的源语言Lustre在其语义下和翻译后的目标语言C在其语义下执行等价。

因为Lustre语义与C的语义差异很大，所以证明的难点就在于如何定义Lustre语义，而Lustre语义定义的难点又在于其语义环境的定义。Lustre 程序的的特点决定了Lustre不能简单使用C类似的环境定义。Lustre 的时态运算需要保留历史环境；Lustre 翻译过程中会对多种变量进行分类要求不同类型变量的环境要有一定的隔离性；节点调用的证明是每层证明的重点，要求环境在一定程度上要反应节点调用的调用关系；Lustre 程序执行过程中对类型的限制十分严格，这要求环境在存储值的同时也要保存变量类型。

L2C介绍

L2C是一款能够将状态机模型和同步数据流语言Lustre翻译成C语言的可信编译器，其利用交互式定理证明器COQ开发，通过分层翻译的方式完成Lustre到C的翻译，并定义Lustre到C相关层的形式化语义，证明翻译前的支持状态机模型的源语言Lustre在其语义下和翻译后的目标语言C在其语义下执行等价。通过语义保持的方式实现翻译过程的形式化验证，使得L2c的验证过程更加完备可信程度更高。而语义定义是进行语义保持验证的核心，而环境定义又是语义定义的基础，下面就介绍一下L2c中Lustre语义的环境定义。

1.Lustre环境中基本内存单元的定义

在Lustre的内存模型中，使用Compcert的memval作为内存存储的基本单元。这样Lustre和C的共用相同的基本内存单元，这样能够简化语义保持的等价性证明。当Lustre变量刚分配时，每个相关的memval的值都是未定义的Undef状态；当变量赋值后，其相关的memval的值是有值的Byte状态。Fragment状态不在Lustre环境中使用。

Inductive memval: Type :=

  | Undef: memval

  | Byte: byte -> memval

  | Fragment: val -> quantity -> nat -> memval.

2.Lustre环境中内存值的基本存储空间

在Lustre的内存模型中，以mvl作为内存值的基本存储空间。mvl是memval的列表，每个mvl对应一个变量的存储空间，mvl的长度对应变量类型的大小。

Definition mvl := list memval.

当Lustre变量刚分配时，为其分配其类型大小对应长度的Undef列表

Definition alloc(size: Z) :=

  list_repeat (Z.to_nat size) Undef.

3.Lustre值的定义

Lustre值的定义分为整形值、浮点值、单精度浮点值和mvl值，其中mvl值为数组和结构体的值。C中的数组和结构体的值是通过指针来定义的，指向内存中对应的地址块中对应的偏移位置。而Lustre语义中没有指针的概念，所以用mvl来对应C内存中对应长度的基本内存单元。在证明中进行数组和结构体值的比较时，如果某一个数组结构体变量在Lustre环境中的值为：Vmvl mv，其在C的环境中的值为：Vptr b ofs，在C的内存m中取地址块b中偏移ofs的对应长度的内存片段为mv，即可证明该数组结构体变量在Lustre和C的环境中等价。

Inductive val: Type :=

  | Vint: int -> val

  | Vfloat: float -> val

  | Vsingle: float32 -> val

  | Vmvl: mvl -> val.

4.Lustre局部环境的存储空间

Lustre局部环境的存储空间定义为locenv。locenv是一个树形存储空间，通过变量id作为存储的索引值，存储每个变量对应的mvl值及其类型。mvl的长度和类型的大小相等。locenv即可单独作为节点内的局部环境的存储空间，也可作为Lustre需要保存的历史值的环境树的叶子节点，还可以作为Lustre全局常量的存储空间。

Definition locenv:= PTree.t (mvl*type).

5.Lustre环境树定义

Lustre节点的局部变量在每个周期结束后都不再保存，Lustre节点的返回值、时钟标志变量、时态运算自定义变量和子节点的调用实例需要保存其历史值，节点的返回值、时钟标志变量和时态运算自定义变量的存储环境le通过locenv来保存。节点内的子节点调用实例的存储环境sube是一个环境子树，通过实例名来索引；每个实例环境对应为环境子树中的一个子环境列表：list env。普通子节点调用的实例环境为长度为1的子环境列表。高阶子节点调用的实例环境为长度为高阶迭代次数的子环境列表，高阶调用的每次迭代对应子环境列表中对应位置的子环境。

Inductive env: Type := mkenv {

  le: locenv; 

  sube: PTree.t (list env)

}.

Lustre中节点对应的保存历史值的环境树对应于C中节点的输出结构体。节点的返回值、时钟标志变量和时态运算自定义变量将存储于节点输出结构体中，子节点的调用实例对应输出结构体中的子结构体，每个子结构体又与调用实例对应的子节点相对应。最终证明Lustre环境树中的各级变量和输出结构体中对应的子元素的值相等，Lustre环境树中实例环境子树和输出结构体中的对应子结构体匹配。

环境定义的难点就在于在项目的起初就预见到 Lustre对环境的诸多要求，所以最初定义的环境会较难满足证明的需求。所以环境定义在证明过程中不断的被修改，而环境定义又是证明的基础，所以导致证明的过程也反复地被修改。每次环境的修改在简化证明的同时，也势必造成整个语义定义和证明过程的大范围地修改。