Research On Formal Modeling And Refinement For Avionics Software Requirements

With the increasing importance of avionics software in avionics systems,the de-sign and establishment of formal modeling and verification methods to support accurate and efficient avionics software requirements has become the key to enhance the safety and development efficiency of avionics systems,and is necessary to meet the formal development requirements of airworthiness standards.Sys ML/MARTE,a graphical description-based modeling language,is the mainstream modeling language used in Model Based Software Engineering(MBSE)and is often applied to the specification of safety-critical software requirements.Compared with natural language,graphical re-quirements description improves the expressiveness and comprehensibility of require-ments,which is conducive to the improvement of R&D efficiency.However,due to the lack of systematic and rigorous semantic definitions,Sys ML/MARTE can cause problems in terms of accuracy and consistency to system development,threatening the correctness of safety-critical software.In this paper,in response to the multi-level,multi-source and highly complex re-quirements of avionics systems,we construct a safety modeling language Safety＿Sys ML State Machine(S~2MSM)for avionics software requirements based on extracting the safety subsets of Sys ML and MARTE modeling languages and combining safety au-tomata theory for avionics software requirements.The main contributions of this paper are as follows:·A formal modeling language S~2MSM for avionics multi-level requirements is proposed,which extracts the safety subsets of Sys ML and MARTE modeling languages and combines safety automata theory to support the analysis and verification of avionics high-level requirements and low-level requirements.·A formal syntax and semantics for S~2MSM is constructed,and a formal semantics for modeling elements and semantic environments in S~2MSM is constructed using a labeled transition system as the semantic model for S~2MSM.The language innovatively integrates the theoretical knowledge of behavioral state machines and security automata to construct a hierarchical semantics that enhances the accuracy and consistency in the development process and is widely applicable to safety-critical systems.·Refinement mapping relations and refinement mapping rules from S~2MSM high level requirement model to S~2MSM low level requirement model are constructed.The refinement mapping of models is analyzed from the perspective of structure and RTC semantics,and the feasibility and correctness of the S~2MSM modeling language for developing avionics software is demonstrated.·A formal modeling tool based on S~2MSM,S~2M,is designed and implemented to support the formal modeling and verification of safety-critical software requirements using S~2MSM.To demonstrate the feasibility and effectiveness of the approach,this paper illus-trates the specific application of S~2MSM and refinement mapping rules in a safety-critical system using an aircraft roll angle control system as an example.