声明
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。
国内刊号：11-2560/TP
国际刊号：1000-9825
发布日期:
作者：康跃馨,甘元科,王生原
单位：康跃馨，清华大学 计算机科学与技术系, 北京 10008411,甘元科，清华大学 计算机科学与技术系, 北京 10008402,王生原，清华大学 计算机科学与技术系, 北京 10008403
关键词：同步数据流语言;形式化验证的编译器;Lustre语言
基金：国家科技重大专项（MJ-2015-D-066）
同步数据流语言（如Lustre、Signal）在航空、高铁、核电等安全关键领域得到广泛应用.例如，适合这些领域实时控制系统建模和开发的Scade工具就是基于一种类Lustre语言.这类语言相关开发工具，特别是编译器的安全性问题也自然受到高度关注.近年来，基于形式化验证实现可信编译器构造成为程序设计语言领域的研究焦点之一，也取得了瞩目的成果，如CompCert项目实现了产品级的可信C编译器.同样，人们也采用这种方法开展了同步数据流语言可信编译器的研发工作.主要关注从事这一工作的两个长线项目，二者均研发面向基于Lustre的同步数据流语言编译器，分别以Vélus和L2C代称.对Vélus和L2C从多个重要的角度进行较为深入的分析与比较.
来源：2019年第7期
《软件学报》期刊编辑部
严正声明：本站非期刊官网，非中介代理。
本站仅提供学术规范服务：快速预审、润色编辑服务、中英文查重、降重、去重服务、推荐合适的期刊投稿等学术规范服务。 如需提供学术规范服务请联系在线编辑。