典型文献
多旋翼飞控推进子系统的Coq形式化验证
文献摘要：
飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.
文献关键词：
形式化验证;定理证明;多旋翼飞行器;飞行控制系统;推进系统;Coq;OCaml
中图分类号：
作者姓名：
石正璞;崔敏;谢果君;陈钢
作者机构：
南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106
文献出处：
引用格式：
[1]石正璞;崔敏;谢果君;陈钢-.多旋翼飞控推进子系统的Coq形式化验证)[J].软件学报,2022(06):2150-2171
A类：
Coq,OCaml
B类：
形式化验证,高可靠,飞行控制系统,系统软件,开发模式,将领,领域知识,自然语言,语言形式,代码,软件测试技术,出错,二义性,完备性,形式验证,验证技术,软件开发方法,高飞,飞控系统,定理证明,明器,全权,软件库,知识整理,层次结构,文档,基本函数,复合函数,函数概念,形式化描述,常量,公理,导正,立为,引理,悬停,求解算法,多子,多旋翼飞行器,推进系统
AB值：
0.359336
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
