使用形式化方法的定时分析

摘要

使用形式化方法的定时分析。提供了一种用于提供可扩展到具有大量任务和消息的工业情况研究的精确定时分析的方法和工具，包括：建模和分析任务和消息响应时间的能力；ECU使用；总线使用；任务/消息链的端到端等待时间；以及任务/消息图表中的定时同步问题。以被称为日历自动机的形式化结构建模系统任务和消息。模型时以诸如Promela的建模语言写成的，并且专用于分析规范的代码来仪器化。模型和仪器化从系统描述和分析规范中自动生成。通过诸如SPIN的兼容模型检查器对系统模型进行穷举性状态空间探索。探索期间，仪器化的代码产生对不同定时分析的结果。提供优化技术来生成模型，模型要求较少的存储和时间用于分析，并且使得方法可扩展到大型工业情况研究。