分布式航电系统可调度性分析的组合方法
计算机科学中的逻辑
2018-08-01 v1 形式语言与自动机理论
软件工程
摘要
本工作提出一种用于分布式综合模块化航电（DIMA）系统可调度性分析的组合方法，该系统由空间分布的ARINC-653模块通过统一AFDX网络互联而成。我们将DIMA系统建模为UPPAAL中的一组秒表自动机，通过模型检验验证其可调度性。然而，由于状态空间庞大，直接模型检验不可行。因此我们引入组合分析，逐个检查每个分区及其通信环境。基于消息接口的概念，构建若干消息发送自动机以建模分区的环境。我们定义了时间选择模拟关系，支持复合消息接口的构造。通过使用假设-保证推理，我们确保每项任务满足截止时间且通信约束在全局也得以满足。该方法应用于一个具体DIMA系统的分析。
引用
@article{arxiv.1807.11570,
title = {A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems},
author = {Pujie Han and Zhengjun Zhai and Brian Nielsen and Ulrik Nyman},
journal= {arXiv preprint arXiv:1807.11570},
year = {2018}
}
备注
In Proceedings MeTRiD 2018, arXiv:1806.09330. arXiv admin note: text overlap with arXiv:1803.11050