同步数据流语言高阶运算消去的可信翻译
同步数据流语言(例如Lustre,Signal等)广泛应用于工业界的核心安全级控制系统,如航空、核电等高安全等级的关键领域,与语言相关的软件的安全性也越来越受到人们的关注,特别是一些基础软件,如操作系统、编译器等.确认这些软件的安全可靠非常重要,同时,随着软件系统的复杂度的提高,软件的安全性保证也变得越来越困难,依靠传统的测试、代码审核和过程管控等方法来保证软件的安全性是远远不够的.近年来,形式化验证方法已成功地应用于可信编译器的实现中,CompCert是其中的杰出代表.形式化验证方法从数学角度对软件系统进行描述,从逻辑上对软件系统的正确运行进行验证,能够充分地保证软件系统可信,可以最大程度地提高软件系统的可信度.国产自主可控的嵌入式仿真软件SkyEye和同步数据流语言高阶运算消去的可信翻译
我们项目组基于形式化验证方法开展了一项从Lustre*语言到C子集Clight的可信翻译器的研究工作,称为L2C项目，图 1是该项目的整体框架.
Lustre是一种类Lustre语言,它是以Lustre V6的核心语言为基础,并加上一些类似于Scade的扩展. Lustre语言中除了通常的算术和逻辑表达式之外,还包含了struct,list,switch和array等表达式,这些表达式的执行规则类似于C语言中的相应表达式.此外,Lustre*从Scade中继承了一些高阶运算和对于数组和结构体的操作.Clight来源于CompCert项目,是一种兼容于关键嵌入式软件推荐使用的较大的C语言子集.
L2C项目的开发采用辅助证明工具Coq实现,集程序、性质和证明于一体,最终代码被抽取为Ocaml代码,与前端的Ocaml代码集成,得到完整编译过程的代码.通过图 1的最后一步,Lustre*源程序最终被翻译到CompCert项目的Clight AST,Clight语言的语法语义采用CompCert的定义.
同步数据流语言Lustre与Clight相比有着巨大的差异,Lustre具有时钟同步、数据流、并发及流数据对象等特征,而Clight则具有顺序控制流特征,语言跨度较大.直接进行翻译及证明将会非常复杂,因此,我们将项目分为多个层次,保证每个层次语法和语义跨度不大,每个层次完成特定的工作,比如时钟归一化、拓扑排序、时态算子消除等工作.& lt; span style=‘font-family:宋体;color:black’>本文的研究工作高阶消去翻译及正确性证明,包含于如图 1所示的LustreT到LustreR层的Reducing过程中.
高性能嵌入式仿真软件SkyEye
随着科技的发展，系统工程的设计体量逐渐庞大起来，尤其是对于轨道交通、航空航天、核电站等安全关键领域中，如何在复杂度逐年变大的同时保证其安全性和可靠性，是近年来各大公司需要研究的课题。最近比较火热的基于模型的系统工程（MBSE）技术则给大家提供了一种全新的技术方向，分享一种全数字实时仿真的安全关键领域解决方案，提供一种新的解决思路。国产自主可控的嵌入式仿真软件SkyEye和同步数据流语言高阶运算消去的可信翻译，提供高效的运算速度，提高研发效率和安全性。
新一代全数字仿真平台SkyEye
基于模型的全数字研发解决方案MBSE工具软件SkyEye是能够满足模拟或仿真外部硬件行为进行软件运行和测试需求的工具。该工具运用国际流行的仿真、测试脚本语言来编写外部硬件逻辑行为所产生外部激励事件以构成嵌入式软件的外部信号激励或数据输入，从而满足软件在全数字仿真运行环境下无须人的干预而闭环运行的要求。
作为基于嵌入式应用的特点，嵌入式软件全数字仿真测试支撑平台SkyEye要为嵌入式系统提供全数字仿真测试环境或测试平台，实现对嵌入式系统进行实时、闭环的系统测试。在该平台上完成被测软件的分析、运行和测试，最重要的是要实现嵌入式系统外部事件的全数字仿真平台，使得嵌入式软件就像在真实硬件环境下连续不中断地运行。国产自主可控的嵌入式仿真软件SkyEye和同步数据流语言高阶运算消去的可信翻译
SkyEye的优势
作为一种全数字实时仿真的安全关键领域解决方案，SkyEye可与第三方语言或者模型集成，目前已实现SkyEye与SystemC集成进行时序仿真，以及SkyEye与工业软件MATLAB或者Simulink集成进行多领域协同仿真。
- 更灵活快速的虚拟目标系统搭建–通过可视化图形界面拖拽虚拟硬件组件快速搭建。
- 仿真状态可控性、确定性和重复性–在虚拟系统上运行的二进制文件与实际目标上运行的二进制文件相同，仿真过程可以通过运行、暂停控制、可以随时重复执行，每次运行结果是确定的，可以使用软件复现问题。
- 提供GDB源码调试和汇编级调试工具，使开发者更高效的分析和定位问题。
- 提供代码覆盖率和生成报告功能，进行源码和目标码的覆盖率分析。
- 提供故障注入功能，可以进行内存和IO的故障注入进行测试。
- 提供协同仿真工具，支持与其他异构模型协同仿真。
- 提供外设建模工具和二次开发API接口，方便用户进行二次开发。
- 提供Python API接口，可以进行自动化测试脚本构建所需测试环境。
- Docker容器化支持。
- 界面提供自动化测试功能，可以选择所需测试用例自动运行并给出测试结果与其他异构模型协同仿真。
本文标题：高性能嵌入式仿真软件SkyEye
本文链接：http://www.digiproto.com
