同步语言Lustre的编译前端的设计与实现

同步语言Lustre所描述的反应系统通常应用在航空航天、国防建设等领域,对系统的正确性和安全性都要求很高。如果系统在运行时出现了正确性问题,很可能会导致系统崩溃,产生非常严重的后果。系统中的任何一个词法错误或者语法错误都应该受到重视,而且应该被及时纠正。因此,对Lustre语言进行正确的编译是十分重要的。传统的Lustre语言的编译器都采用OCaml语言描述,无法保证所有人员都能够很容易地理解和使用,而且,需要耗费开发人员大量的时间和精力。基于上述问题,提出了一种新型的Lustre语言编译器。新型的Lustre语言编译器前端主要采用C++语言进行描述,并对生成的抽象语法树的结构进行重新定义,简化了编译的过程。该编译前端会对一个经典的Lustre语言模型进行检测,通过对检测的结果进行分析,验证了该编译前端的可行性。

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

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

在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程

Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。

用模块模型检查的方法来证明进程的正则网络的若干经验

提供了一个使用同步描述性语言ＬＵＳＴＲＥ的例子，这个例子是关于使用此语言来描述，说明和验证一个资源协调器（这是一种正则的网络硬件设备）程序及性质都可以用ＬＵＳＴＲＥ来表达的事实可以被用来作归纳验证，验证可通过模型检查来进行。