| 可信软件代码中程序标注的使用及类型验证 |
| |
| 引用本文： | 赵洋,徐晓刚,张功萱,张容.可信软件代码中程序标注的使用及类型验证[J].武汉大学学报(信息科学版),2010(5). |
| |
| 作者姓名： | 赵洋 徐晓刚 张功萱 张容 |
| |
| 作者单位： | 南京理工大学计算机科学与技术学院;南京大学计算机软件新技术国家重点实验室; |
| |
| 基金项目： | 国家自然科学基金资助项目(60850002); 高等学校博士学科点专项科研基金资助项目(20093219120026); 南京理工大学科技发展基金资助项目(XKF09017) |
| |
| 摘 要： | 程序标注技术能够勾勒程序代码中的各种数据属性和软件行为,提出了使用许可类型系统作为沟通程序标注和程序代码的桥梁,从程序代码的角度分析和验证了程序的安全性,进而提升了整个软件系统的可靠性和可维护性。
|
| 关 键 词： | 可信代码 程序标注 程序验证 |
Employment of Program Annotations in Trusted Code and Their Type Verification |
| |
| ZHAO Yang, XU Xiaogang ZHANG Gongxuan ZHANG Rong.Employment of Program Annotations in Trusted Code and Their Type Verification[J].Geomatics and Information Science of Wuhan University,2010(5). |
| |
| Authors: | ZHAO Yang XU Xiaogang ZHANG Gongxuan ZHANG Rong |
| |
| Institution: | ZHAO Yang1,2 XU Xiaogang2 ZHANG Gongxuan1 ZHANG Rong1(1 School of Computer Science,Nanjing University of Science , Technology,200 Xiaolingwei,Nanjing 210094,China)(2 State Key Lab for Novel Software Technology,Nanjing University,22 Hankou Road,Nanjing 210093,China) |
| |
| Abstract: | We propose to use the permission system to act as a bridge connecting program annotations and program code.Within the permissions,we could verify the credibilities and safety properties of the program from the level of source code.Thus the reliability and maintainability of software systems could be improved. |
| |
| Keywords: | trusted code program annotations program verification |
| 本文献已被 CNKI 等数据库收录！ |
