论文研究-基于BIP框架的DPU系统建模与验证.pdf下载

DPUdata process unit, 数据处理单元是嵌入式系统中的一个典型组件, 被广泛应用于太空领域, 它在层次化的嵌入式系统架构中起到承上启下的作用。保证这类安全攸关系统可靠性的主要方法包括冗余容错、测试和仿真。近年来, 形式化方法作为确保可靠性的一种重要补充, 得到了广泛的关注。BIPbehavior interaction priority是一个通用的系统级形式化建模框架, 支持层次化和模块化, 包含一套支持建模、模拟和验证的工具集。给出了一种基于BIP框架对DPU进行系统级建模与验证的一般方法, 总结了一套使用BIP框架对DPU建模应遵循的原则及技巧。以航天领域一个真实DPU系统为例, 系统地对方法、原则和技巧进行了介绍。通过该方法, 找出了使用传统方法难以发现的错误。实践表明, 该方法具有很好的可复用性和可扩展性, 是确保系统可靠性的有益补充。