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

Abstract

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.