spardl模型的event-b解释

？针对由周期行为和模式转换机制组成的实时系统提出的spardl需求建模语言，详细阐明了其对应的spardl模型的event-b解释。通过event-b来解释spardl的语义，同时提出一种基于spardl模型特征的精化框架用于event-b模型的开发。最后，通过案例研究的分析展示用event-b对spardl模型建模和验证的方法的有效性。