Meta-Predicate for Rodin

Abstract

Event-B provides a concise mathematical language for specifying invariants and guards. While both Event-B and Rodin matured, certain patterns for specifying properties like deadlock freedom emerged and are in use. These pat- terns are often realized by copy and paste of guards into other guards or in- variants, leading to duplicated code and incomprehensible specifications. Furthermore, it may lead to errors if predicates are not kept in sync. We observed errors like these during the case studies of ABZ 2014 and started developing an extension to Event-B that allows accessing guards by corresponding event names. Since, it has been implemented as a plugin for the Rodin platform.