基于Z-AADL模型的形式化转换

结构分析与设计语言(Architecture Analysis and Design Language,AADL)是针对嵌入式实时系统领域中的软件开发复杂度问题而提出的一种基于模型驱动开发的体系结构建模语言,可用于设计和分析一些安全关键嵌入式实时系统的软硬件体系结构。但是AADL严格来说只是一种半形式化的建模语言,虽然也描述了模型中构件的属性,但是对模型的非功能属性并没有明确的形式化描述,因此对AADL系统模型的非功能属性进行形式化验证,对于保证系统的正确性和可靠性具有重要意义。针对AADL模型中对非功能属性及数据性质等描述的不足之处,将其与形式规格说明语言Z语言相结合,提出了一种新的描述能力更加强大的形式规范语言—Z-AADL,并且定义了将Z-AADL模型转换为形式化模型—ZIA模型的转换规则,以实现Z-AADL模型到ZIA形式化模型的转换。并通过一个转换实例进行说明。