Event-B Formalisation of a Chat System: A Case Study

Néstor Cataño

ªFaculdade de Ciencias e Tecnologia, Universidade do Algarve, Campus de Gambelas, Faro, 8005-139, Algarve, Portugal

**Abstract**

This paper presents the formal modelling and refinement of a chat system using the EVENT-B method. Software requirements are elicited as User Stories and systematically translated into EVENT-B syntax. We model core chat functionalities, including user creation, chat session creation, message sending, forwarding, deletion, and chat muting, while ensuring system consistency through invariants and discharging proof obligations with the Rodin IDE. We discuss design decisions, modelling challenges, and strategies for maintaining the correctness of dynamic, interactive system behaviours, addressing trade-offs between abstraction and executability, and promoting Correctness-by-Construction (CbC). The development adopts a two-phase refinement strategy: an initial horizontal refinement extending system behaviour, followed by a vertical data refinement that prepares abstract models for code generation. Statistical results on the number of proof obligations generated and automatically discharged provide insight into the practical modelling and verification effort. Finally, we highlight lessons learnt for applying EVENT-B to the formal specification of user-driven messaging systems.

**Keywords:** Event-B, Formal Methods, Refinement Calculus, Software Development Methodologies, Verification

# 1. Introduction

Formal methods offer a mathematically rigorous foundation for specifying and verifying software systems, thus helping to guarantee desirable properties such as safety. Among formal methods, EVENT-B [1] provides a refinement-based framework well suited for incrementally developing Correctness-by-Construction (CbC) systems [10, 11]. However, bridging the gap between informal requirements and formal specifications remains a challenging task.
This paper presents the formal modelling and refinement of a chat system using EVENT-B. The starting point for the development is a collection of informal User Stories, which are systematically translated into EVENT-B machines and events. Core functionalities such as user creation, chat session creation, content sending, forwarding, deletion, are formalised while preserving system invariants. Soundness of the EVENT-B model is enforced through the generation and discharge of proof obligations using Rodin [3].

The development adopts a two-phase refinement strategy. First, a hor-
izontal refinement incrementally extends system behaviour by introducing
read-status tracking of messages. Second, a vertical data refinement prepares
the model for code generation by replacing abstract set-based structures with
concrete sequence-based representations. Statistical results on proof obliga-
tions highlight the practical modelling and verification effort.

The **main contributions** of this work are: (i.) a complete formalisation of a dynamic, event-driven chat system using EVENT-B; (ii.) the identification of modelling patterns for dynamic state management and event guard design; (iii.) lessons on preparing abstract models for practical code generation through systematic refinement; (iv.) an illustration of challenges and best practices for modelling Correctness-by-Construction in user-interactive systems; and, a systematic approach for translating User Stories into formal EVENT-B specifications in the context of an interactive chat system.

This paper is organised as follows. Section 2 introduces preliminaries on EVENT-B notation. Section 3 discusses the software requirements of the chat system. Section 4 describes the abstract machine and its first refinement. Section 5 presents the vertical data refinement. Section 6 discusses modelling practices. Section 7 discusses statistics of the formal EVENT-B model, number of proof obligations generated and discharged with Rodin automatically. Section 8 reviews related work, and Section 9 concludes.

## 2. Preliminaries

Software development with EVENT-B starts with the definition of an
initial *blueprint* of the system one wants to model. This blueprint represents
the future system implementation. Blueprints give insight on some but not
all the aspects of the future system. A blueprint then goes through a series
of stages called refinements [2]. A blueprint refinement adds details to the
blueprint. Refinements provide a hierarchical organization of the blueprints.
The design of the initial system blueprint and its subsequent refinements
are based on the description contained in an existing software requirements document. Each stage of blueprint organisation serves a different purpose. At higher levels, blueprints are used to state key system properties. At lower levels, blueprints implement the system behaviour. It is crucial that the initial blueprint and its refinements are consistent with each other, and that they are coherent with respect to the system specification. A refinement step generates Proof Obligations (POs) expressed in predicate logic to assert that the blueprint refinement is a refinement of the blueprint. That is, POs guarantee that the blueprint and its refinements represent the same system.

In EVENT-B, system blueprints are referred to as *machines*. EVENT-B supports two main kinds of machine refinements: *horizontal refinement* and *vertical refinement* [1]. Horizontal refinement, sometimes called *superposition* in the literature, allows developers to extend and enrich the system's behaviour by introducing new events or strengthening existing ones. Through horizontal refinement, a machine can: (i.) add new events, (ii.) strengthen event guards (in the case of refinement), (iii.) add new guards and actions via event extension, or (iv.) enrich event actions while preserving previously established properties. The horizontal refinement is considered complete once all software requirements have been incorporated into the model.

Vertical refinement is *data refinement*: it transforms the model into a close-to-implementation model, e.g. finite sets are transformed into Boolean arrays or sequences of elements. A key part of vertical refinement is the definition of a *gluing invariant* that bridges the abstract machine with its refinement by stating properties of the combined machines. A final vertical refinement step is typically realised with a code generator [5, 17, 7].

## 2.1. Event-B Mathematical Notation

EVENT-B provides a full battery of set and relation notation. Figure 1 shows some of the EVENT-B mathematical notation used by EVENT-B. We use square brackets to apply (evaluate) a relation to (over) a set of elements as mentioned above. For instance, $r[s]$ applies relation $r$ to all the elements in set $s$. The result of $r[s]$ is a set of elements in the range of relation $r$. EVENT-B provides standard notations for set union, intersection, difference, etc. Symbol $\times$ denotes the cross product between two sets. The operator **dom** returns the domain of a relation, and **ran** its range relation. The expression $id[s]$ denotes the identity relation over a set of elements $s$. Applying the forward composition relation $q;r$ to an element $a$ in the domain of relation $q$ returns a set of elements calculated as the result of applying $r$ to
<table><caption>Figure 1: Basic EVENT-B mathematical notation</caption><thead><tr><td>Syntax</td><td>Name</td><td>Definition</td></tr></thead><tbody><tr><td>s &lt;&lt; r</td><td>domain restriction</td><td>{(x, y) | (x, y) &isin; r &and; x &isin; s}</td></tr><tr><td>s &lt;= r</td><td>domain subtraction</td><td>{(x, y) | (x, y) &isin; r &and; x &notin; s}</td></tr><tr><td>r &rarr; s</td><td>range restriction</td><td>{(x, y) | (x, y) &isin; r &and; y &isin; s}</td></tr><tr><td>r &rarr; s</td><td>range subtraction</td><td>{(x, y) | (x, y) &isin; r &and; y &notin; s}</td></tr><tr><td>r[s]</td><td>relational image</td><td>{y | (x, y) &isin; r &and; x &isin; s}</td></tr><tr><td>r &oplus; q</td><td>relational overriding</td><td>{(x, y) | (x, y) &isin; q &or; ((x, y) &isin; r &and; &not; &exist; z &middot; (x, z) &isin; q)}</td></tr></tbody></table>

q[{a}] . When a relation q is a function, q[{a}] should be used as q(a) . The domain restriction relation expression s<r restricts the domain of a relation r to (consider only elements in) a subset s of its domain. The range restric- tion relation expression r>s restricts the range of relation r to consider only elements in a subset s of its range. Domain (range) subtraction is defined similarly to domain (range) restriction, except that the elements in the set s are disregarded rather than considered.

## 2.2. Event-B Relations and Functions

Relations are sets of pairs. A relation f with domain A and range B is denoted as $A \leftrightarrow B$. If f is a function defined for all elements of A, we say that f is a total function, and we write $f: A \to B$. If f is defined for some values of A, we say that f is a partial function, and we write $f: A \mapsto B$. If f is a function such that no element in its range is associated with more than one element in the domain of f, then we say that f is a one-to-one or injective function, and we write $f: A \to B$. If f is a function whose range is B, we say that f is an onto or surjective function, and we write $f: A \mapsto B$. If f is both one-to-one and onto, then f is a bijection, and we write $f: A \leftrightarrow B$.

# 3. Software Requirements for the Chat System

We elicited the software requirements of the chat system based on the core functionalities observed in widely used messaging applications, includ- ing WHATSAPP. Our focus is on basic interactions, such as user creation, messaging, and session management. We purposely abstract away from soft- ware requirements rooted in the user interface, as these may involve the
interplay of multiple core functionalities. Our focus remains on modelling the core functionality.

No completely flawless automated mechanism or silver bullet exists to translate User Stories into an EVENT-B formal specification. Nonetheless, we stick here to strict guidelines as described in the following. Software requirements (the User Stories) can relate the static part of an EVENT-B machine, its dynamic part, or both parts. We thus start by modelling the static part of the EVENT-B machine, that is, the machine context, which includes the definition of constants, sets, and axioms. The machine context is used by the abstract EVENT-B machine and its machine refinements. The machine declares, for instance, machine (state) variables and invariants, which restrict the values that the variables can take. Machine variables are also part of the static part of the machine. The dynamic part of the models is the set of machine events.

<table><caption>Table 1: Chat machines hierarchy</caption><thead><tr><td>Machine</td><td>Observations</td></tr></thead><tbody><tr><td>Abstract</td><td>basic chat functionality with users</td></tr><tr><td>Ref. 1</td><td>active and muted chats, read and unread content</td></tr><tr><td>Ref. 2</td><td>screen chats and sequences</td></tr></tbody></table>

Table 1 shows the machine hierarchy of the EVENT-B model of the chat system. The abstract machine observes basic functionality for chat sessions, including the functionality for creating a chat session, selecting or unselecting a chat, chatting, deleting content, removing content, deleting a chat session, muting and unmuting a chat, and broadcasting and forwarding network content. The first machine refinement (horizontal refinement) includes functionality that checks whether chat content has been read or not. The second machine refinement adds implementation details; for instance, it represents content as a sequence (rather than a set) of content items. This is useful for chat sessions that are implemented as a sequence of ordered content displayed from top to bottom. It would further help us formulate a property that says that for any chat session, the chat content appears identical to both users. This property is a safety invariant: it states that “some desirable situation always holds”, or, that “nothing bad happens”.

US-01 describes the functionality for creating a chat session between Me and Another-User. The chat may not exist already.
<table><tr><td>US-01</td><td><strong>create-chat-session</strong></td></tr><tr><td>Description</td><td>As a user, I want to create a chat session so that I can communicate with Another-User</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> A chat session between Me and Another-User does not exist</td></tr><tr><td>Criterion</td><td><strong>When:</strong> I decide to create chat session with Another-User<br/><strong>Then:</strong> Chat session between Me and Another-User is created</td></tr></table>

US-02 describes the functionality for selecting a chat session. The effect of having two Given conditions is the condition obtained as the conjunction of both.

<table><tr><td>US-02</td><td><strong>select-chat</strong></td></tr><tr><td>Description</td><td>As a user, I want to select a chat session so that I can start chatting with Another-User</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> A chat session between Me and Another-User exists</td></tr><tr><td>Criterion</td><td><strong>Given:</strong> A chat session between Me and Another-User is not active<br/><strong>When:</strong> I select a chat session with Another-User<br/><strong>Then:</strong> The chat session between Me and Another-User is made active</td></tr></table>

US-03 introduces the functionality used for Me to chat with Another-User. Sent content is made available for both users Me and Another-User.

<table><tr><td>US-03</td><td><strong>chatting</strong></td></tr><tr><td>Description</td><td>As a user, I want to send some content during a chat session with Another-User so that I can transmit some information</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> Chat session with Another-User is active</td></tr><tr><td>Criterion</td><td><strong>When:</strong> Content is produced and sent by Me<br/><strong>Then:</strong> Content is made available to Me as well as to Another-User</td></tr></table>
US-04 describes the behaviour whereby chat content is deleted from the sender's chat.

<table><tr><td>US-04</td><td><strong>delete-content</strong></td></tr><tr><td>Description</td><td>As a user, I want to delete some content exchanged with another user during a chat session to unclutter my chat</td></tr><tr><td>Acceptance<br>Criterion</td><td><strong>Given:</strong> Content exists<br><strong>When:</strong> Me decides to delete the content he has received<br><strong>Then:</strong> The content is deleted from Me</td></tr></table>

Deleting a chat session between Me and Another-User does not delete the content as seen by Another-User, regardless of who sent the content to whom.

<table><tr><td>US-05</td><td><strong>delete-chat-session</strong></td></tr><tr><td>Description</td><td>As a user, I want to delete a chat session with Another-User</td></tr><tr><td>Acceptance<br>Criterion</td><td><strong>Given:</strong> A chat session between Me and Another-User exists<br><strong>When:</strong> I select to delete the only active chat session<br><strong>Then:</strong> The chat session is deleted as well as its associated content</td></tr></table>

When a chat session has been muted, communication between the two chat users is disabled both ways. Nevertheless, communication can be enabled later on.

<table><tr><td>US-06</td><td><strong>mute-chat</strong></td></tr><tr><td>Description</td><td>As a user, I want to mute a chat session so that I can prevent communication with and from Another-User</td></tr><tr><td>Acceptance<br>Criterion</td><td><strong>Given:</strong> Chat session between Me and Another-User exists<br><strong>When:</strong> I select to mute a chat session<br><strong>Then:</strong> Chat session is muted and no communication from Me to the muted user or vice-versa is permitted</td></tr></table>

US-07 re-establishes the communication between two users of a muted chat. Only the user who muted the chat can unmute it.
<table><tr><td>US-07</td><td><strong>unmute-chat</strong></td></tr><tr><td>Description</td><td>As a user, I want to unmute a chat session so as to reestablish communication with another user</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> Chat session between Me and Another-User is muted</td></tr><tr><td>Criterion</td><td><strong>Given:</strong> I had muted the chat session previously<br><strong>When:</strong> I select to unmute a chat session<br><strong>Then:</strong> Communication between Me and Another-User is re-established</td></tr></table>

US-08 and US-09 describe the situation whereby some content is sent to a group of users; forwarding a content requires that respective chat sessions between Me and the group of users exist, broadcasting creates new chat sessions if they do not exist already.

<table><tr><td>US-08</td><td><strong>broadcast</strong></td></tr><tr><td>Description</td><td>As a user, I want to broadcast a content to a group of users so that I can communicate with all of them quickly</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> Me wants to broadcast some content</td></tr><tr><td>Criterion</td><td><strong>Given:</strong> Me decides to broadcast the content to Other-Users<br><strong>When:</strong> The content is sent to Other-Users</td></tr></table>

<table><tr><td>US-09</td><td><strong>forward</strong></td></tr><tr><td>Description</td><td>As a user, I want to forward a content to a group of users so that I can communicate with all of them quickly</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> Me wants to forward some content</td></tr><tr><td>Criterion</td><td><strong>Given:</strong> Respective chats between Me and Other-Users exist<br><strong>When:</strong> Me decides to forward the said content to Other-Users<br><strong>Then:</strong> The content is sent to Other-Users</td></tr></table>

US-10 is the counterpart of US-02, unselecting a chat requires the chat to be active.
<table><tr><td>US-10</td><td><strong>unselect-chat</strong></td></tr><tr><td>Description</td><td>As a user, I want to unselect a chat session so that I can chat with Another-User</td></tr><tr><td>Acceptance</td><td><strong>Given:</strong> A chat session between Me and Another-User exists</td></tr><tr><td>Criterion</td><td><strong>Given:</strong> A chat session between Me and Another-User is active<br/><strong>When:</strong> Me wants to make the session with Another-User inactive<br/><strong>Then:</strong> Chat session between Me and Another-User becomes inactive</td></tr></table>

US-09 and US-10 could alternatively have been modelled without explicitly requiring the chat to be inactive or active, respectively. In contrast, by explicitly specifying these **Given** conditions in the User Stories and preserving them within the EVENT-B models, we adopt a *defensive* modelling strategy. This approach enforces that the system must occupy the correct state prior to any transition, thereby strengthening correctness guarantees and reducing potential sources of inconsistency during system evolution.

Table 2 shows the elicited system invariants. Event correctness require that events respect the machine invariants. Machine variables must satisfy both invariants and axioms.

## 4. Abstract Machine and First Machine Refinement

The following two invariants encode the first invariants in Table 2, where USER and CONTENT are two carrier sets.

* @inv1 user ⊆ USER

* @inv2 content ⊆ CONTENT

Invariant 3 in Table 2 defines **chat** as a relation between users. Invariant 4 is satisfied by constraining **chat** to be a binary relation. Invariant 5 is enforced by modelling **chat** as a set, thereby ensuring that no pair of users participating in a chat session is duplicated.

* @inv3 chat ∈ user ↔ user // chat sessions
<table><caption>Table 2: system invariants</caption><thead><tr><td>#</td><td>Invariants</td></tr></thead><tbody><tr><td>1</td><td>Users have unique identifiers across the system.</td></tr><tr><td>2</td><td>Content has a unique identifier across the system.</td></tr><tr><td>3</td><td>Chat sessions have unique identifiers across the system.</td></tr><tr><td>4</td><td>A chat session involves exactly two users.</td></tr><tr><td>5</td><td>There can be at most one chat session between two users.</td></tr><tr><td>6</td><td>A chat session between two users may include content accessible to one or both.</td></tr><tr><td>7</td><td>Content is linked to a chat session only if one user has sent it to the other.</td></tr><tr><td>8</td><td>Active and muted are disjoint: a system can never reach a state where user A has muted user B while either is actively chatting with the other.</td></tr><tr><td>9</td><td>Chat sessions may not be symmetric: if user A creates a session to chat with user B, B may not have a session to chat with A.</td></tr><tr><td>10</td><td>Active chat sessions may not be symmetric: if A is actively chatting with B, B may not be actively chatting with A.</td></tr><tr><td>11</td><td>Chat content never exists for a user pair without a chat session.</td></tr><tr><td>12</td><td>Several chat sessions can be created, but at most one may be active per user at any given time.</td></tr><tr><td>13</td><td>Chatting with a muted user is impossible: no content can be exchanged.</td></tr></tbody></table>

Enforcing invariants 6 and 7 in Table 2 requires a more nuanced analysis as they relate chat content, the sender, and the receiver (or recipients). We define **chatcontent** as a partial function with domain **user** (the person who sends the message) and range **content** $\to \mathbb{P}(\mathbf{user})$, where **content** represents the sent content, and $\mathbb{P}(\mathbf{user})$ denotes the set of recipients. Since **chatcontent** is a partial function, a user may exist who has not chatted with anyone. Likewise, its range being a partial function implies that content may exist outside a chat, meaning it is not part of the set of exchanged messages.

Since **chatcontent** and its range are functions, the set of users to whom user **u1** has sent some content **c** is uniquely represented as $\mathit{chatcontent}(\mathbf{u1})(\mathbf{c})$, provided that **u1** is in the domain of **chatcontent** and **c** is in the domain of $\mathit{chatcontent}(\mathbf{u1})$. We represent the set of users with whom **u1** has chatted as
ranchatcontent(u1)), and the set of content items sent by u1 (to anyone) by dom(`chatcontent(u1)`)).

$$ \texttt{@inv4 chatcontent \in user \rightarrow (content \rightarrow \mathbb{P}(user))} $$

Next, we proceed to encode invariant 8 in Table 2: “active and muted chats are disjoint”. We encode **active** as partial function, hence, a user has zero or one active session (see **@inv5**). Invariant **@inv7** states that all muted sessions and their content are valid. We encode invariant 8 as **@inv8**.

$$ \texttt{@inv5 active \in user \rightarrow user // active chat session} $$

$$ \texttt{@inv6 muted \in user \leftrightarrow user // muted sessions} $$

$$ \texttt{@inv7 active \subseteq chat \land muted \subseteq chat} $$

$$ \texttt{@inv8 muted \cap active = \emptyset} $$

Invariants 9 and 10 in Table 2 state that chat and active sessions are not necessarily symmetric, for which no additional invariant is introduced. Invariant **@inv11** enforces invariant 11 in the same table. Expression `chat[{u}]` returns the set of users with whom user u is chatting.

$$ \texttt{@inv11 \forall u,c,s \cdot u \in user \land c \in content \Rightarrow (u \mapsto c \mapsto s \in chatcontent \Rightarrow s \subseteq chat[{u}])} $$

Invariant 12 is enforced by the fact that **active** is a function (see **@inv5**). Until now, we have shown invariants 1 to 6 as they are defined in the abstract machine, and invariants 7 to 12 as they appear in the first machine refinement (see Table 1). Additionally, the first machine refinement introduces variable **toread** to represent content that has been sent but not yet read by the recipient.

$$ \texttt{@inv11 toread \in user \leftrightarrow user} $$

$$ \texttt{@inv12 toread \subseteq chat} $$

We have so far presented only the definitions for the static part of the abstract machine. The definitions for the dynamic part are accomplished through the use of events. The remainder of this section presents the *extended* versions of the events, as obtained through the *horizontal* refinement of the abstract machine. The event `create-chat-session` implements US-01 by creating a chat session that allows user `u1` to communicate with user `u2`. Guard `@grd2` encodes the **Given** condition of US-01, aiding Rodin in infer-
ring the types of u1 and u2. Action @act1 adds the pair u1 $\mapsto$ u2 to the set of existing chats, while @act2 ensures that the content associated with the chat session between u1 and u2 starts empty. Notably, this event does not create a corresponding chat session for u2 to initiate communication with u1.

We implement US-02 as event **select-chat**. By using relational overriding operator $\oplus$ instead of the set union operator $\cup$, action @act1 enforces u1 to have at most one active chat session. Furthermore, @grd4 implements a *defensive* style of programming. Guard @grd3 ensures that a muted chat session is never active. While guard @grd2 implements the first **Given** condition in US-02, guard @grd4 implements the second one. Action @act1 uses the overriding operator $\oplus$ instead of the union operator $\cup$ to enforce invariant @inv5 and thus function **active** remains a function. Had u1 $\mapsto$ u2 been added to **active** using the union operator $\cup$, the function **active** would have mapped u1 to two distinct users, violating its functional property. Such an inconsistency would have been detected by Rodin, resulting in an unprovable proof obligation.

event create-chat-session // US-01
any u1 u2
where
@grd1 u1 \in user \land u2 \in user @grd2 u1 $\mapsto$ u2 $\notin$ chat
then
@act1 chat := chat $\cup$ {u1 $\mapsto$ u2}
@act2 active(u1) := u2

end

event select-chat // US-02
any u1 u2
where
@grd1 u1 \in user \land u2 \in user @grd2 u1 $\mapsto$ u2 $\in$ chat
@grd3 u1 $\mapsto$ u2 $\notin$ muted @grd4 u1 $\mapsto$ u2 $\notin$ active
then
@actr11 active := active $\oplus$ {u1 $\mapsto$ u2}
@actr12 toread := toread $\setminus$ {u1 $\mapsto$ u2}
end

US-03 is modelled as event **chatting**, therefore, user u1 sends content c to user u2. Guard @grd2 implements the **Given** condition and enforces that c is a fresh content. Action @act1 adds c to the set of contents. Action
The event mute-chat encodes US-06. It mutes the chat session between u1 and u2. Specifically, action @act1 adds the pair u1$\to$u2 to the set of muted chats. Action @act2 prevents a muted chat from being active. Alternatively, we could have added a guard @grd4 u1 $\mapsto$ u2 $\notin$ active, but this would not reflect the typical behaviour of a chat system in which a user u1 can mute u2 while actively chatting with them.

event mute-chat // US-06
any u1 u2
where
@grd1 u1∈user ∧ u2∈user @grd2 u1 $\mapsto$ u2 ∈ chat
@grd3 u1 $\mapsto$ u2 $\notin$ muted
then
@act1 muted := muted ∪ {u1$\mapsto$u2}
@act2 active := active \ {u1$\mapsto$u2}
end

The event unmute-chat implements US-07. It unmutes the chat between u1 and u2. Guard @grd3 ensures that only u1 (who originally muted u2) can unmute u2. Since muted is a function, u2 is unique. Guard @grd2 is redundant, as it can be inferred from @grd3 and the fact that muted is a subset of chat.

event unmute-chat // US-07
any u1 u2
where
@grd1 u1∈user ∧ u2∈user @grd2 u1 $\mapsto$ u2 ∈ chat
@grd3 u1 $\mapsto$ u2 ∈ muted
then
@act1 muted := muted \ {u1$\mapsto$u2}
end

We implement US-09 as the event forward, whereby user u forwards content c to a set of users us. Guards @grd1, @grd2 and @grd5 enforce the type for u and us. Guard @grd4 sets a type for c. Guard @grd6 ensures that u has chat sessions with every element of us. The expression `muted[{u}]` ∩ us = Ø verifies that no member of us is in the set of users that u has muted. Similarly, the expression `muted[us] ∩ {u}= Ø` ensures that u has not
been muted by any member of us. Action @act2 creates individual chat sessions for each member of us to communicate with u. Action @act1 overrides **chatcontent** to include content c into the chat sessions between u and each element of us. Notably, event **forward** does not define an ordering among the content items in a chat session, hence, at this abstract level, we cannot predict the sequence in which chat content is read.

We have implemented US-08 as the event **broadcast** in a similar way to event **forward**. The major difference is that guard @grd6 for event **forward** is not included in event **broadcast**.

event forward // US-09
any u us c
where
@grd1 u ∈ user @grd2 us ⊆ user
@grd3 muted[{u}] ∩ us = ∅ ∧ muted[us] ∩ {u} = ∅
@grd4 c ∈ content @grd5 u ∈ domchatcontent)
@grd6 us ⊆ chat[{u}]
then
@act1 chatcontent := chatcontent ⊕ {u ↦ (chatcontent(u) ∪ {c ↦ us})}
@act2 chat := chat ∪ (us × {u})
@act3 toread := toread ∪ ((us × {u}) \ active)
end

Event **unselect-chat** implements US-10. It unselects the chat session between **u1** and **u2** by dropping **u1** ↦ **u2** from **active**.

event unselect-chat // US-10
any u1 u2
where
@grd1 u1∈user ∧ u2∈user @grd2 u1 ↦ u2 ∈ chat
@grd3 u1 ↦ u2 ∈ active
then
@act1 active := active \ {u1→u2}
end

## 4.1. Discussion on design choices

The activation of the mapping $a1 \mapsto a2$ within the system state establishes a new chat session between users **a1** and **a2**. As the Rodin platform automaton-
ically discharges the proof obligations associated with the create-chat-session event, the correctness of this event with respect to the invariants specified in the abstract machine is ensured.

**Chatting.** Chat content may be added to both u1, u2 and u2, u1 sessions. If the content is added for both users, the second line of @act3 in event chatting, Page 13, should be extended with a u2 $\mapsto$ (chatcontent(u2) $\cup$ {c $\mapsto$ {u1}}) expression to ensure that c is visible not only to u1 but also to u2. Taking this approach however will generate an unprovable proof obligation stating that u2 must be in the domain of chatcontent for chatcontent(u2) to be well-typed. This issue can be resolved by adding an event guard @grd6 u2 $\in$ dom chatcontent to event chatting. However, @grd6 would not hold the first time, particularly when u2 has not yet sent any content to anyone (not just to u1). We can then extend the add-content event (not shown) with an action "$@act2 chatcontent(u) := content \times \{\emptyset\}$$" that creates default content associations with the $\emptyset$ for each user. However, if a code generator were to generate code directly from there, it would incur a computationally expensive task. This type of analysis is not particularly complex and can be conducted through code inspection. However, writing the formal specification in EVENT-B allows us to leverage Rodin to formally verify if the extended code is correct w.r.t the system invariants.

We could redefine action @act3 of event chatting as below. However, this solution is incorrect as the last $\oplus$ expression *forgets* about the chat-content(u2). This issue is not spotted by Rodin since it generates proof obligations that are provable and discharged automatically. This can only be spotted by a domain expert who understands the intended behaviour.

$$ \begin{aligned} \texttt{@act3 chatcontent} &:= \texttt{chatcontent} \\ &\quad \oplus \{u1 \mapsto (\texttt{chatcontent(u1)} \cup \{c \mapsto \{u2\}\}) \\ &\quad \oplus \{u2 \mapsto \{c \mapsto \{u1\}\}\} \end{aligned} $$

Another option regarding action @act3 is to use a comprehension set expression to convey the new value of chatcontent(u2) as indicated in the last overriding $\oplus$ expression below. The drawback of this alternative is that this set expression is not directly encoded using sets or relations, as oftentimes leveraged by code generators [14, 13].
$$
\begin{align*}
@act3 \quad \mathit{chatcontent} &:= \mathit{chatcontent} \\
&\qquad \oplus \{u1 \mapsto (\mathit{chatcontent}(u1) \cup \{c \mapsto \{u2\}\})\} \\
&\qquad \oplus \{cc,s \cdot u2 \mapsto \{cc \mapsto s\} \in \mathit{chatcontent} \lor (cc=c \land s=\{u1\}) \\
&\qquad \qquad \mid u2 \mapsto \{cc \mapsto s\}\}
\end{align*}
$$

**Deleting content.** Deleting content is one of the subtlest functionalities as executing it can potentially violate invariants throughout the system. If we add “@act2 content := content \ {c}” to event delete-content in Page 13, Rodin will generate an unprovable proof obligation. The proof obligation relates to @inv4 in Page 11 and states that for each user u different from u1, the range of chatcontent(u) is a partial function from content\{c} to P(user), which is not possible because u may have forwarded or broadcasted c to another user previously. Alternatively, we can represent content as below. However, computing the value of chatcontent this way requires traversing user twice and content once, which could be time-consuming depending on the type of structures used to store chatcontent or to encode sets in general.

$$
@act2 \quad \mathit{content} := \{cc,a,b,s \cdot a \in \mathit{dom}(\mathit{chatcontent}) \wedge \\
\phantom{@act2 \quad \mathit{content} := \{cc,a,b,s \cdot a \in } cc \mapsto s \in \mathit{chatcontent}(a) \wedge b \in s \wedge \neg(a=u1 \wedge b=u2 \wedge cc=c) \mid cc\}
$$

**Forwarding content.** Event forward in Page 15 extends chatcontent with triplets $u \mapsto \{c \mapsto u2\}$, for every $u2 \in \mathit{us}$. If we wanted to further extend chatcontent with triplets $u2 \mapsto \{c \mapsto u\}$, we would need to add a second overriding expression as shown below. As a result, the whole expression would need to be refined before it can be translated into a programming language such as Java, Python, C, or others.

$$
\begin{align*}
\mathit{chatcontent} &:= \mathit{chatcontent} \\
\oplus \{u &\mapsto (\mathit{chatcontent}(u) \cup \{c \mapsto \mathit{us}\})\} \\
\oplus \{u2, \mathit{cc}, s &\cdot (u2 \mapsto \{\mathit{cc} \mapsto s\} \in \mathit{chatcontent}) \lor \\
&\phantom{\oplus \{u2, \mathit{cc}, s \cdot (u2 \mapsto \{\mathit{cc} \mapsto s\} \in \mathit{chatcontent}) \lor} (\mathit{cc}=c \land \mathit{s}=\{u\} \land u2 \in \mathit{us}) \\
&\qquad \mid u2 \mapsto \{\mathit{cc} \mapsto s\}\}
\end{align*}
$$

**Muting a chat.** Regardless of the question of how correct a specification is, one should also decide whether to use a *defensive* or *offensive* style of specification and foresee the effect of that style on the rest of our model. A defensive event specification does not make (or make fewer) requirements on the environment. An offensive event specification strengthens event guards.
Event **mute-chat** encodes a defensive style of programming whereby only unmuted chats can then be muted. If the chat **u1** ↦ **u2** is already muted, then event **mute-chat** does not execute. However, if we were to execute @act1 on a muted chat, the state variable **muted** would remain unchanged, as sets do not allow duplicate elements (see @act1).

## 5. Data Refinement

The functionality of a machine can be extended through a machine refinement. Our goal is to refine the EVENT-B model in a way that facilitates the task of code generators [13, 5, 17]. We use Rodin to develop the EVENT-B model of the chat system. The Rodin IDE automatically integrates abstract machine components into the internal representation of a refinement machine. For instance, the refinement of the **initialisation** event includes machine variable initialisations as carried by the abstract **initialisation** event. Additionally, guards and actions in a refinement event (defined using the **ex-tends** keyword) are implicitly combined with those defined in the abstract event. Moreover, *gluing invariants* ensure consistency by relating abstract machine variables with their corresponding concrete counterparts.

So far, we have represented content and users using sets. In the second machine refinement, we leverage data refinement by transforming these sets into sequences. A sequence of natural numbers, denoted as **a..b**, represents the natural numbers from **a** to **b**, inclusive.

$$a..b = \{x \mid x \in \mathbb{N} \wedge a \le x \wedge x \le b\}$$

We can hence use the **1..n** notation to model a sequence of type **T** and size **n** as a total function from **1..n** to **T**. By defining **sequence** as a total function, we ensure that it has no gaps in its domain.

$$@inv sequence \in 1..n \rightarrow T$$

However, in the definition of **sequence**, deleting an element **k** from the domain **1..n** requires shifting all subsequent elements one position to the left. To achieve this, we define a second sequence, **sequence2**, derived from **sequence** by taking the first **k-1** elements and appending the elements from **k+1** onwards, but repositioned starting at index **k**. This shifting approach could be used in the definition of a **delete-content** event that will ultimately
remove the content from both users' screens.

$$ 
\begin{aligned}
\mathit{sequence2} = (1..k-1) \triangleleft \mathit{sequence1} \cup \\
\{i, t \cdot i \mapsto t \in \mathit{sequence1} \wedge i>k \mid (i-1) \mapsto t\}
\end{aligned}
$$

The following gluing invariants relate `userSeq` with `user` in the abstract machine. Since `userSeq` is surjective, no abstract `user` is discarded.

$$ @invr21 \mathit{usersize} \ge 0 $$

$$ @invr22 \mathit{userSeq} \in (1..\mathit{usersize}) \rightarrow \mathit{user} $$

$$ @invr23 \mathit{user} = \{n, u \cdot n \mapsto u \in \mathit{userSeq} \mid u\} $$

Variable contents encodes content as a sequence, where `csize` is the number of elements it contains. The variable content is the type of contents. The domain of contents is `1..csize`; therefore, when `csize` is 0, contents is empty. The invariants `@invr22` and `@invr23` together form a gluing invariant that relates contents with content.

$$ @invr21 \mathit{csize} \ge 0 $$

$$ @invr22 \mathit{contents} \in (1..\mathit{csize}) \rightarrow \mathit{content} $$

$$ @invr23 \mathit{content} = \{n, c \cdot n \mapsto c \in \mathit{contents} \mid c\} $$

Next, variable `chatcontent` is refined as the variable `screen`, which organises sent content sequentially. The variable `screen` is used to display exchanged content in order.

$$ @invr24 \mathit{screen} \in \mathit{user} \rightarrow (\mathit{user} \rightarrow \mathbb{P}(\mathit{contents})) $$

Next, we present the **chatting** event refinement, where `k1` is the position at which content `c` is placed on `u1`'s screen<fnref n="1" />. To ensure that `u1`'s chat content is displayed in order, `k1` must always be greater than any value in `dom/screen(u1)(u2)` when the event **chatting** executes. Similarly, `k2` represents the position of content item `c` on `u2`'s chat screen with `u1`. Guards `@grdr21` and `@grdr22` enforce invariant `@invr24`, ensuring that `screen` remains a function. Action `@actr23` maps position `csize+1` to content `c`, while action `@actr21` maps position `k1` on `u1`'s chat screen to `c` and position `k2` on `u2`'s chat screen to `c`.

<footnote n="1">¹We have omitted the event guards for clarity and conciseness of presentation.</footnote>
event chatting extends chatting // US-03

any k1 k2

then

@actr21 screen := screen ⊕
{u1 ↦ (screen(u1) ⊕ {u2 ↦ (screen(u1)(u2) ⊕ {k1 ↦ c}))},
u2 ↦ (screen(u2) ⊕ {u1 ↦ (screen(u2)(u1) ⊕ {k2 ↦ c}))}

@actr22 csize := csize+1

@actr23 contents := contents ⊕ {(csize+1) ↦ c}

end

## 6. Discussions on Modelling Practices

The development of the chat system surfaced a set of modelling practices that are applicable beyond the scope of this case study. These observations provide insights on the effective modelling of message exchange systems.

**State consistency is crucial.** An invariant of a model is a predicate that is true of all reachable states. Ensuring that machine invariants are correctly written and preserved by events is paramount for maintaining system correctness. The proper definition of (partial or total) functions can prove to be a challenge in the presence of events that delete content. Events for forwarding or broadcasting content pose additional challenges, as the intended behaviour usually aligns more closely with set-comprehension expressions, which are not necessarily linked to code implementations or code generators. Forwarding and broadcasting further require invariants to be checked over sets rather than single elements, placing a significantly heavier load on Rodin's proof engines.

**Guard design reduces errors.** Careful defensive event modelling, including the extensive use of event guards to enforce invariants, proved essential to preserving system consistency. Our design explicitly distinguished between defensive guard design for initial chat interactions and for subsequent messaging between existing chat users, producing a refinement of chat content into sequences.

**Set comprehension limits practicality.** Although abstract specifications favour sets and relations for simplicity, delving into implementation-oriented data structures such as sequences is necessary for practical future
code generation. Set comprehension is expressive and useful for abstract specifications but is poorly supported in code generation [14]. Recognising and refining away such constructs is important when targeting code generation and executable systems.

**Proof obligations alone are insufficient.** While Rodin's proof engines automate and discharge many proof obligations for correctness checks, human reasoning about domain-specific properties remains indispensable. Some errors, such as misinterpreting deletion effects, cannot be automated with a prover, although they can potentially be detected with model checkers.

**Efficiency and simplicity trade-offs are inevitable.** Modelling choices often involve a trade-off between model simplicity and runtime efficiency. For example, certain broadcast mechanisms could be modelled more simply with the use of set comprehension expressions but might lead to inefficient implementations if not refined further.

## 7. Statistics of the Chat System

<table><caption>Table 3: Chat System Model Statistics</caption><thead><tr><td>machine</td><td>#POs</td><td># automated</td><td>manual</td><td>%</td></tr></thead><tbody><tr><td>abstract</td><td>23</td><td>23</td><td>0</td><td>100%</td></tr><tr><td>refinement 1</td><td>54</td><td>54</td><td>0</td><td>100%</td></tr><tr><td>refinement 2</td><td>34</td><td>28</td><td>6</td><td>82%</td></tr></tbody></table>

Table 3 shows statistics on the number of proof obligations (POs) generated by the Rodin platform, the number and percentage of POs discharged automatically, and the number of POs requiring human intervention. In general, the more concrete the machine becomes, the lower the percentage of POs that are discharged automatically by Rodin's proof engines. This is due to the fact that refinement POs for refinement machines carry over definitions and invariants from the abstract machines. For the second refinement machine, the proof obligations that are not discharged automatically are primarily related to the definition of the variable *screen*, which requires both its domain and codomain to be partial functions.

The results show that all the POs were discharged automatically in the abstract and the first refinement machines, indicating a strong correlation between definition of invariants, defensive style of modelling, and Rodin proof
force. The decrease in automation in the second refinement arises primarily
from the complexity introduced by the **screen** variable, which requires func-
tion updates across multiple dimensions. These findings confirm that a CbC
approach remains tractable at moderate refinement depths, while also high-
lighting areas where automated tooling could be enhanced, particularly for
nested data refinements and sequence-based structures.

8. Related Work

A recent study [16] presents the formal modelling and refinement of a Content-Based Publish/Subscribe (CBPS) communication system with EVENT-B. Their work focuses on service-to-service communication within an Internet of Things (IoT) context, emphasising the decentralised management of dynamic communication patterns and the formal verification of message delivery. Although their target application is different (communication between IoT services rather than user-driven messaging), their modelling of dynamic message flows, event-driven interactions, and consistency preservation in a decentralised environment aligns with the challenges addressed in our chat system formalisation. Whereas they further verify a liveness property using the Prob [12] model checker, we only considered safety properties.

Fakhfakh et al. [9] formally specify and verify a broadcasting protocol using EVENT-B, focusing on reliable message delivery across network nodes. Their work addresses challenges of dynamic communication and state consistency, similar to our chat system formalisation. However, while their focus is protocol-level broadcasting, our work models interactive user-driven messaging with additional features such as forwarding and read-status tracking.

Benyagoub et al. [4] model scalable conversation protocols in distributed
systems using Event-B, representing peers as state-transition systems com-
municating via messages. While their focus is on general communication
protocols, our work targets user-driven chat systems, applying similar prin-
ciples to ensure Correctness-by-Construction for features like user creation,
messaging, and deletion.

El Mimouni et al. [8] formally modelled the Simple Text Oriented Mes-
saging Protocol (STOMP) in EVENT-B, focusing on client-server communi-
cation and protocol compliance. Although their work targets protocol-level
interactions rather than user-driven messaging, it similarly highlights the
challenges of modelling event-driven communication systems.
A formal analysis of the Signal protocol is presented in [6], using Logic of
Events theory to verify confidentiality and authentication guarantees. While
Signal also addresses dynamic messaging, our modelling focuses instead on
the correctness-by-construction of core chat functionalities such as user cre-
ation, message sending, forwarding, and deletion, without considering secu-
rity or liveness properties.

Saraswat et al. [15] formalise and verify a checkpointing algorithm for dis-
tributed systems using Event-B, focusing on message broadcasting to main-
tain global consistency. While their work targets system-level coordination,
ours applies similar modelling techniques to user-interactive chat systems,
addressing dynamic state management and event-driven behaviours.

9. Conclusion

This work presented the formal modelling and refinement of a chat sys-
tem using EVENT-B. We discussed design modelling decisions and how they
affect the capture of dynamic behaviours of interactive systems. Through
the formalisation of the chat system, several modelling patterns emerged
that are applicable beyond this case study. User Stories were systematically
translated into EVENT-B events using a structured syntax-based approach:
acceptance criteria guided the definition of event guards and actions, ensuring
close alignment between informal requirements (the User Stories) and formal
modelling in EVENT-B. The use of refinement techniques with EVENT-B al-
lows statically defined structures such as chat content to dynamically evolve
through the use of *gluing invariants*.

Our contributions are three-fold: (i.) a structured approach for systemat-
ically translating informal User Stories into formal EVENT-B models; (ii.) a
set of practical design choices, such as state consistency enforcement, guard
strengthening, and the trade-offs between model simplicity and implementa-
tion; and (iii.) empirical statistics on proof obligation discharge, highlighting
the relation between model abstraction level and proof automation.

Several functionalities commonly found in modern messaging applica-
tions were intentionally omitted to concentrate on the essential dynamic
behaviours: (i.) Archiving chats, that is, backing up a chat, making it in-
active, and hiding it from a user. (ii.) Pinning a chat. This is more of an
interface-related functionality, consisting in moving a chat up in the list of
existing chats so that the user does not need to scroll down to search for
that chat in her chat list. (iii.) Contact lists. Chats can only be created out
of a local contact list. (iv.) Copying a message or content. The message or
content can be pasted thereafter. (v.) Time stamps. Users can check the
time a message was sent or received. (vi.) Group of users. Users can create
groups. These groups can be used for chatting, phone calls, or video confer-
ences. (vii.) Phone calls and video conferences. Users can place phone calls
or make video conferences to a person or a group of people.

References

[1] Jean-Raymond Abrial. *Modeling in Event-B: System and Software Design*. Cambridge University Press, New York, NY, USA, 2010.

[2] Jean-Raymond Abrial and Stefan Hallerstede. Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. *Fundam. Inf.*, 77(1-2):1-28, 2007. ISSN 0169-2968.

[3] Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. *Software Tools for Technology Transfer*, 12(6):447-466, 2010.

[4] Sarah Benyagoub, Yamine Aït Ameur, Meriem Ouederni, Atif Mashkoor, and Ahmed Medeghri. Formal design of scalable conversation protocols using event-b: Validation, experiments, and benchmarks. *Journal of Software: Evolution and Process*, 32(2), 2020.

[5] Néstor Cataño and Víctor Rivera. EventB2Java: A Code Generator for Event-B. In *Nasa Formal Methods (NFM)*, volume 9690 of *LNCS*, pages 166-171, Minneapolis, MN, USA, June 7-9 2016. Springer.

[6] Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, and Douglas Stebila. A Formal Security Analysis of the Signal Messaging Protocol. *J. Cryptol.*, 33(4):1914-1983, 2020.

[7] Andrew Edmunds and Michael Butler. Tool Support for Event-B Code Generation. In *Workshop on Tool Building in Formal Methods*, Québec, Canada, 2010. J. Wiley and Sons.

[8] Sanae El Mimouni and Mohamed Bouhdadi. Formal modeling of the Simple Text Oriented Messaging Protocol using Event-B method. In
2015 IEEE/ACS 12th International Conference of Computer Systems and Applications (AICCSA), pages 1-4, 2015.

[9] Faten Fakhfakh, Mohamed Tounsi, and Mohamed Mosbah. Formal specification and Verification of a Broadcasting Protocol: a Refinement-Based Approach. Procedia Computer Science, 176:2858-2867, 2020.

[10] Anthony Hall. Correctness by Construction: Integrating Formality into a Commercial Development Process. In Lars-Henrik Eriksson and Peter Alexander Lindsay, editors, *FME 2002:Formal Methods—Getting IT Right*, pages 224–233, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.

[11] Anthony Hall and Roderick Chapman. Correctness by Construction: Developing a Commercial Secure System. *IEEE Software*, 19(1):18–25, January 2002.

[12] Michael Leuchel and Michael Butler. ProB: A Model Checker for B. In *FME 2003: Formal Methods*, Lecture Notes in Computer Science, Pisa, Italy, 2003. Springer-Verlag.

[13] Dominique Méry and Neeraj Kumar Singh. Automatic code generation from Event-B models. In *Proceedings of the Second Symposium on Information and Communication Technology*, SoICT. ACM, 2011.

[14] Víctor Rivera, Néstor Cataño, Tim Wahls, and Camilo Rueda. Code Generation for Event-B. STTT, 19(1):31–52, 2017.

[15] Bal Krishna Saraswat, Raghuraj Suryavanshi, and Divakar Yadav. Formal Specification & Verification of Checkpoint Algorithm for Distributed Systems using Event-B. *International Journal of Engineering Trends and Technology (IJETT)*, 69(4):1–9, 2021.

[16] Sarah Hussein Toman, Aida Lahouij, Sonia Kotel, Lazhar Hamel,ZNah Hussein Toman, and Mohamed Graiet. Service to Service Communication based on CBPS system: Refinement and Verification. *Soft Computing*, 28(19):10943–10963, 2024.

[17] Steve Wright. Automatic Generation of C from Event-B. In *Workshop on Integration of Model-based Formal Methods and Tools*, Nantes, France, 2009. Springer-Verlag.