基于AADL的数据流转换与验证

来源：计算机技术与发展杂志2016年第04期北京时间：

作者：孙健;徐敏

摘要：AADL在嵌入式实时系统领域，支持系统软、硬件结构建模的同时又能对可靠性、实时性等非功能属性进行描述，可以在模型驱动开发过程中的早期模型建立阶段，通过形式化的模型检验方法对系统模型的关键属性进行验证，从而能够及早地发现在设计过程中存在的潜在错误，对保证系统实时性和提高开发效率来说都具有十分重要的意义。针对数据流时延特性问题，文中提出将AADL数据流的分析形成数据流的形式化描述的方法，建立这种形式化描述到时间自动机语义的映射关系作为映射法则的定义，并将时间自动机的转换按单一和混合两种类型分别给出了转换法则和转换实例的说明。在混合数据流转换中，新建了非周期线程的模板，以支持数据流的综合分析。最后给出了数据流性质验证的参考查询语句，并对数据流转换到的时间自动机模型进行了必要的实验检验。

关键词：AADL ;数据流时延;形式化描述;时间自动机;性质验证