AADL子集到TASM的转换规则研究

摘要

随着现代化的推进，计算机软件已广泛应用于航天航空、武器装备、交通等安全攸关的系统中。由于在安全攸关实时系统中一个微小的逻辑错误都有可能导致不可预见的灾难性后果，所以保证软件系统的质量成为了迫切的需求和挑战。对安全攸关系统的建模、分析与验证成为了现在模型验证方向的研究热点。
　　AADL语言即架构分析和设计语言是一种支持模型工程设计的半形式化建模语言，能表示安全攸关实时系统的功能性需求与非功能性需求，并已发布了标准语言库。但由于AADL语言的复杂性和半形式化语言的特性，所以对AADL子集的提取与AADL子集的形式化转换是我们急需解决的问题。TASM是一种形式化语言，能很好的描述AADL模型的功能性行为和非功能性（时间执行、资源消耗等）行为;并能通过简单的转换运行到验证和仿真工具上（如UPPAAL，TASM ToolSet等），对AADL模型进行正确性、一致性以及可调度性等非功能性验证。
　　为了实现对安全攸关实时系统的软件部分的AADL建模验证与分析，本文选取了一种AADL子集并对子集进行形式化转换。主要工作如下:
　　首先，在AADL全集的基础上，基于最小化原则、可实现性原则以及完备性原则选取了一种相对完整的AADL子集，并对AADL子集构件进行描述。
　　其次，实现AADL子集到TASM的形式化转换，完成子集到TASM的转换规则，并以伪代码形式对规则进行描述。转换规则中设计了线程构件内的基于多级调度的调度协议转换规则，实现多级调度模型的构建。
　　最后，以ARINC653标准的飞行控制系统的软件系统为实例模型，利用开源工具OSATE实现AADL到TASM的转换，并在UPPAAL上验证多级调度系统的可调度性，从而验证TASM转换规则的可行性。

目录

声明

摘要

第一章 绪论

1．1 课题研究背景与意义

1．2 国内外研究现状

1．3 存在的问题

1．4 本文的研究目标与工作

1．5 论文的结构

第二章 研究基础

2．1 AADL概述

2．1．1 AADL构件

2．1．2 AADL端口和连接

2．1．3 AADL语法

2．2 时间抽象状态机TASM

2．2．1 TASM简介

2．2．2 TASM的抽象语法

2．3 开源工具OSATE

2．4 UPPAAL工具

2．5 本章小结

第三章 一种AADL子集的选取

3．1 引言

3．2 AADL子集标准

3．2．1 AADL子集标准遵守的原则

3．2．2 AADL子集满足原则的论述

3．3 AADL子集要素分析

3．3．1 AADL子集的BNF范式描述

3．3．2 系统构件

3．3．3 进程构件

3．3．4 端口通信

3．3．5 线程构件

3．3．6 模式转换

3．3．7 行为附件

3．4 本章小结

第四章 AADL子集到TASM的转换

4．1 引言

4．2 系统构件的转换

4．3 进程构件的转换

4．4 模式的转换

4．5 端口通信的转换

4．5．1 数据事件端口通信的线程构件

4．6 线程构件的转换

4．6．1 线程执行的转换

4．6．2 分派器的转换

4．6．3 行为附件的转换

4．6．4 调度器的转换

4．7 相关工作对比

4．8 本章小结

第五章 多级调度验证

5．1 系统模型构建

5．2 模型转换实现

5．3 可调度性验证

第六章 总结与展望

6．1 总结

6．2 展望

参考文献

攻读硕士学位期间参加的科研项目

致谢