Formal Modeling of Airborne Software High-Level Requirements Based on Knowledge Graph

摘要

Airborne airworthiness certification DO-178C software release proposes a higher safety and reliability demands of airborne software. This raises great challenges to airborne software modeling and verification. In order to achieve airborne software high-level requirements objectives, we propose a formal method of modeling high-level requirements based on knowledge graph. The method gives a formal language to describe knowledge graph and constructs knowledge graph collaboratively. Then we represents high-level requirements by causal model and formal modeling of high-level functional requirements and non-functional requirements by knowledge graph. These improve the requirement traceability, namely these are helpful to trace the high-level requirements to system requirements so as to achieve high-level requirements' traceability objective that DO-178C demands. Additionally, we provide the modeling tool for domain experts to construct knowledge graph collaboratively and realize their high-level requirements modeling. We also give some high-level requirements verification. These are significant to generate safe, reliable, accurate and high-quality airborne software.