Event-B Trace Semantics Clause Samples

Event-B Trace Semantics. In this section we briefly present how traces of an Event-B model are constructed. Much more detailed treatment of the subject is given in [10] and [11]. An elementary step of a machine interpretation is the computation of the set of next states for some current event. For some event e the next states are found by selecting a set of suitable values for the event parameters and using them to characterise the possible next states vj. An Event-B machine may be understood as a relation T : Event S S : T =df pe (Ge(pe, v) Se(pe, v, vj)). Here pe, Ge, Se are the event parameters, guard and before-after predicate. T is a predicate character- ising a relation on system states: it is a total function from events to relations on states. A next event would start from a state produced by a previous event. This is expressed with the sequential composition operator ";": e1; e2 = v1 T (e1)[v1/vj] T (e2)[v1/v]. v1 is a vector of fresh names used to record the final state of e1 and pass it on to e2. The concept of sequential composition can be generalised to a chain of events. Operator seq performs a sequential composition over an event list: seq( ) = id(S) and seq( e t) = T (e); seq(t). From these definitions, the traces of a machine are formulated as all possible traces reachable from the initial machine state Init: traces(M) = {t | seq(t)[Init] ƒ= ø} In the next section we use the traces semantics of flows and Event-B to define the consistency conditions for a model combining a flow expression and an Event-B machine.