基于UPPAAL的嵌入式系统AADL模型实时性验证-计算机科学与技术专业论文.docx

 承诺书 本人声明所呈交的博/硕士学位论文是本人在导师指导下 进行的研究工作及取得的研究成果。除了文中特别加以标注和 致谢的地方外，论文中不包含其他人已经发表或撰写过的研究 成果，也不包含为获得南京航空航天大学或其他教育机构的学 位或证书而使用过的材料。 本人授权南京航空航天大学可以将学位论文的全部或部 分内容编入有关数据库进行检索，可以采用影印、缩印或扫描 等复制手段保存、汇编学位论文。 （保密的学位论文在解密后适用本承诺书） 作者签名： 日 期：    摘 要 随着嵌入式系统的规模、复杂程度和可靠性需求的不断提升，模型驱动的体系结构开发方 法已经成为复杂嵌入式系统开发的主流。体系结构分析与设计语言 AADL（Architecture Analysis and Design Language, AADL）是嵌入式实时系统领域模型驱动方法的新标准，在支持系统软、 硬件结??建模的同时可对可靠性、实时性等非功能属性的描述，可在模型驱动开发过程早期的 模型建立阶段，通过形式化的模型检验方法对系统模型的关键属性进行验证，及早发现设计过 程中潜在的错误，对保障系统实时性和提高开发效率都具有重要的意义。 为了对 AADL 模型的可调度性和数据流时延特性进行验证，本文采用时间自动机形式化模 型检验方法建立了 AADL 模型中调度模型和数据流的时间自动机，实现了从 AADL 模型到时 间自动机模型的转换和验证工作。在调度模型时间自动机的建立中，设计了周期、非周期的线 程模板以及抢占和非可抢占的调度器模板，通过模型转换法则将 AADL 调度模型转换到时间自 动机模型。在数据流的模型转换中，分别设计了单一数据流和混合数据流到时间自动机的转换 方法，混合数据流转换得到的时间自动机可与调度模型时间自动机构成时间自动机网络，实现 了数据流与调度模型的综合分析与验证。 利用 Eclipse 的插件开发技术，设计了自动化模型转换插件并将其集成到 AADL 的建模工 具 OSATE 中，实现了建模、转换、验证与分析过程的集成开发环境。最后利用时间自动机建 模与验证工具 UPPAAL 对转换得到的时间自动机进行模拟和验证，等价地验证原 AADL 模型 的设计是否满足实时性要求。测试数据表明，所建立模型转换方法能有效地将 AADL 模型转换 到时间自动机模型，在 UPPAAL 中能够正确地分析原模型的可调度性和数据流时延特性。 关键词： AADL，时间自动机，可调度性，数据流时延，模型转换，UPPAAL i  ABSTRACT With the increasing size, complexity and reliability requirements of embedded system, the architecture development method of model driven has become popular in embedded real-time system. Architecture Analysis and Design Language (AADL) is a new standard of model driven system engineering for embedded real-time system. It supports soft/hardware structural modeling, and imports non-functional attributes description such as real-time and security qualities. During the process of MDD (Model-Driven Development), it is of great significance for ensuring the system real-time performance and improving the efficiency of system development to find potential design problems on critical aspects in the model design stage. In order to analyze the schedulability and flow latency of AADL models, time automata is established for both scheduling model and data flows of AADL model using the formal analysis method, which realizes