4. Formal modeling and proving of Campus Management System: Event-B perspective

[Full PDF Text]


Nadeem Akhtar, Malik M. Saad Missen, and Rida Zahra Hashmi .


Campus Management System (CMS) provides the management and information processing services that are critical for the efficient working of the university. A CMS is a complex system formed by the integration of a number of interacting sub-systems working together. Errors at any level in CMS can cause huge loss, therefore it is important to ensure correctness of the system. A CMS has been formally specified, modeled, and validated for the Baghdad-ul-Jadeed campus of The Islamia University of Bahawalpur, Pakistan. It provides a formally validated correct platform for automation and management of all the aspects of student admission, examination, student attendance, results and faculty attendance. This CMS is based on formal modeling and formal proofs to ensure correctness, with model-based methods with underlying mathematical concepts of set theory and first-order predicate calculus. A novel abstraction and refinement based formal method Event-B is used. It has an exhaustive industrial development platform RODIN which provides exhaustive evaluation and implementations. The proposed CMS model is centered on the fundamental principles of abstraction and refinement.

Index Terms:

Campus Management System (CMS); Event-B; Formal modeling; Formal validation; Theorem Proving; RODIN.

Cite this: Nadeem Akhtar, Malik M. Saad Missen, and Rida Zahra Hashmi, “ Formal modeling and proving of Campus Management System: Event-B perspective ”, BUJICT Journal, Volume 10,  Issue, II December 2017, pp. 1-6.


[1] Jean-Raymond Abrial, Modeling in Event-B System and Software Engineering.: Cambridge University Press, 2010.
[2] Jean-Raymond Abrial et al., “Rodin: An Open Toolset for Modelling and Reasoning in Event-B,” International Journal on Software Tools for Technology Transfer (STTT), vol. 12, no. 06, pp. 447-466, November 2010.
[3] Lili Xu and Hong Zhang, “Formal Verification of Software Safety Criteria Using Event-B,” in International Conference on Reliability, Maintainability and Safety (ICRMS), 2014, pp. 342-347.
[4] Fabio Levy Siqueira, Thiago C. de Sousa, and Paulo S. Muniz Silva, “Using BDD and SBVR to refine business goals into an Event-B model: a research idea,” in IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), 2017, pp. 31-36.
[5] Dieu Huong Vu, Anh Hoang Truong, Yuki Chiba, and Toshiaki Aoki, “Automated testing reactive systems from Event-B model,” in 4th NAFOSTED Conference on Information and Computer Science, 2017, pp. 207-212.
[6] Yousra Ben Daly Hlaoui, Ahlem Ben Younes, and Leila Jemni Ben Ayed, “From Sequence Diagrams to Event B: A Specification and Verification Approach of Flexible Workflow Applications of Cloud Services Based on Meta-model Transformation,” in IEEE 41st Annual Computer Software and Applications Conference, 2017, pp. 187-192.
[7] Nestor Catano, “An Empirical Study on Teaching Formal Methods to Millennials,” in IEEE/ACM 1st International Workshop on Software Engineering Curricula for Millennials (SECM), 2017, pp. 3-8.
[8] Guillaume Babin, Yamine Ait-Ameur, and Marc Pantel, “Web Service Compensation at Runtime: Formal Modeling and Verification Using the Event-B Refinement and Proof Based Formal Method,” IEEE TRANSACTIONS ON SERVICES COMPUTING, vol. 10, no. 1, pp. 107-120, January/February 2017.
[9] Michael Jastram and Michael Butler, Rodin User’s Handbook: Covers Rodin V.2.8. USA: CreateSpace Independent Publishing Platform, 2014.
[10] M. Leuschel and M. Butler, “ProB: A Model Checker for B,” in Proceedings FME 2003, Pisa, Italy, 2003, pp. 855-874.