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