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

• 作者: 孙健 徐敏
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: AADL 数据流时延 形式化描述 时间自动机 性质验证
• 年，卷（期）: 2016,（4）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 41-45
• 页数: 5页
• 分类号: TP302
• 字数: 5428字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2016.04.009

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐敏	南京航空航天大学计算机科学与技术学院	31	222	7.0	14.0
2	孙健	南京航空航天大学计算机科学与技术学院	17	192	6.0	13.0