结构分析描述语言（AADL）是一种描述任务关键嵌入式系统架构和行为的建模语言，在航空航天领域广泛被应用。为验证AADL模型的任务关键属性和系统行为的正确性，提出基于NuSMV（新符号模型检查器）的AADL模型形式化验证方法。首先，覆盖AADL模型的所有软件构件和行为特征，提出了AADL模型到NuSMV模型的映射规则和转换算法；其次，采用图同构方法分析了转换算法的正确性；然后，在NuSMV模型中采用时态逻辑公式对AADL模型中待验证属性进行描述，以验证AADL模型中安全性、活性和嵌套模态配置的正确性；最后，以飞行控制系统为例，详细阐释了基于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.
[1] 胡晓义, 王如平, 王鑫, 等.基于模型的复杂系统安全性和可靠性分析技术发展综述[J].航空学报, 2020, 41(6):523436. HU X Y, WANG R P, WANG X, et al.Recent development of safety and reliability analysis technology for model-based complex system[J].Acta Aeronautica et Astronautica Sinica, 2020, 41(6):523436(in Chinese).
[2] 朱和铨, 徐浩军, 张鹏, 等.模型驱动的软件构件研制保证水平验证方法[J].航空学报, 2015, 36(3):907-920. ZHU H Q, XU H J, ZHANG P, et al.Model-driven validation method for software component development assurance level[J].Acta Aeronautica et Astronautica Sinica, 2015, 36(3):907-920(in Chinese).
[3] FEILER H P, LEWIS B, VESTAL S.The SAE Architecture Analysis & Design Language (AADL) a standard for engineering performance critical systems[C]//2006 IEEE Conference on Computer Aided Control System Design, 2006 IEEE International Conference on Control Applications, 2006 IEEE International Symposium on Intelligent Control.Piscataway:IEEE Press, 2006:1206-1211.
[4] 刘超, 吴海桥.基于NuSMV的系统安全性分析平台开发和应用[J].飞机设计, 2013, 33(2):68-71. LIU C, WU H Q.Development and application of system safety analysis platform based on NuSMV[J].Aircraft Design, 2013, 33(2):68-71(in Chinese).
[5] MKAOUAR H, ZALILA B, HUGUES J, et al.From AADL model to LNT specification[M]//Lecture Notes in Computer Science.Cham:Springer International Publishing, 2015:146-161.
[6] D'SOUZA M, RAMESH S, SATPATHY M.Architectural semantics of AADL using Event-B[C]//2014 International Conference on Contemporary Computing and Informatics (IC3I).Piscataway:IEEE Press, 2014:92-97.
[7] HADAD A S A, MA C Y, AHMED A A O.Formal verification of AADL models by event-B[J].IEEE Access, 2020, 8:72814-72834.
[8] CHKOURI M Y, ROBERT A, BOZGA M, et al.Translating AADL into BIP-application to the verification of real-time systems[M]//Models in Software Engineering.Berlin, Heidelberg:Springer, 2009:5-19.
[9] ŎLVECZKY P C, BORONAT A, MESEGUER J.Formal semantics and analysis of behavioral AADL models in real-time maude[C]//Proceedings of the 12th IFIP WG 6.1 International Conference and 30th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems.Berlin, Heidelberg:Springer,2010:47-62.
[10] YANG Z B, HU K, MA D F, et al.From AADL to timed abstract state machines:A verified model transformation[J].Journal of Systems and Software, 2014, 93:42-68.
[11] 刘倩, 桂盛霖, 李允, 等.基于UPPAAL的AADL模型可调度性验证[J].计算机应用, 2009, 29(7):1820-1824. LIU Q, GUI S L, LI Y, et al.Schedulability verification of AADL model based on UPPAAL[J].Journal of Computer Applications, 2009, 29(7):1820-1824(in Chinese).
[12] YANG C X, DONG Y W, ZHANG F, et al.Formal semantics of AADL models with machine-readable CSP[C]//2012 IEEE/ACIS 11th International Conference on Computer and Information Science.Piscataway:IEEE Press, 2012:565-571.
[13] AHMAD E, DONG Y W, WANG S L, et al.Adding formal meanings to AADL with hybrid annex[C]//International Conference on Formal Aspects of Component Software 2014.Cham:Springer, 2015:228-247.
[14] ZHANG F, ZHAO Y W, MA D F, et al.Formal verification of behavioral AADL models by stateful timed CSP[J].IEEE Access, 2017, 5:27421-27438.
[15] BAO Y X, CHEN M S, ZHU Q, et al.Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2017, 36(12):1989-2002.
[16] YU H F, MA Y, GAUTIER T, et al.Exploring system architectures in AADL via Polychrony and SynDEx[J].Frontiers of Computer Science, 2013, 7(5):627-649.
[17] 刘博, 李蜀瑜.基于NuSMV的AADL行为模型验证的探究[J].计算机技术与发展, 2012, 22(2):110-113. LIU B, LI S Y.AADL behavior based on NuSMV model validation of inquiry[J].Computer Technology and Development, 2012, 22(2):110-113(in Chinese).
[18] SAE Aerospace.Architecture Analysis and Design Language (AADL):SAE AS5506[S].Warrendale:SAE International, 2017.
[19] Aerospace S A E.Architecture analysis and design language V2.0:SAE AS5506A[S].Warrendale:SAE International, 2012.
[20] SAE Aerospace.Annex behavior specification V1.6:SAE AS5506[S].Warrendale:SAE International, 2007.
[21] CAO H H, YING S, DU D H.Towards model-based verification of BPEL with model checking[C]//The Sixth IEEE International Conference on Computer and Information Technology (CIT'06).Piscataway:IEEE Press, 2006:190.
[22] YOUNES A B, HLAOUI Y B, AYED L J B.A meta-model transformation from UML activity diagrams to Event-B models[C]//2014 IEEE 38th International Computer Software and Applications Conference Workshops.Piscataway:IEEE Press, 2014:740-745.
[23] Object Management Group (OMG).UML 2.0 superstructure specification[EB/OL].[2020-10-31].https://www.omg.org/spec/UML/2.0/Beta1/Infrastructure/PDF.
CJA