摘要
国产龙芯处理器在国产信息化的道路上发挥着重要作用,其性能的发挥需要系统核心软件的全力配合。作为系统核心软件之一的编译器的重要性已提升至信息产业前列,是确保安全关键系统能否正常运行的关键。以国防科工委公布的航天型号C语言安全子集作为安全检测技术的标准,构造符合规范的测试用例,通过形式化验证技术对LonGcc编译器进行改造、升级。最后实测表明,所构造的编译器符合C语言安全子集标准,并且没有增加执行时的开销。
The domestic made Godson processor has played an important role in domestic informatization by giving full play to its property with the support of the core software system.As one of the core software system,the importance of the compiler has been raised to the forefront of the information industry and it is regarded as the key to ensure normal operation of safety critical systems.Taken the space type C safe subset published by COSTIND as a standard of safety inspection technology,test cases conforming to the specification are constructed and LonGcc compiler is modified and upgraded by formal verification techniques.The final measured results show that the constructed compiler is in accordance with C language subset safety standards and does not increase the overhead at execution time.
作者
赖策
李明东
刘茜
李艳梅
LAI Ce;LI Mingdong;LIU Xi;LI Yanmei(College of Computer, China West Normal University,Nanchong Sichuan 637009,China)
出处
《西华师范大学学报(自然科学版)》
2017年第4期462-466,共5页
Journal of China West Normal University(Natural Sciences)
基金
西华师范大学创新团队项目(CXTD2014-11)