Enhancing B-Method by Timing Diagram

A Formal method is a requirements engineering technique used for specification, development and verification of software. B-Method is a Formal Method approach which uses set theoretic notations to specify and model systems. Event-B is adapted from the B-Method. Its events occur spontaneously rather than being invoked. Therefore, Event-B is suitable for reactive and real time systems. However, Event-B lacks remarkable features for identifying time constraints, such as Timing diagrams. Thus, the Timing diagram is introduced in this paper for enhancing the Event-B. In this paper we demonstrate techniques to create an Event-B model from the Timing diagram. We propose a pattern to transform the Timing diagram into the Event-B model. The Timing diagram which is used in the paper is adapted, from UML 2.0 Timing diagram, to have features to support translating from the Timing diagram into the Event-B model. We use a case study: a Lift Display system as an example for translating