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