Specification and refinement of discrete timing properties in Event-B

Abstract

Event-B is a formal language for systems modeling, based on set theoryand predicate logic. It has the advantage of mechanized proof, and it is possible tomodel a system in several levels of abstraction by using refinement. Discrete timingproperties are important in many critical systems. However, modeling of timingproperties is not directly supported in Event-B. In this paper we identify three maincategories of discrete timing properties for trigger-response pattern, deadline, delayand expiry. We introduce language constructs for each of these timing properties thataugment the Event-B language. We describe how these constructs can be mappedto standard Event-B constructs. To ease the process of using the timing constructsin a refinement-based development, we introduce patterns for refining the timingconstructs that allow timing properties on abstract models to be replaced by timingproperties on refined models. The language constructs and refinement patternsare illustrated through some generic examples. Event-B refinement allows atomicevents 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 correctlyrefine timing constraints on abstract atomic events with more elaborate timingconstraints on the refined events. This paper presents an initial set of patterns.