基于NuSMV的AADL模型形式化验证技术

Architecture Analysis and Design Language (AADL) is a modeling language used to describe the architecture and behavior of mission critical embedded system, which is widely used in the aerospace field.To verify the correctness of the key attributes of AADL model and system behavior, this paper studies the formal verification method for the AADL model based on NuSMV(New Symbolic Model Verifier).Firstly, covering all the software components and behavior characteristics of AADL model, mapping rules and transformation algorithm from the AADL model to the NuSMV model are proposed.Secondly, correctness of the transformation algorithm is analyzed by the graph isomorphism method.Then, the temporal logic formula is used to describe the attributes to be verified in the NuSMV model, so as to verify the safety, activity and nested mode configuration in the AADL model.Finally, taking the flight control system as an example, the formal verification method of AADL model based on NuSMV is explained in detail, and the statistical information of verification attributes is given.