基于时间抽象状态机的AADL模型验证

来源：软件学报杂志2015年第2期北京时间：

作者：杨志斌,胡凯,赵永望,马殿富,Jean-Paul BODEVEIX

单位：杨志斌，Institut de Recherche en Informatique de Toulouse, Université de Toulouse, Toulouse, France;北京航空航天大学 计算机学院, 北京 10019111,胡凯，北京航空航天大学 计算机学院, 北京 10019102,赵永望，北京航空航天大学 计算机学院, 北京 10019103,马殿富，北京航空航天大学 计算机学院, 北京 10019104,Jean-Paul BODEVEIX，Institut de Recherche en Informatique de Toulouse, Université de Toulouse, Toulouse, France05

摘要：提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance, navigation and control)进行了实例性验证.

关键词：AADL(architecture analysis and design language);TASM(timed abstract state machine);模型转换;形式验证

基金资助：法国航空航天基金; 软件开发环境国家重点实验室自主课题(SKLSDE-2014ZX-09, SKLSDE-2013ZX-30)