L2C介绍

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

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

3.Lustre值的定义

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

5.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对环境的诸多要求，所以最初定义的环境会较难满足证明的需求。所以环境定义在证明过程中不断的被修改，而环境定义又是证明的基础，所以导致证明的过程也反复地被修改。每次环境的修改在简化证明的同时，也势必造成整个语义定义和证明过程的大范围地修改。

L2C中Lustre语义的环境定义相关推荐

L2C中CtempGen层语义保持证明中环境匹配的定义
ModelCoder是一款由迪捷软件自主研发,支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具.ModelCoder支持同步数据流以及状态机等嵌入式模型,其从模型生成代码的过 ...
TensorFlow中的语义分割套件
TensorFlow中的语义分割套件描述该存储库用作语义细分套件.目标是轻松实现,训练和测试新的语义细分模型!完成以下内容: 训练和测试方式资料扩充几种最先进的模型.轻松随插即用能够使用任何 ...
anaconda新建python2环境安装不了jupyterlab_Anaconda 5.0.0 JupyterLab 0.27.0 中配置多Python环境支持...
Anaconda 5.0.0 JupyterLab 0.27.0 中配置多Python环境支持概述 Anaconda 5.0.0 中自带了 JupyterLab 0.27.0 版本,这是 Anaco ...
在Visual Studio Code中配置GO开发环境
一.GO语言安装详情查看:GO语言下载.安装.配置二.GoLang插件介绍对于Visual Studio Code开发工具,有一款优秀的GoLang插件,它的主页为:https://github ...
了解React Native中的不同JavaScript环境
by Khoa Pham 通过Khoa Pham 了解React Native中的不同JavaScript环境 (Get to know different JavaScript environmen ...
oracle的env函数用法,env命令_Linux env 命令用法详解：显示系统中已存在的环境变量...
env命令用于显示系统中已存在的环境变量,以及在定义的环境中执行指令.该命令只使用"-"作为参数选项时,隐藏了选项"-i"的功能.若没有设置任何选项和参数时,则 ...
eclipse中SSH三大框架环境搭建二
通过上一篇博客我们可以轻松搭建strtus2的环境,接下来由我来继续介绍spring的环境搭建以及spring注入的简单使用相关链接:eclipse中SSH三大k框架环境搭建<一> ec ...
python关键字define_在Python中，使用关键字define定义函数。
在Python中,使用关键字define定义函数. 以下属于生药学有效性评价的是A:有效成分定量分析B:限量检查C:重金属检测D:基原鉴定若有如下定义和语句:A:7B:12C:8D:9 图示电路中的 ...
atom配置python_在Atom中设置Python开发环境
在使用Python开发环境中,很多人比较喜欢使用Atom.在Atom中,有很多编辑工具,包括文字,方括号,原子.Atom是完全免费的,并且它具有许多可用的程序包和主题,从而使编码变得更加容易.在这里, ...

L2C中Lustre语义的环境定义

L2C介绍

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

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

3.Lustre值的定义

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

5.Lustre环境树定义

L2C中Lustre语义的环境定义相关推荐

最新文章

热门文章