An Event-B Interpretation for SPARDL Model

Real time systems consisting of periodic behaviors together with the mode transition mechanism are largely applied in the development of control systems for spacecrafts and automobiles in industry. We have proposed a requirement modeling language called SPARDL for modeling and analyzing such periodic control systems in [11]. In this paper, we specify an Event-B interpretation for the SPARDL model. The semantics of SPARDL is presented by Event-B and a refinement framework is introduced to develop the Event-B models based on the features of the SPARDL model. Furthermore, a case study is analyzed to show the effectiveness of our proposed approach to modeling and validation of the SPARDL model by Event-B.