Specification and refinement of discrete timing properties in Event-B

Abstract: Event-B is a formal language for systems modeling, based on set theory and predicate logic. It has the advantage of mechanized proof, and it is possible to model a system in several levels of abstraction by using refinement. Discrete tim-ing properties are important in many critical systems. However, modeling of timing properties is not directly supported in Event-B. In this paper we identify three main categories of discrete timing properties for trigger-response pattern, deadline, delay and expiry. We introduce language constructs for each of these timing properties that augment the Event-B language. We describe how these constructs can be mapped to standard Event-B constructs. To ease the process of using the timing constructs in a refinement-based development, we introduce patterns for refining the timing constructs that allow timing properties on abstract models to be replaced by tim-ing properties on refined models. The language constructs and refinement patterns are illustrated through some generic examples. Event-B refinement allows atomic events at the abstract level to be broken down into sub-steps at the refined level. The goal of our refinement patterns is to provide an easy way to represent and cor-rectly refine timing constraints on abstract atomic events with more elaborate timing constraints on the refined events. This paper presents an initial set of patterns