可信编译器L2C的核心翻译步骤及其设计与实现

同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好”误编译”问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证取得了很大的成功,如CompCert C编译器.L2C是基于这种方法开发的可信编译器,它以扩展的Lustre语言为源语言,以Clight （CompCert中的C语言子集）为目标语言.就我们所知,L2C是同类工作中唯一面向实际工业应用的同步数据流语言编译器.本文重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.     

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.     

同步数据流语言高阶运算消去的可信翻译

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.     

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler.     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

一种包解析器硬件配置描述语言及其编译结构

设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.     

同步数据流语言可信编译器Vélus与L2C的比较

同步数据流语言（如Lustre、Signal）在航空、高铁、核电等安全关键领域得到广泛应用.例如,适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言.这类语言相关开发工具,特别是编译器的安全性问题也自然受到高度关注.近年来,基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一,也取得了瞩目的成果,如CompCert项目实现了产品级的可信C编译器.同样,人们也采用这种方法开展了同步数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目,二者均研发面向基于Lustre的同步数据流语言编译器,分别以Vélus和L2C代称.对Vélus和L2C从多个重要的角度进行较为深入的分析与比较.     

Use of a formal notation for static semantics in compiler design

Formal notations for the specification of the syntax and the dynamic semantics of languages exist and are of great benefit to the compiler writer. However, formal notations for the static semantics of languages have tended to be tools of the language designer and of little practical significance to the compiler writer. This paper describes how a particular notation was used to assist in the implementation of a Cobol compiler and of an interpreter for a simulation language.     

A Formally Verified Compiler Back-end

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.     

Modeling multi-rate DSP specification semantics for formal transformational design in HOL

The CATHEDRAL Silicon Compilers synthesize hardware for DSP algorithms specified in Silage, a high level applicative language. In order to optimize the results of the silicon compilation in terms of chip-area and/or throughput, the user often massages the specification applying transformations to the Silage code. To guarantee that the transformations preserve the behavior of the specified algorithm, the formal semantics of the specification language had to be defined. The semantics has been used to prove in HOL the correctness of the transformations and to prove properties of the specification. We are currently building a system where a menu of useful andcorrectness preserving transformations will be available to the user. In this system the user could choose appropriate transformations from the menu taking advantage of his creativity and expertise to interactively guide the silicon compiler, without the risk of introducing inconsistencies. This article describes the formalmulti-rate semantics of a substantial subset of Silage and illustrates some formally verified transformations.     

Integrating discrete controller synthesis into a reactive programming language compiler

We define a mixed imperative/declarative programming language: declarative contracts are enforced upon imperatively described behaviors. This paper describes the semantics of the language, making use of the notion of Discrete Controller Synthesis (DCS). We target the application domain of adaptive and reconfigurable systems: our language can serve programming closed-loop adaptation controllers, enabling flexible execution of functionalities w.r.t. changing resource and environment conditions. DCS is integrated into a1 programming language compiler, which facilitates its use by users and programmers, performing executable code generation. The tool is concretely built upon the basis of a reactive programming language compiler, where the nodes describe behaviors that can be modeled in terms of transition systems. Our compiler integrates this with a DCS tool, making it a new environment for formal methods. We define the trace semantics of our contracts language, describe its compilation and establish its correctness, and discuss implementation and examples.     

基于Clight形式语义的代码功能描述提取

软件代码的功能提取是功能集成的最基本前提,但软件功能提取普遍存在正确率低的问题。为此,提出基于Clight形式语义的代码功能描述提取机制,并用Clight代码功能描述算法实现。该机制严格基于Clight自然语义推理规则,忽略代码执行的中间细节,只关注执行前后的存储状态,并以此作为代码的功能描述,提高了功能提取的正确率和关键领域软件开发的成功率。     

Testing syntax and semantic coverage of Java language compilers

Software testing is a critical and important stage of the application software development life-cycle. Testing is a verification activity that affects the overall software quality. The verification of critical and dependable computer software such as real-time safety-critical software systems consumes about 50% of the project time. In this work, we consider testing compilers. Since a compiler is a highly usable software, an increased emphasis on reliability requires a careful testing before releasing the compiler. In compiler testing, the compiler implementation is verified to conform to the specified language syntax and semantic available in the standard language documentation. In this work, an algorithm is designed and a tool is developed to automate the generation of test cases to check the language syntax. In addition, we propose a heuristic approach to cover language semantics. Since Java is a relatively new programming language, we concentrate on testing the adherence of new Java compilers to the language syntax and semantics.     

Deriving a compiler from an operational semantics written in VDL

This paper addresses the issue of compiler correctness. The approach taken is to systematically construct a correct compiler for a language from a formal semantic definition of the language. For this purpose, an operational semantics of a language is chosen as the basis for the approach. That is, the compiler for a language is derived from an interpreter of the language. The derivation process uses the notion of mixed computation proposed by Ershov. Briefly stated, one begins interpreting and when a primitive state changing instruction is about to be executed, the instruction is emitted as code instead. The correctness of all compilers produced by the method is guaranteed by proving the derivation rules correct. This proof is a one-time task for each specification language. The specification language studied in this paper is the Vienna Definition Language (VDL). The object code generated by the compiler is in an intermediate language close to an assembly language. Therefore, the translation from the intermediate language into the assembly language should be straightforward.     

Action semantics-directed prototyping

We present a methodology for compiler synthesis based on Mosses-Watt's action semantics. Each action in action semantics notation is assigned specific “analysis functions”, such as a typing function and a binding-time function. When a language is given an action semantics, the typing and binding-time functions for the individual actions compose into typing and binding-time analyses for the language; these are implemented as the type checker and static semantics processor, respectively, in the synthesized compiler. Other analyses can be similarly formalized and implemented. We show a sample language semantics and its synthesized compiler, and we describe the compiler synthesizer that we have developed.     

An optimizing compiler for the icon programming language

Compiling code for the Icon programming language presents several challenges, particularly in dealing with types and goal-directed expression evaluation. In order to produce optimized code, it is necessary for the compiler to know much more about operations than is necessary for the compilation of most programming languages. This paper describes the organization of the Icon compiler and the way it acquires and maintains information about operations. The Icon compiler generates C code, which makes it portable to a wide variety of platforms and also allows the use of existing C compilers for performing routine optimizations on the final code. A specially designed implementation language, which is a superset of C, is used for writing Icon's run-time system. This language allows the inclusion of information about the abstract semantics of Icon operations and their type-checking and conversion requirements. A translator converts code written in the run-time language to C code to provide an object library for linking with the code produced by the Icon compiler. The translation process also automatically produces a database that contains the information the Icon compiler needs to generate and optimize code. This approach allows easy extension of Icon's computational repertoire, alternate computational extensions, and cross compilation.     

UML类图的形式化及分析

统一建模语言(UML)是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为事实上的工业标准。但是UML不是形式化的建模语言,缺乏精确的语义描述,因此会导致一些问题。Z是一种广泛使用的形式化规约语言,Z适合用来精确地表示模型的语法和语义。文章采用Z符号来表示UML类图的组成元素的语法和语义及其映射关系,最后对UML类图的一些性质进行分析和验证。