A requirement modeling language called SPARDL was proposed for modeling and analyzing such periodic control systems consisting of periodic behaviors together with the mode transition mechanism. The Event-B interpretation was specified for the SPARDL model. The semantics of SPARDL were presented by Event-B and a refinement framework was introduced to develop the Event-B models based on the features of the SPARDL model. Finally, a case study was analyzed to show the effectiveness of our proposed approach to modeling and validation of the SPARDL model by Event-B.%针对由周期行为和模式转换机制组成的实时系统提出的SPARDL需求建模语言,详细阐明了其对应的SPARDL模型的Event-B解释.通过Event-B来解释SPARDL的语义,同时提出一种基于SPARDL模型特征的精化框架用于Event-B模型的开发.最后,通过案例研究的分析展示用Event-B对SPARDL模型建模和验证的方法的有效性.
展开▼
