软件学报

作者：李少峰，乔磊，杨孟飞，张锦坤，马智，刘洪标

单位：李少峰，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007111,乔磊，北京控制工程研究所, 北京 10019002,杨孟飞，中国空间技术研究院, 北京 10009403,张锦坤，北京控制工程研究所, 北京 10019004,马智，北京控制工程研究所, 北京 10019005,刘洪标，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007106

关键词：程序设计;内存管理;形式化验证;精化验证;嵌入式系统

基金：国家自然科学基金(61632005,62032004,61802017);中国科学院软件研究所计算机科学国家重点实验室开放课题基金(SYSKF1804)

安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

来源：2022年第6期

《软件学报》期刊编辑部

查看软件学报杂志2022年第6期