Verifying the Safety of Aviation Software Based on Extended Colored Petri Net

Abstract EN

At present, various functions of aircraft have become more and more dependent on airborne software system, and the structure of modern airborne software is extremely complex.

Engineers need to eliminate the situation in which the safety performance of the entirety reduces caused by mutual influence among components.

This paper presents a comprehensive method with high efficiency for safety verification of airborne software system, in order to ensure the system meet safety requirement of airworthiness standard at the design stage.

Safety Verification Colored Petri Net (SVCPN) for software safety verification is firstly proposed, and then the mapping transformation rules from Block Definition Diagram (BDD) of System Modeling Language (SysML) to SVCPN are proposed to achieve the accurately formal description of software system.

Traversing all delivery paths of safety level transfer based on the Reachable Tree Diagram, to detect the components that do not meet the safety requirement of airworthiness standard.

Based on the disambiguation algorithm, the fundamental components that cause safety problem are found out through the establishment of antinet to achieve the safety level reassign, ensuring the safety performance of the whole system.

Finally, the case study and the comparison and analysis are applied to show the feasibility and superiority of our method.