基于AADL的信息物理融合系统的建模与验证

发布时间：2018-10-13 08:26

【摘要】：信息物理融合系统CPS是通过计算、通信与控制技术有机和深度的融合实现计算资源与物理资源紧密结合的下一代智能系统,体系结构分析与设计语言AADL是一种基于构件的体系结构建模语言,是嵌入式实时系统体系结构描述语言标准,广泛应用于航空电子等安全关键领域的系统建模分析。本文基于AADL将形式化建模与验证方法引入CPS的分析与设计中,提出了一套面向CPS的模型建立、模型转换及模型验证的完整框架。首先,对AADL的基本建模元素、建模流程及CPS系统特点、建模需求进行研究分析,总结AADL对CPS软硬件体系结构建模的优点,以及对CPS中大量数据和并发、不确定关系缺乏形式化描述的不足,基于形式化规格说明语言Z和进程演算对AADL进行扩充,为AADL添加对变量约束的Z模式和并发、不确定以及动作约束算子的描述,对数据进行形式化的描述来对其进行约束,对动态并发、不确定的因素进行建模,提出一种能够描述CPS系统行为的体系结构建模规范CPS-AADL。其次,由于AADL不支持直接的形式化验证,本文在构件交互自动机研究的基础上提出一种带数据约束并支持系统构件交互描述的形式化规范,带数据约束的构件交互自动机Z-COIA,同时给出Z-COIA的组合验证算法,并将CPS-AADL模型转换到Z-COIA形式化规范,给出了模型转换规则及其正确性说明。最后,在经典时序逻辑的基础上提出了面向Z-COIA的时序逻辑系统CIA-CTL,并给出其具体的语法语义定义和模型检测算法,从而实现了对CPS-AADL模型检测和验证分析,并通过一个典型的CPS系统——喷气飞机的飞行导航系统的模型建立、模型转换以及模型验证的具体过程和对本文给出的形式化建模与验证的整体框架进行分析实践,验证了提出的形式化建模方法的可行性和有效性。
[Abstract]:The information physics fusion system (CPS) is the next generation intelligent system which combines the computing resources with the physical resources through the organic and deep fusion of computing, communication and control technology. Architecture Analysis and Design language (AADL) is a component-based architecture modeling language, which is the standard of embedded real-time system architecture description language. It is widely used in avionics and other key areas of system modeling and analysis. Based on AADL, the formal modeling and verification method is introduced into the analysis and design of CPS, and a complete framework of model building, model transformation and model verification for CPS is proposed. First of all, the basic modeling elements of AADL, modeling process and characteristics of CPS system, modeling requirements are analyzed, and the advantages of AADL in modeling CPS hardware and software architecture are summarized, as well as a large amount of data and concurrency in CPS. Due to the lack of formal description of uncertain relations, AADL is extended based on formal specification language Z and process calculus, and the description of Z schema and concurrency, uncertainty and action constraint operators for variable constraints are added to AADL. Data is formally described to constrain it, and dynamic concurrency and uncertainty factors are modeled. An architecture modeling specification CPS-AADL., which can describe the behavior of CPS system, is proposed. Secondly, because AADL does not support direct formal verification, this paper proposes a formal specification with data constraints and supporting component interaction description based on the research of component interactive automata. The component interactive automata Z-COIAA with data constraints is given, and the combination verification algorithm of Z-COIA is given. The CPS-AADL model is converted to the formal specification of Z-COIA, and the rules of model transformation and its correctness are given. Finally, on the basis of the classical temporal logic, a temporal logic system (CIA-CTL,) oriented to Z-COIA is proposed, and its specific syntax and semantic definition and model checking algorithm are given, so that the CPS-AADL model detection and verification analysis are realized. And through a typical CPS system, the model establishment, model transformation and model verification of the jet aircraft flight navigation system, and the analysis and practice of the formal modeling and verification of the overall framework given in this paper. The feasibility and validity of the proposed formal modeling method are verified.
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP29

【参考文献】