CoqMatrix: Formal matrix library with multiple models in Coq

Date:Oct, 2023

Author: Zhengpu Shi, Guojun Xie, Gang Chen

Type Journal Article (CCF-B Journal)

Journal: Journal of Systems Architecture DOI: doi.org/10.1016/j.sysarc.2023.102986 Paper URL: online paper

Keywords: Coq theorem prover, Formal matrix theory, Unified matrix interface, Matrix models comparison, Isomorphic mapping, Formal vector theory, Unified vector interface

Abstract: Matrices are common tools in mathematics and computer science, and matrix formalization in proof assistants can provide strong support for verifying system behaviors related to matrix operations. The Coq community has proposed at least five formal matrix models, although the Coq standard library does not implement them. Developers who require a formal matrix library could have difficulty choosing what model to use. More importantly, once a choice is made, switching to another model later can be expensive. Although these matrix models have formalized matrix theory to a certain scale, demonstrating the ability to support the development of matrix theory, they have not identified the absolute advantages over other models, making it difficult for developers to choose. Moreover, the models have different data structures with completely different signatures of function and theorem, forcing developers to virtually completely rewrite matrix-related scripts when switching to a new matrix model. To address these problems, herein we undertake the following. First, we propose a unified matrix interface and integrate existing formal matrix models in the Coq community based on this interface. Secondly, we construct bijective functions between the different models to form isomorphisms, thus establishing connections between these models. We also provide technical comparison conclusions to help developers make choices. Hence, matrix formalization developers have a reference guide in the early stage and can switch to other models at a low cost at a later stage or use multiple models simultaneously with conversion assistance.

Cite format: Zhengpu Shi, Guojun Xie, and Gang Chen. CoqMatrix: Formal matrix library with multiple models in Coq[J]. Journal of Systems Architecture, 2023, 143: 102986. https://doi.org/10.1016/j.sysarc.2023.102986

Bib file: .BIB

Integration of Multiple Formal Matrix Models in Coq

Date:Dec, 2022

Author: Zhengpu Shi & Gang Chen

Type Conference proceedings (CCF-C Conference)

Conference: SETTA 2022 DOI: 10.1007/978-3-031-21213-0_11 Paper URL: online paper

Abstract: Matrices are common tools in mathematics and computer science, and matrix formalization in proof assistants can provide strong support for verifying system behaviors related to matrix operations. The Coq community has proposed at least five formal matrix models, although the Coq standard library does not implement them. Developers who require a formal matrix library could have difficulty choosing what model to use. More importantly, once a choice is made, switching to another model later can be expensive. Although these matrix models have formalized matrix theory to a certain scale, demonstrating the ability to support the development of matrix theory, they have not identified the absolute advantages over other models, making it difficult for developers to choose. Moreover, the models have different data structures with completely different signatures of function and theorem, forcing developers to virtually completely rewrite matrix-related scripts when switching to a new matrix model. To address these problems, herein we undertake the following. First, we propose a unified matrix interface and integrate existing formal matrix models in the Coq community based on this interface. Secondly, we construct bijective functions between the different models to form isomorphisms, thus establishing connections between these models. We also provide technical comparison conclusions to help developers make choices. Hence, matrix formalization developers have a reference guide in the early stage and can switch to other models at a low cost at a later stage or use multiple models simultaneously with conversion assistance.

Cite format: Zhengpu Shi, Gang Chen. (2022). Integration of Multiple Formal Matrix Models in Coq. In: Dong, W., Talpin, JP. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2022. Lecture Notes in Computer Science, vol 13649. Springer, Cham. https://doi.org/10.1007/978-3-031-21213-0_11

Bib file: .BIB

多旋翼飞控推进子系统的Coq形式化验证

Coq Formalization of Propulsion Subsystem of Flight Control System for Multicopter

Date:June, 2022

Author: 石正璞,崔敏,谢果君,陈钢

Type Journal Article (CCF-A类中文期刊)

Journal: Journal of Software (软件学报) DOI: 10.13328/j.cnki.jos.006575 Paper URL: online paper

Chinese keywords: 形式化验证;定理证明;多旋翼飞行器;飞行控制系统;推进系统;Coq;Ocaml

Chinese abstract: 飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.

Cite format: Zhengpu Shi, Min Cui, GuoJun Xie, Gang Chen. Coq Formalization of Propulsion Subsystem of Flight Control System for Multicopter. Journal of Software, 2022,33(6):2150-2171

Cite format(中文): 石正璞,崔敏,谢果君,陈钢.多旋翼飞控推进子系统的Coq形式化验证.软件学报,2022,33(6):2150-2171

Bib file: .BIB