可信软件代码中程序标注的使用及类型验证  

Employment of Program Annotations in Trusted Code and Their Type Verification

作　　者：赵洋[1,2] 徐晓刚[2] 张功萱[1] 张容[1] 

机构地区：[1]南京理工大学计算机科学与技术学院,南京市孝陵卫200号210094 [2]南京大学计算机软件新技术国家重点实验室,南京市汉口路22号210093

出　　处：《武汉大学学报（信息科学版）》2010年第5期570-573,共4页Geomatics and Information Science of Wuhan University

基　　金：国家自然科学基金资助项目(60850002);高等学校博士学科点专项科研基金资助项目(20093219120026);南京理工大学科技发展基金资助项目(XKF09017)

摘　　要：程序标注技术能够勾勒程序代码中的各种数据属性和软件行为,提出了使用许可类型系统作为沟通程序标注和程序代码的桥梁,从程序代码的角度分析和验证了程序的安全性,进而提升了整个软件系统的可靠性和可维护性。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.

关 键 词：可信代码 程序标注 程序验证 

分 类 号：TP311.53[自动化与计算机技术—计算机软件与理论]