针对安全关键系统的多语言编程形式化验证

项目名称： 针对安全关键系统的多语言编程形式化验证

项目编号： No.61170051

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 自动化技术、计算机技术

项目作者： 董渊

作者单位： 清华大学

项目金额： 15万元

中文摘要： 航空等领域中对安全关键软件的形式化验证有着迫切的需求，尤其关注存储安全性和正确性等特性。现实中的安全关键软件通常都采用多种语言共同实现，多语言编程使用非常普遍，而多语言接口部分常常是错误高发地带，而且也是目前研究的薄弱环节。为此，本项目以安全关键软件系统的完整形式化验证为远期目标，着重研究C语言与汇编语言这种具有代表性的多语言编程接口的形式化建模，以此为基础探索多语言编程的验证方法，并以广泛应用的开源嵌入实时操作系统为目标，开展原型系统验证研究。本项目将给出一种考虑多语言编程特征的程序建模和验证方法，解决其关键问题，为安全关键软件的构造提供技术支持。

中文关键词： 安全关键软件；形式化验证；多语言编程；嵌入系统；

英文摘要：

英文关键词： Safety-Critical Software；Formal Verification；Multilingual Programming；Embedded System；