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

摘要：l2c信号是由现代化GPS IIR-M卫星播发的新一代民用信号。基于软件接收机的信号采集与数据处理的研究旨在提高信号在低信噪比环境下的捕获稳定性和跟踪精度。l2c信号结构描述了其民用中码和民用长码的时分复用特征。信号采集部分包括宽频天线和接收机前端的设计,工作频段为l1-l2频段,前端采用下变频和频谱搬移来避免频谱混叠。数据处理中采用降频处理的方法能有效增强信号捕获的稳定性,并利用圆周相关算法获得cM码的初始相位。码和载波跟踪数据处理包含计算原理的介绍和跟踪环结构设计。最后,通过低信噪比环境下的实验来验证l2c信号采集与数据处理方法的有效性。