Meta-Predicates 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. Fur- thermore, 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.

Publication
Presented at Rodin Workshop
Date