11institutetext: LIPN, Université Sorbonne Paris Nord, Villetaneuse, France
22institutetext: Pontificia Universidad Javeriana, Cali, Colombia.

# A Rewriting Logic Semantics and Statistical Analysis for Probabilistic
Event-B

Carlos Olarte 11 Camilo Rocha 22 Daniel Osorio 22

###### Abstract

Probabilistic specifications are fast gaining ground as a tool for statistical
modeling of probabilistic systems. One of the main goals of formal methods in
this domain is to ensure that specific behavior is present or absent in the
system, up to a certain confidence threshold, regardless of the way it
operates amid uncertain information. This paper presents a rewriting logic
semantics for a probabilistic extension of Event-B, a proof-based formal
method for discrete systems modeling. The proposed semantics adequately
captures the three sources of probabilistic behavior, namely, probabilistic
assignments, parameters, and concurrency. Hence, simulation and probabilistic
temporal verification become automatically available for probabilistic Event-B
models. The approach takes as input a probabilistic Event-B specification, and
outputs a probabilistic rewrite theory that is fully executable in PMaude and
can be statistically tested against quantitative metrics. The approach is
illustrated with examples in the paper.

###### Keywords:

Probabilistic Event-B Statistical model checking PVeStA

##  1 Introduction

For many systems, there is an obvious need for using specialized formal
methods in the spirit of formalisms, inference systems, and simulation
techniques for selected tasks. When properly combined, formal methods have a
great potential to become more useful in practice, and scale up because of
modularization and specialization of needs. In the realm of probabilistic
systems, where a vast number of randomized algorithms and protocols fall, both
inference- and algorithmic-based analysis techniques are needed to answer the
key question of whether such systems are correct. Probabilistic systems must
behave properly, up to a confidence threshold, regardless of the way they
operate amid uncertain information. A challenging task is to find combinations
of formalisms, inference systems, and simulation techniques for verifying such
systems.

This paper focuses on probabilistic simulation and statistical analysis for a
probabilistic extension of Event-B [1], a formal method for system-level
modeling and analysis. Event-B uses set theory as a modeling notation,
refinement to represent systems at different abstraction levels, and
mathematical proofs to verify consistency between refinement levels (and other
proof obligations). The probabilistic extension of Event-B proposed by [6] is
based on three mechanisms. First, interaction with the external environment is
governed by a probabilistic choice; that is, external inputs are chosen
uniformly from finite sets representing the potential values for the variables
under the control of the external environment. Second, the extension includes
probabilistic assignment to variables (representing the state of the system)
by uniform choice from finite sets. This is useful to handle the uncertainty
associated to “external” data. Third, all concurrent transitions in a system
are probabilistic. That is, in the presence of the two first mechanisms,
concurrency yields a probabilistic transition system where each possible
transition from a state is weighted by a probability measure. The authors of
[8] have proposed an inference system for reasoning within this probabilistic
extension of Event-B. The purpose of the presented paper is to complement the
work in [8] by enabling algorithmic simulation and statistical model checking.

This paper develops a rewriting logic semantics for the above-mentioned
probabilistic extension of Event-B. It takes as input a probabilistic Event-B
model and outputs a probabilistic rewrite theory [4]. The mapping implementing
this translation is explained in detail, including its soundness and
completeness properties for simulation in relation to the given model. The
resulting probabilistic specification is executable in Maude [11] and it is
amenable to simulation-based verification such as, e.g., statistical model
checking with help of the PVeStA model checker tool [5]. The translation has
been fully automated and it supports a wide range of Event-B operators.

The approach presented here can be seen as a complement to the proof-theoretic
techniques developed in [8]. It allows system designers to experiment with the
system via simulation and automatically verify system’s properties via
(stochastic) model checking, thus gaining more confidence on the model before
embarking on a proving task. It is known that Event-B offers both proof-
theoretic methods, and simulation and model checking tools (via, e.g., the
ProB animator and model checker in the Rodin platform [1, 14]) for system
modeling. These latter features do not exist, to the best of the authors’
knowledge, for probabilistic Event-B models. Ultimately, the developments
presented here open new opportunities for incarnating the more ambitious long-
term ideal of combining formalisms, inference systems, and simulation
techniques for verifying probabilistic systems.

Outline. Section 2 presents an overview of the probabilistic extension of
Event-B. Section 3 develops the mapping from Event-B models to probabilistic
rewrite theories and studies its main formal properties. Section 4 showcases
an example of the transformation and its statistical analysis. The web page of
the companion tool [17] of this paper presents other case studies and provides
some experimental results. Finally, Section 5 concludes the paper.

##  2 Probabilistic Event-B in a Nutshell

This section presents an overview of the probabilistic extension of Event-B
proposed by [8]. As it is the case for the non-probabilistic case, a
probabilistic Event-B model consists of a _context_ (§2.1) and a _machine_
(§2.2).

###  2.1 Contexts

A context in Event-B describes the constant part of the system, including the
definition of deferred sets and constants. More precisely, a context is a
triple $\mathcal{C}=\langle SET_{l}\cup SET_{n},CTE\rangle$ where $SET_{l}$ is
a set of set declarations of the form $S:\\{id_{1},...,id_{m}\\}$, $SET_{n}$
is a collection of set declarations of the form $S:n$ (where $n$ is a natural
number), and $CTE$ is a set of constant definitions of the form
$c~{}:~{}type~{}:=~{}v$.

Deferred sets. A typical context can define any number of deferred sets, and
axioms indicating either that any such a set is finite (but its cardinality is
unknown) or has a fixed cardinality $n$. The former construction is not
considered here, while the latter is supported via the $SET_{n}$ component.
For instance, the declaration ENUM:3 generates three constant symbols (e.g.,
ENUM$i$, for $1\leq i\leq 3$) that inhabit the set ENUM. Moreover, the
deferred set declaration STATE:{open,close} defines the set STATE inhabited
exactly by the two (distinct) constant symbols open and close.

Types, values, and constants. The syntax DEFAULT:STATE :=open defines the
constant DEFAULT of type STATE with value open. Basic types include deferred
sets, Boolean values, and integer numbers. Types can be also built via
Cartesian products (A * B) and powersets (POW(A)). From those constructions,
relations and (partial, total, injective, etc.) functions can be defined as
expected. For instance, the set-theoretic language of Event-B reduces $r\in
A\mathbin{\leftrightarrow}B$ ($r$ is a relation from $A$ to $B$) into
$r\subseteq A\texttt{*}B$ and finally into $r\in\texttt{POW}(A\texttt{*}B)$.
For succinctness, $A$ and $B$ in $A\texttt{*}B$ are restricted here to be
basic types.

According to the types above, the values for constants can be elements of a
deferred set, numbers, Booleans, pairs ($a\mapsto b$), set of values as in
$\\{a,b,c\\}$, or integer intervals as in $1..42$. The complete grammar can be
found in [17].

⬇

CONTEXT GEAR_CTX

SETS

SUD:{ up, down }

SER:{ extended, retracted }

SOC:{ open, close }

CONSTANTS

FCMD : Nat := 9

END

As a running example, consider the controller for a landing gear system
modeled in Event-B in [9] and probabilized in [6]. When landing, the following
sequence of actions occur: the doors of the system are opened, the landing
gears are extended, and then the doors are closed. Similarly, after taking
off, the doors are opened, the gears retracted, and the doors are closed. The
pilot may initiate and interrupt these sequences with a handle that can be in
two positions: _up_ (executing the retracting sequence) and _down_ (extending
sequence). The context GEAR_CTX defines the three needed deferred sets and a
constant of type Nat that will be used in the next section.

###  2.2 Machines

A machine in Event-B specifies a set of variables, defining the state of the
system, and the system’s actions, called _events_. More precisely, a machine
is a structure of the form
$\mathcal{M}=\langle\mathcal{C},\vec{x},I,\mathcal{E},init\rangle$ where
$\mathcal{C}$ is a context, $\vec{x}$ is a set of variables typed by the
invariant $I$, $\mathcal{E}$ is a set of probabilistic events, and init is the
initialization event.

State of the machine.  In an Event-B specification, the section SEES of a
machine determines the context $\mathcal{C}$ accessible by the model. For
simplicity, it is assumed here that each machine _sees_ exactly one context.
The section VARIABLES contains a list of identifiers. The types (or domains)
for each variable (e.g., currentState:STATE) are defined in the section
INVARIANTS. Besides typing information, Event-B models include also invariant
properties that must be preserved along the system’s transitions. The
translation in Section 3 requires only the types for the variables and hence,
for the moment, only invariants of the form $x:A$ (the type of $x$ is $A$) are
considered. Section 4 shows how the infrastructure presented here can be used
to verify some other properties.

Events. The machine _initialization_ is deterministic and the section
INITIALISATION assigns values (of the appropriate type) to all the variables
(e.g., currentState := open). Such values are built from elements of deferred
sets, constants in the context, standard arithmetic and Boolean operations,
and expressions on sets and relations (see [1, Chapter 6] for the complete
set-theoretic language).

⬇

EVENT ID

WEIGHT W

ANY P

WHERE G

THEN A

END

The system’s actions are defined by _events_ , which are composed of _guards_
and _actions_. In the case of probabilistic models, each event is also
assigned a _weight_. At a given state, the numerical expression W determines
the weight of the event with identifier ID. Such an expression is built from
constants, the machine’s variables, and arithmetic operations. As explained
later in the semantics, events with higher weights are more likely to be
chosen for execution.

The variables declared in the optional section ANY are called _parameters_ ;
they represent an interaction with an external environment, which is not under
the control of the system. Hence, the behavior of the event is not fixed but
it may have different outcomes depending on the values chosen for those
parameters. The expressions $y:\in S$ states that the parameter $y$ may take
values from the non-empty and finite set $S$. The set $S$ can be a an
arbitrary expression returning a set, including for instance: set
comprehension ($\\{x.S\mid P(x)\\}$, elements of $S$ that satisfy the
predicate $P$ and $\\{x.S\mid F(x)\\}$ defining the set $\\{F(x)\mid x\in
S\\}$); the Cartesian product; domain of a relation; range restriction
($r\mathbin{\rhd}S=\\{x\mapsto y\in r\mid y\in S\\}$); domain subtraction
($S\mathbin{\lhd\mkern-14.0mu-}r=\\{x\mapsto y\in r\mid x\notin S\\}$);
overriding
($r\mathbin{\lhd\mkern-9.0mu-}s=s\cup(\mathop{\mathrm{dom}}\nolimits{(s)}\mathbin{\lhd\mkern-14.0mu-}r)$;
etc. The complete list of expressions involving set/relations (union,
membership, range restriction, cardinality, etc.) currently supported by our
tool can be found at [17]. Semantically, in $y:\in S$, a value from $S$ is
chosen with a uniform probability distribution and assigned to the parameter
$y$.

The Boolean expression G in the WHERE section determines whether the event can
be fired at a given state or not. The _action_ of the event determines the new
state and it is specified by a list of simultaneous assignments in the THEN
section. It is assumed that the right hand side (RHS) of an assignment is an
expression of the appropriate type including constants and variables
(considering the values before the assignment), as well as the event’s
parameters. When the RHS is a list of expressions, a uniform probabilistic
distribution is assumed for them. Moreover, it is also possible to use an
enumerated probabilistic assignment as in
$x:=\\{\texttt{open}<EMAIL_ADDRESS>specifying that $x$ may take
the value open (resp., close) with probability $0.7$ (resp., $0.3$).

⬇

MACHINE GEAR SEES GEAR_CTX

VARIABLES handle gear door cmd

INVARIANTS

handle : SUD

gear : SER

door : SOC

cmd : Nat

INITIALISATION

handle := up

cmd := 0

gear := retracted

door := closed

In the running example, the pilot may use the handle to initiate and interrupt
the extending and retracting sequences. The machine GEAR uses three variables
to observe the current state of the handle, the gear, and the doors. The
variable cmd controls the number of times the pilot has initiated the
sequence.

The event extend in Figure 1 models the extension of the gear when the handle
is down and the doors are opened. As a model of failures, there is a $10\%$ of
risk that the gears do not react correctly to their command. The event retract
can be explained similarly. The state of the doors are controlled by the
events open and close. For instance, if the doors are closed, the gear
retracted, and the current command is _extend_ (handle=down), the doors are
opened with probability 0.9.

The interface of the system with the pilot is modeled with the event $pcmd$
below. The requirements of the system impose that: the pilot cannot command
the handle

⬇

EVENT pcmd

WEIGHT

FCMD - cmd

ANY

cc :$\in$ {up, down}

WHERE

cmd <= FCMD

THEN

handle := cc

cmd := cmd + 1

END

more than a fixed number of times before one of the sequences begins; and
consecutive uses of the handle must decrease the priority of using it again.
Since the pilot may interrupt an already started sequence, this event modifies
the state of the handle with equal probability to up and down. Due to the
weight of the event, such changes are allowed only up to FCMD times (the
constant defined in the context GEAR_CTX).

⬇

EVENT extend

WEIGHT

FCMD + cmd

WHERE

handle=down /\door=open /\gear=retracted

THEN

cmd := 0

gear := {extended @ 0.9 , retraced @ 0.1}

END

⬇

EVENT retract

WEIGHT

FCMD + cmd

WHERE

handle=up /\ door=open /\ gear=extended

THEN

cmd := 0

gear :=<EMAIL_ADDRESS><EMAIL_ADDRESS>
END

⬇

EVENT open

WEIGHT

FCMD + cmd

WHERE

door=closed /\

( (handle=down /\ gear=retracted) \/

( handle=up /\ gear=extended) )

THEN

door := {open @ 0.9 , closed @ 0.1 }

cmd := 0

END

⬇

EVENT close

WEIGHT

FCMD + cmd

WHERE

door=open /\

( (handle=down /\ gear=extended ) \/

( handle=up /\ gear=retracted) )

THEN

door := {open @ 0.1 , closed @ 0.9 }

cmd := 0

END

Figure 1: Events controlling the gear and the doors

###  2.3 Probabilistic Semantics

The state of a machine is a valuation $\mathfrak{s}$ mapping variables and
constants to values of the appropriate type. For a variable or constant $x$,
$\mathfrak{s}(x)$ denotes the value of $x$ in $\mathfrak{s}$. Given an
expression $E(\vec{x})$ that may depend on the (list of) variables $\vec{x}$,
the evaluation of $E$ in the context $\mathfrak{s}$ is denoted as
$E(\vec{x})[\mathfrak{s}]$. Moreover, for an event $e\in\mathcal{E}$, ${\it
var}(e)$ is the set of variables that appear on the left hand side (LHS) of
the assignments in the action of the event. In each event, a variable can
appear only once as LHS in the list of assignments.

An event $e=\langle
w(\vec{x}),\vec{y},G(\vec{x},\vec{y}),act\rangle\in\mathcal{E}$ is _enabled_
at state $\mathfrak{s}$ if $w(\vec{x})[\mathfrak{s}]>0$ and there exists a
valuation $\sigma$ for the parameters $\vec{y}$ making the guard true, i.e.,
$G(\vec{x},\vec{y})[\mathfrak{s}]\sigma={true}$. Then, the action $act$ can be
performed. Given a state $\mathfrak{s}$, $\mathcal{E}(\mathfrak{s})$ denotes
the set of enabled events at $\mathfrak{s}$. The notation $w_{e}$ is used to
denote the weight expression of the event $e$; similarly for the other
components of the event.

The semantics of a machine $\mathcal{M}$ is a probabilistic labeled transition
system (PLTS) $\langle S,s_{0},Acts,T\rangle$ where $S$ is the set of states,
$s_{0}$ is the valuation obtained after executing the initialization, $Acts$
is the set of labels of the events, and $T:S\times Acts\times
S\allowbreak\mathrel{\mathop{\hbox
to11.99998pt{\rightarrowfill}}\limits}[0,1]$ is the transition probability
function defined as follows:

$(\mathfrak{s},e,\mathfrak{s}^{\prime})=\left\\{\begin{array}[]{ll}0&\mbox{ if
}\mathfrak{s}\not\allowbreak\mathrel{\mathop{\hbox
to11.99998pt{\rightarrowfill}}\limits}\mathfrak{s}^{\prime}\\\
\underbrace{\frac{w_{e}[\mathfrak{s}]}{\sum\limits_{e\in\mathcal{E}}w_{e}[\mathfrak{s}]}}_{weight}\times\sum\limits_{\sigma\in\mathcal{T}(\mathfrak{s},e)}\left(\underbrace{\frac{1}{|\mathcal{T}(\mathfrak{s},e)|}}_{parameters}\times\underbrace{\prod\limits_{x\in{\it
var}(e)}~{}\sum\limits_{E\in
Val(x,\mathfrak{s},\mathfrak{s}^{\prime},\sigma,e)}P(E)}_{assignments}\right)&\mbox{
otherwise}\end{array}\right.$

where: $\mathfrak{s}\not\allowbreak\mathrel{\mathop{\hbox
to11.99998pt{\rightarrowfill}}\limits}\mathfrak{s}^{\prime}$ means that either
$\mathcal{E}(\mathfrak{s})=\mathord{\varnothing}$ or $x[\mathfrak{s}]\neq
x[\mathfrak{s}^{\prime}]$ for a variable $x$ not in ${\it var}(e)$ (i.e.,
$\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ differ on a variable not modifiable
by the event); $\mathcal{T}(\mathfrak{s},e)$ is the set of valuations for the
parameters of the event $e$ that make its guard true, i.e.,
$\sigma\in\mathcal{T}(\mathfrak{s},e)$ iff
$G_{e}(\vec{x},\vec{y})[\mathfrak{s}]\sigma=\it{true}$;
$Val(x,\mathfrak{s},\mathfrak{s}^{\prime},\sigma,e)$ is the set of expressions
on the RHS of the assignment that assign to $x$ its value in
$\mathfrak{s}^{\prime}$, i.e., $E\in
Val(x,\mathfrak{s},\mathfrak{s}^{\prime},\sigma,e)$ iff
$E[\mathfrak{s}]\sigma=x[\mathfrak{s}^{\prime}]$; and $P(E)$ is the
probability of choosing the expression $E$ among all the other expressions.

The aim of the first term (_weight_) is to normalize the weights of the
enabled events. Hence, the larger $w_{e}[\mathfrak{s}]$ is, the higher the
probability of choosing $e$ for execution when enabled. Since the expression
$w_{e}$ depends on the state of the variables, such probability may change
during the execution of the system. The second term (_parameters_) counts the
number of possible assignments for the parameters that satisfy the guard of
the event at state $\mathfrak{s}$. Recall that the domain for the parameters
must be a non-empty finite set. The third term (_assignments_) considers all
possible expressions that can be generated due to assignments with a list of
expressions (uniform distribution) or enumerated probabilistic assignments. In
the following,
$\mathfrak{s}\stackrel{{\scriptstyle\,\,(p,e)\,\,}}{{\,\,===\Longrightarrow}}\mathfrak{s}^{\prime}$
denotes that $T(\mathfrak{s},e,\mathfrak{s}^{\prime})=p$ and $p>0$.

The work in [8] establishes conditions for the PLTS generated by an Event-B
specification to be a Discrete Time Markov Chain (DTMC). For that, some proof
obligations must be discarded: (1) the weight of the events are natural
numbers; and (2) in a probabilistic assignment
$x:=\\{E_{1}@p_{1},...,E_{n}@p_{n}\\}$, $0<p_{i}\leq 1$ and $\sum p_{i}=1$. In
that case, it is possible to show that for all states $\mathfrak{s}$,
$\sum\\{p\mid\mathfrak{s}\stackrel{{\scriptstyle\,\,(p,e)\,\,}}{{\,\,===\Longrightarrow}}\mathfrak{s}^{\prime}\\}=1$.
These conditions are assumed to be true in the rest of the paper for any
machine $\mathcal{M}$.

##  3 Translating Machines to Probabilistic Rewrite Theories

Rewriting logic (RL) [15] (see a survey in [16]) is a general model for
concurrency where systems are declaratively specified using algebraic data
types and (conditional) rewrite rules. This section presents a map
$[\\![\cdot]\\!]:\mathcal{M}\allowbreak\mathrel{\mathop{\hbox
to11.99998pt{\rightarrowfill}}\limits}\mathcal{R}_{\mathcal{M}}$ from a
probabilistic Event-B machine to a probabilistic rewrite theory [4]. The
rewrite theory $\mathcal{R}_{\mathcal{M}}$ is obtained in two steps. First, it
contains (as a subtheory) a rewrite theory $\mathcal{R}$ defining sorts and
operations to represent declared types/sets and constants of any context, as
well as the infrastructure needed to encode the variables and the events of
any probabilistic machine. Second, $\mathcal{R}$ is extended with rules
specific for the machine $\mathcal{M}$. Computation with
$\mathcal{R}_{\mathcal{M}}$ is shown to be free of un-quantified non-
determinism (a condition needed for statistical analysis [4]), as well as to
be sound and complete w.r.t. the probabilistic semantics of $\mathcal{M}$.

In the following sections, the background on RL needed to understand the
translation is introduced gradually. In most of the cases, the notation of
Maude [11], a high-level language that supports membership equational logic
and rewriting logic specifications, will be adopted. This has the immediate
effect of producing an executable specification. For the sake of readability,
some details of the specification are omitted. The complete specification of
the theory $\mathcal{R}_{\mathcal{M}}$ is available at [17] as well as a
parser automatizing the translation $[\\![\cdot]\\!]$.

###  3.1 Translating Contexts

A _rewrite theory_ is a tuple $\mathcal{R}=(\Sigma,E\uplus B,R)$. The static
behavior of the system is modeled by the order-sorted equational theory
$(\Sigma,E\uplus B)$ and the dynamic behavior by the set of rewrite rules $R$
(more on this in §3.2). The signature $\Sigma$ defines a set of typed
operators used to build the terms of the language (i.e. the syntax of the
modeled system). $E$ is a set of (conditional) equations over $T_{\Sigma}$
(the set of terms built from $\Sigma$) of the form
$t=t^{\prime}~{}\mathbf{if}\phi$. The equations specify the algebraic
identities that terms of the language must satisfy (e.g., $x+0=x$). Moreover,
$B$ is a set of structural axioms (associativity, commutativity, and identity,
or combinations of them) over $T_{\Sigma}$ for which there is a finitary
matching algorithm. The equational theory thus defines algebraic data types
and deterministic and finite computations as in a functional programming
language.

Let’s start defining appropriate sorts (types) and operators to specify an
Event-B contexts $\mathcal{C}=\langle SET_{l}\cup SET_{n},CTE\rangle$. Natural
and integer numbers, as well as Booleans, are mapped directly to the
corresponding sorts in Maude. Any other constant symbol inhabiting the
deferred sets $SET_{l}$ and $SET_{n}$ (e.g., open, close) is represented as a
string. The sort EBElt below defines the values for basic types:

⬇

fmod EBELT is \--- Functional module EBELT (equational theory)

sort EBElt . \--- Basic values

op elt : Int -> EBElt . \--- Nat and Int

op elt : Bool -> EBElt . \--- Boolean

op elt : String -> EBElt . \--- Elements of deferred sets

op _<_ : EBElt EBElt -> Bool . \--- Order on EBElt

[...]

\--- Total order on EBElt

view EBElt< from STRICT-TOTAL-ORDER to EBELT is sort Elt to EBElt . endv

Terms elt("open") and elt(9) of sort EBElt represent, respectively, the
constant symbol open in the deferred set SOC and the number $9$. The equations
defining the strict total order _<_ (underscores in Maude denote the position
of the parameters in an operator) are defined as expected for elements of the
same type (e.g., for two integers $n,m$, elt(n) < elt(m) = n < m). Although
elements of different types are not supposed to be compared in (well-typed)
machines, the definition of $<$ decrees that elt(s) < elt(b) for any string
$s$ and Boolean $b$ and elt(b) < elt(n) for any number $n$.

⬇

fmod EBSET is \--- Sets of EBElt

pr SORTABLE-LIST-AND-SET{EBElt<} * (sort Set{EBElt<} to EBSet) .

op _.._ : Int Int -> EBSet . \--- Building finite subsets of Int

op gen-set : String Nat -> EBSet . \--- Building indexed (string) constants

op gen-set : List{String} -> EBSet . \--- Building a EBSet from a list of
strings

[...]

Sortable lists allow to uniquely represent sets as lists, which is key for
having quantified non-determinism. The Maude’s theory SORTABLE-LIST-AND-SET is
instantiated with the total order EBElt< defined above and the sort
Set{EBElt<} is renamed to EBSet. The defined operators, and their equations
omitted here, are used to encode deferred sets by enumeration, cardinality or
as integer intervals: gen-set("open" "close") reduces to {elt("open"),
elt("close")}; gen-set(s,n) reduces to the set

{elt(s1),...,elt(sn)} and the term n .. m reduces to {elt(n),...,elt(m)}.

Pairs of EBElts as well as (sortable) lists and sets of pairs are built as
follows:

⬇

fmod EBPAIR is

pr EBSET .

sort EBPair . \--- Pairs of EBElt

op _|->_ : EBElt EBElt -> EBPair .

[...]

view EBPair from STRICT-TOTAL-ORDER to EBPAIR is sort Elt to EBPair . endv

fmod EBRELATION is \--- Relations / sets of pairs

pr SORTABLE-LIST-AND-SET{EBPair} * (sort Set{EBPair} to EBRel) .

[...]

The module EBRELATION implements most of the operations on sets and relations
defined in the syntax of Event-B. However, as explained in Section 3.2, the
operations and equations needed to specify expressions including set
comprehensions ($\\{x.S\mid P(x)\\}$ and $\\{x.S\mid F(x)\\}$) are generated
according to the Event-B model at hand.

Values for constants and variables are terms of sort EBType built from
(possibly singleton) sets of EBElts or EBPairs:

⬇

fmod EB-TYPE is

pr EBRELATION .

sort EBType .

op val : EBSet -> EBType . \--- Sets of basic types

op val : EBRel -> EBType . \--- Sets of pairs

[...]

Hence, the value of the Event-B constant FCMD is encoded as the term
val(elt(9)) while a function $f$ of type 1..2 * SOC might be assigned the
value

val( (elt(1) |-> elt("open"), elt(2)|-> elt("close")) ).

All Boolean and arithmetic operations, and operations on sets and relations
are lifted to operators of sort EBType ad-hoc. For instance,
val(elt(2))+val(elt(3)) reduces to val(elt(3)+elt(2)) that, in turn, reduces
to val(elt(3+2)) 111Operators of sort EBType are certainly partial and a term
such as
val(elt(2))+val(elt("open")) does not have any reduction. It is worth noticing
that such terms cannot appear in the encoding of a well-typed Event-B model..
The theory EB-TYPE thus defines an encoding $[\\![\cdot]\\!]_{\texttt{e}}$
from Event-B expressions into EBType expressions where Event-B (arithmetic,
Boolean, relational, and set) operators and values are mapped into the
corresponding terms defined in EB-TYPE. Most of the cases in the definition of
$[\\![\cdot]\\!]_{\texttt{e}}$ are immediate. The interesting cases will be
introduced gradually next.

An Event-B context is specified as a mapping from the identifiers of the
deferred sets to EBSets and context’s constants to their values in the sort
EBType. This is the purpose of the following theory:

⬇

mod EBCONTEXT is

pr CONFIGURATION . pr EB-TYPE . pr MAP{Qid, EBSet} . pr MAP{Qid, EBType} .

subsort Qid < Oid . \--- Names for contexts

op Context : -> Cid . \--- Class for contexts

op sets :_ : Map{Qid , EBSet} -> Attribute . \--- Context’s user-defined sets

op constants :_ : Map{Qid , EBType} -> Attribute . \--- Context’s constants

op init-context : Qid -> Object . \--- Building a context

var Q : Qid .

eq init-context(Q) = < Q : Context | sets : init-sets, constants : init-constants > .

\--- Operators to be instantiated by the implementation of the context

op init-sets : -> Map{Qid , EBSet} . \--- Building deferred sets

op init-constants : -> Map{Qid , EBSet} . \--- Initializing constants

endm

It is customary in Maude to represent complex systems by using an object
oriented notation (theory CONFIGURATION). An object $O$ of a class $C$ is
represented by a record-like structure of the form $\langle
O:C~{}|~{}a_{1}:v_{1},\cdots,a_{n}:v_{n}\rangle$, where $a_{i}$ are attribute
identifiers and $v_{i}$ are terms that represent the current values of the
attributes. The state of the system is then a multiset of objects called
_configuration_. In the above theory, quoted identifiers (e.g., ’GEAR_CTX) are
used as object identifiers (subsort Qid < Oid). Moreover, a new class
identifier (Cid) is defined along with the needed attributes. The term init-
context(Q) encodes a context with identifier Q and attributes sets and
constants. Logical variables as Q are implicitly universally quantified in
equations and rules.

The theory EBCONTEXT is common to any Event-B model and each particular
context needs to extend it with equations populating the definition of the
deferred sets and also initializing the constants. For instance, in the
running example, the following equations need to be added:

⬇

eq init-sets = ( ’SUD |-> gen-set("up" "down"),

’SOC |-> gen-set("open" "close")) .

’SER |-> gen-set("extended" "retracted"),

eq init-constants = ( ’FCMD |-> val(elt(9)) ) .

######  Definition 1 (Encoding of Contexts).

Let $\mathcal{C}=\langle SET_{l},SET_{n},CTE\rangle$ be an Event-B context.
The theory $\mathcal{R}_{\mathcal{C}}$ results from extending EBCONTEXT with
the following equations:

$\begin{array}[]{lll}\mbox{\it init-sets}&=&\\{id_{S}\mapsto\mbox{{\it gen-
set}}((id_{1},...,id_{m}))\mid id_{S}:\\{id_{1},...,id_{m}\\}\in
SET_{l}\\}\cup\\{id_{S}\mapsto\mbox{\it gen-set}(id_{S},k)\mid id_{S}:k\in
SET_{n}\\}\\\ \mbox{\it init-
constants}&=&\\{c\mapsto[\\![e]\\!]_{\texttt{e}}\mid(c~{}:~{}type~{}:=~{}e)\in
CTE\\}\end{array}$

###  3.2 Encoding Machines

The specification of a machine $\mathcal{M}$ in the theory
$\mathcal{R}_{\mathcal{M}}$ requires some extra sorts and equations, but also,
(probabilistic) rewrite rules. Before continuing with the encoding, the
meaning of the set of rewrite rules $R$ in $(\Sigma,E\uplus B,R)$ is
explained.

Probabilistic rewrite rules. A rewrite rule $l(\vec{x})\rightarrow
r(\vec{x})\;\mathbf{if}\;\phi(\vec{x})$ specifies a pattern $l(\vec{x})$ that
can match some fragment of the system’s state $t$ if there is a substitution
$\theta$ for the variables $\vec{x}$ that makes $\theta(l(\vec{x}))$ equal
(modulo the set of structural axioms $B$) to that state fragment, changing it
to the term $\theta(r(\vec{x}))$ in a local transition if the condition
$\theta(\phi(\vec{x}))$ is true. In a probabilistic rewrite theory [4],
rewrite rules can have the more general form $l(\vec{x})\rightarrow
r(\vec{x},\vec{y})\;\mathbf{if}\;\phi(\vec{x})\;\textit{with
probability}\;\vec{y}{\ :=\ }\pi(\vec{x}),$ where some new variables $\vec{y}$
are present in the pattern $r$. Due to the new variables $\vec{y}$, the next
state specified by such a rule is not uniquely determined: it depends on the
choice of an additional substitution $\rho$ for the variables $\vec{y}$. In
this case, the choice of $\rho$ is made according to the family of probability
functions $\pi_{\theta}$: one for each matching substitution $\theta$ of the
variables $\vec{x}$.

Probabilistic rewrite theories can be simulated directly in Maude by sampling,
from the corresponding probabilistic functions, the values for the variables
$\vec{y}$ appearing on the RHS. Moreover, using a Monte-Carlo simulation and
the query language QuaTEx (Quantitative Temporal Expressions), it is possible
to analyze quantitative properties of the system by statistical model checking
(more details on §4).

Machine’s variables and state. The specification of a machine starts with a
theory that extends EBCONTEXT with a mapping from the identifiers of the
variables to their values:

⬇

mod EBMACHINE is

inc EBCONTEXT . \--- Context specification.

op Machine : -> Cid . \--- Class for machines

op variables :_ : Map{Qid , EBType} -> Attribute . \--- Machine’s variables

op init-variables : -> Map{Qid , EBType} . \--- Instantiated by the machine at
hand

op init-machine : Qid Qid -> Object . \--- Initial state of the machine

vars QM QC : Qid .

eq init-machine(QC, QM) = \--- Configuration defining the machine QM and its
context QC

init-context(QC) \--- Context

< QM : Machine | variables : init-variables > \--- Variables

< events : Events | state: init-events >. \--- Events

[...] \--- event specification explained below

The specification of a machine $\mathcal{M}$ as the rewrite theory
$\mathcal{R}_{\mathcal{M}}$ is obtained by extending the previous theory in
two ways: (1) the initialization event of the machine gives rise to an
equation that populates the mapping init-variables. And (2), building from the
infrastructure in EB-TYPE, different equations and rewrite rules are added to
EBMACHINE in order to encode the semantics of the machine’s events.

For the running example, (1) amounts to define the equation:

⬇

eq init-variables = (’handle |-> val(elt("up"))) , (’door |->
val(elt("close"))),

(’gear |-> val(elt("retracted"))) , (’cmd |-> val(elt(0))) .

More generally, for any machine with initialization
$x_{1}:=E_{1},...,x_{n}:=E_{n}$ the following equation needs to be added to
EBMACHINE:

$\mbox{\it init-
variables}=x_{1}\mapsto[\\![E_{1}]\\!]_{\texttt{e}},...,x_{n}\mapsto[\\![E_{n}]\\!]_{\texttt{e}}$
(1)

For (2), the theory must generate a purely probabilistic transition system
without un-quantified non-determinism, thus guaranteeing that execution paths
in the system form a measurable set [4]. Otherwise, it is not possible to
perform (sound) statistical analyses (§4). Hence, the theory EBMACHINE is
extended with:

  1. (i)

A deterministic mechanism that, given the current state of the machine,
determines whether an event is enabled or not.

  2. (ii)

A probabilistic rule that chooses, according to the weights of the enabled
events, the next event to be executed. This rule is common to any Event-B
model and thus defined directly in the theory EBMACHINE.

  3. (iii)

For each event, a rule that chooses probabilistically the parameters of the
event (if any) as well as the values for probabilistic assignments. Then, the
state of the machine is updated accordingly. The application of this rule will
correspond to an observable state transition of the machine $\mathcal{M}$.

Events’ state (i). Starting with (i), the sort EvState (declared in EBMACHINE)
defines four possible states for an event:

⬇

sort EvState . \--- States of events

ops blocked unknown execute : -> EvState .

op enable : NzNat -> EvState . \--- Enable with a given weight w > 0

and the object events (see init-machine in the module EBMACHINE) stores a list
with the state of each event:

⬇

sort Event LEvent . \--- Events and list of events

op ev : Qid EvState -> Event . \--- ID of the event and its state

op state:_ : LEvent -> Attribute . \--- Attribute for objects of class Events

op init-events : -> LEvent . \--- To be instantiated by the machine at hand

Initially, all the events are in state _unknown_. Hence, for any machine with
events $e_{1},...,e_{n}$, EBMACHINE must be extended with the following
equation

$\mbox{\it init-events}=ev(e_{1},unknown)~{}\cdots~{}ev(e_{k},unknown)$ (2)

For each constant and variable in the model, a Maude variable of sort EBType
is added. This facilitates the definition of the forthcoming equations and
rules. In the running example: vars $FCMD $handle $gear $door $cmd : EBType .
Such variables will appear in the objects Context and Machine. This allows for
defining $[\\![x]\\!]_{\texttt{e}}=\$x$ when the Event-B variable or constant
$x$ appears in the context of an expression. The prefix “$” is added to avoid
clash of names. Consistently, the following shorthands will be used (CC, MM,
and EE in Maude’s snippets):

$\begin{array}[]{l}\mathfrak{C}=\langle\mbox{\it C}:\mbox{\it Context}\mid
sets:\$sets,constants:\mbox{\it init-constants}\rangle\\\
\mathfrak{M}=\langle\mbox{\it M}:\mbox{\it Machine}\mid
variables:\\{x\mapsto\$x\mid
x\in\vec{x}\\}\rangle\quad\mathfrak{E}=\langle\mbox{\it E}:\mbox{\it
Events}\mid state:\mbox{\it init-events}\rangle\end{array}$

For each event $e$, EBMACHINE is extended with an equation that
(deterministically) updates the state of $e$ from _unknown_ to _blocked_ or to
_enabled_. More precisely, consider an event $e\in\mathcal{E}$ with guard
$e_{G}$, weight $e_{W}$, and set of parameter declarations $e_{any}$. Let
$W=\mbox{\it ebtype2nat}([\\![e_{w}]\\!]_{\texttt{e}})$ and $B=\mbox{\it
ebtype2bool}([\\![e_{G}]\\!]_{\texttt{e}})$ where ebtype2nat(val(elt(n))) = n
(and similarly for ebtype2bool). The needed equation is the following:

$\small\begin{array}[]{lll}\mathfrak{C}~{}\mathfrak{M}~{}\langle E:\mbox{\it
Events}\mid\mbox{\it
state:}LE~{}ev(e,unknown)~{}LE^{\prime}\rangle=\mathfrak{C}~{}~{}\mathfrak{M}~{}~{}\langle
E:\mbox{\it Events}\mid\mbox{\it
state:}LE~{}NSt~{}LE^{\prime}\rangle\end{array}$ (3)

where $NSt$ is the expression

$\mbox{\bf if}~{}B\wedge W>0\wedge\bigwedge\limits_{(y:\in e_{y})\in
e_{any}}\mbox{\it not-empty}([\\![e_{y}]\\!]_{\texttt{e}})\mbox{\bf~{} then
}ev(e,enable(W))\mbox{\bf~{} else }ev(e,blocked)\mbox{\bf~{} fi }$

The constants of the model ($\mathfrak{C}$) and the current values of the
variables ($\mathfrak{M}$) are used to evaluate the Boolean expression of the
guard ($B$) and the integer expression of the event’s weight ($W$). If $B$
holds, $W>0$, and the set of possible values for each parameters is not empty,
the event becomes enabled with weight $W$. Otherwise, it is blocked. The
variables $LE$ and $LE^{\prime}$, of sort LEvent, allow to apply this equation
at any position of the list of events.

Next event (ii). The next step is to add to EBMACHINE the probabilistic rule

$l(LE)\rightarrow r(LE,p)\;\mathbf{if}\;\phi(LE)\;\textit{with
probability}\;p\ :=\ \pi(LE)$ (4)

where: $l(LE)=\langle E:\textit{Events}\mid state:~{}\textit{LE}\rangle$;
$\phi(LE)=true$ iff all event in $LE$ is either enabled or blocked and there
is at least one enabled event; $\pi(LE)$ is a uniform distribution on the
interval $[0,W)$ where $W=\sum\\{w_{j}\mid ev(e_{j},enable(w_{j})\in LE)\\}$;
and $r(LE,p)=\langle E:\textit{Events}\mid
state:~{}ev(pick(acc(filter(LE)),p),\textit{execute})\rangle$. Let
$LE^{\prime}=filter(LE)$ be the list of enabled events in $LE$ with weights
$w_{1},\cdots,w_{n}$. Moreover, let $LE_{A}=acc(LE^{\prime})$ be as
$LE^{\prime}$ where the weight of the $ith$ event in $LE_{A}$ is
$\sum\limits_{1\leq j\leq i}w_{j}$. Then, $pick(LE_{A},p)=e_{k}$ iff $e_{k}$
is the first event in $LE_{A}$ whose weight is strictly greater than $p$.
Intuitively, the rule is enabled only when the state of all the events is
different from _unknown_ and at least one event is _enabled_ (otherwise, the
system is in a deadlock). The enabled events are filtered and their weights
accumulated ($LE_{A}$). Hence, an enabled event $e$ with weight $w$ is chosen
for execution with probability $w/W$, where $W$ is the sum of the weights of
the enabled events at the current state.

Following [4], the probabilistic rule (4) can be written in Maude by
generating random numbers appropriately:

⬇

crl [next-event] : < events : Events | state: LE > =>

< events : Events | ev(pick(LEA, rand(max-value(LEA))), execute) >

if all-ready(LE) \--- All e in LE is in state either blocked or enabled

/\ one-firable(LE) \--- At least one event is enabled

/\ LE’ := filter(LE) \--- Extract the enabled events

/\ LEA := accumulate(LE’) . \--- Accumulate the weights

Here, max-value returns the weight of the last element in LEA (i.e., the sum
$W$ of the weights of the enabled events). A random number in the interval
$[0,W)$ is generated and the choice of the next event follows the distribution
$\pi(LE)$ as explained above.

Actions in events (iii).  Step (iii) consists in defining a rule, for each
event $e$, that updates the state of the machine when such a rule is applied:

$\begin{array}[]{lll}\mathfrak{C}~{}\mathfrak{M}~{}\langle\mbox{\it
events:Events}\mid\mbox{\it state: ev(e,
execute)}\rangle&\Rightarrow&\mathfrak{C}~{}\mathfrak{M}^{\prime}~{}\mathfrak{E}\end{array}$
(5)

where $\mathfrak{M}^{\prime}=\langle\mbox{\it M}:\mbox{\it
Machine}\mid\mbox{\it
variables:}\\{x\mapsto\$x\mid{x\in\vec{x_{u}}}\\}\cup\\{x\mapsto[\\![e_{x}]\\!]_{\texttt{e}}\mid{x:=e_{x}\in
e_{act}}\\}\rangle$ and $\vec{x_{u}}$ is the set of variables that do not
appear in the LHS of the set of actions/assignments $e_{act}$ of the event.
This rule can be fired only if the event has been chosen for execution. The
expression $[\\![e_{x}]\\!]_{\texttt{e}}$, updating the state of the variable
$x$, is built as before but new cases need to be considered:

  * •

$[\\![y]\\!]_{\texttt{e}}=\mbox{\it choice}(\mbox{\it
makeList}([\\![e_{y}]\\!]_{\texttt{e}}))$ if $y:\in e_{y}$ is a parameter of
the model;

  * •

$[\\![\\{\\{E\\}\\}]\\!]_{\texttt{e}}=\mbox{\it choice}(\mbox{\it
makeList}([\\![E]\\!]_{\texttt{e}}))$; and

  * •

$[\\![\\{\\{E_{1}@p_{1},...,E_{n}@p_{n}\\}\\}]\\!]_{\texttt{e}}=\mbox{\it
choice}(\mbox{\it
accumulate}([\\![E_{1}]\\!]_{\texttt{e}}@p_{1},...,[\\![E_{n}]\\!]_{\texttt{e}}@p_{n}))$.

The set of values a parameter can take and the (set) expression $E$ in the
probabilistic assignment $x:=\\{E\\}$ are converted into lists of EBTypes.
Since the elements of EBSet and EBRel are _sortable_ , these lists are always
generated in the same order. This guarantees that there is no un-quantified
non-determinism due to the way the elements of the set are arranged. Similar
to the definition of the rule [next-event], random numbers are used to realize
the needed probabilistic rewrite rule. More precisely, the function
$choice(L)$ generates a random number $0\leq i<size(L)$ and returns the $i$th
element of the list $L$, thus following a uniform probabilistic distribution.
The $i$th element of $L^{\prime}=\mbox{\it
accumulate}(\\{E_{1}@p_{1},...,E_{n}@p_{n}\\})$) is $E_{i}@\sum_{0\leq j\leq
p_{j}}$. In this case, the function _choice_ generates a random number $0\leq
R<1$ and returns the first element $E_{k}@p_{k}$ in $L^{\prime}$ where
$R<p_{k}$. For illustration, the tool generates the following rule for the
event $pcmd$:

⬇

rl [pcmd] : CC MM < events : Events | state: ( ev(’pcmd, execute) ) > =>

CC < $MNAME : Machine | variables:

(’handle |-> choice( makeList(val(elt("up")) , val(elt("down")))),

’cmd |-> ($cmd) + (val(elt(1))), ’door |-> $door ...) > EE .

Handling set comprehension. Sets in parameters and RHS in assignments can be
built using set comprehension. Such expressions must be evaluated in both, the
equation determining the state of the event (checking whether the set of
values for a parameter is empty or not) and the rule specifying the state
transition. The expression $\\{x.S\mid P(x)\\}$ (resp., $\\{x.S\mid F(x)\\}$)
can be thought of as the higher order function _filter_ (resp., _map_) in
functional languages. Even though it is possible to use the reflective
capabilities of rewriting logic and meta-programming in Maude to encode
higher-order functions [12], a simpler path is followed here. For each
expression of the form $\\{x.S\mid P(x)\\}$, the tool generates a new operator
and two equations of the following form:

⬇

op $filter-id : EBType Configuration -> EBType .

eq $filter-id(val(empty), C) = val(empty) . \--- Base case

\--- Recursive case

eq $filter-id(val((E,S)), (< $CNAME : Context | sets: ($sets),constants: (’c1 |-> $c1,...)>

< $MNAME : Machine | variables: (’v1 |-> $v1, ...) > )) =

$filter-id(val( S ), (< $CNAME : Context | ... > < $MNAME : Machine | ... >)) union

if ebtype2bool(exp-P(val(E))) then val(E) else val(empty) fi .

The first parameter corresponds to the (encoding of the) set of values $S$ and
the second is the configuration giving meaning to the constants and variables
of the model. The term _exp-P_ is the EBType expression encoding the predicate
$P$ and the element $E$ is discarded (union val(empty)) if such an expression
evaluates to val(elt(false)). Hence, $[\\![\\{x.S\mid
P(x)\\}]\\!]_{\texttt{e}}=\mbox{\it filter-
id}({[\\![S]\\!]_{\texttt{e}},\mathfrak{C}~{}\mathfrak{M}})$. A similar
strategy is used to encode the set $\\{x.S\mid F(x)\\}$.

Summing up, Event-B models are represented as a term of sort Configuration
with three objects: $\langle C:Context~{}|~{}CAts\rangle~{}\langle
M:Machine~{}|~{}MAts\rangle~{}\langle E:Events~{}|~{}EAts\rangle$ where _CAts_
, _MAts_ , and _EAts_ are the attributes explained above. Moreover, Maude’s
variables appear in $MAts$ and _CAts_ in all the LHS of equations and rules,
thus making available the values of the model to encode arbitrary Event-B
expressions as EBType expressions.

######  Definition 2 (Encoding).

Let $\mathcal{M}=\langle\mathcal{C},\vec{x},I,\mathcal{E},init\rangle$. The
rewrite theory $\mathcal{R}_{\mathcal{M}}$ specifying the behavior of
$\mathcal{M}$ is obtained by extending EBCONTEXT as in Definition 1 and
extending the theory EBMACHINE with: the equations (1), (2), (3); the rule (5)
(for each event); and the operators and equations defining filter- and map-
like expressions. Given a state $\mathfrak{s}$ of the machine $\mathcal{M}$,
$[\\![\mathcal{M}]\\!]_{\mathfrak{s}}$ denotes the term
$\mathfrak{C}_{\mathfrak{s}}~{}~{}\mathfrak{M}_{\mathfrak{s}}~{}~{}\mathfrak{E}$
where $\mathfrak{C}_{\mathfrak{s}}$ is as $\mathfrak{C}$ but each variable
$\$c_{i}$ is replaced with $[\\![\mathfrak{s}(c_{i})]\\!]_{\texttt{e}}$ and
$\mathfrak{M}_{\mathfrak{s}}$ replaces each variable $\$x_{i}$ with
$[\\![\mathfrak{s}(x_{i})]\\!]_{\texttt{e}}$.

Assuming that the specification of the arithmetic, Boolean, and relational
operators in $\mathcal{R}_{\mathcal{M}}$ is adequate with respect to the
corresponding semantics for the Event-B operators, it is possible to show that
the specification is correct in the following sense.

######  Theorem 3.1 (adequacy).

Let $\mathcal{M}$ be an Event-B machine and $\mathcal{R}_{\mathcal{M}}$ be as
in Definition 2. Hence,
$\mathfrak{s}\stackrel{{\scriptstyle\,\,p,e\,\,}}{{\,\,===\Longrightarrow}}\mathfrak{s}^{\prime}$
iff
$[\\![\mathcal{M}]\\!]_{\mathfrak{s}}\longrightarrow_{p}[\\![\mathcal{M}]\\!]_{\mathfrak{s}^{\prime}}$,
where $\longrightarrow_{p}$ denotes one-step rewriting in
$\mathcal{R}_{\mathcal{M}}$ with probability $p$.

###### Proof.

(sketch). In what follows, $\rightsquigarrow$ denotes equational reduction in
$\mathcal{R}_{\mathcal{M}}$. Note that $p$ must be of the form $p_{w}\times q$
where $p_{w}$ is the first term (weight) in the transition probability
function (§2.3) and $q$ is the rest of the expression (resulting probability
for parameters and assignments). $[\\![\mathcal{M}]\\!]_{\mathfrak{s}}$
necessarily exhibits the following reductions:
$[\\![\mathcal{M}]\\!]_{\mathfrak{s}}=\mathfrak{C}_{\mathfrak{s}}~{}\mathfrak{M}_{\mathfrak{s}}~{}\mathfrak{E}\rightsquigarrow^{*}\mathfrak{C}_{\mathfrak{s}}~{}\mathfrak{M}_{\mathfrak{s}}~{}\mathfrak{E}^{\prime}\longrightarrow_{p^{\prime}_{w}}\mathfrak{C}_{\mathfrak{s}}~{}\mathfrak{M}_{\mathfrak{s}}~{}\mathfrak{E}^{\prime\prime}\longrightarrow_{q^{\prime}}\mathfrak{C}_{\mathfrak{s}}~{}\mathfrak{M}^{\prime}_{\mathfrak{s}}~{}\mathfrak{E}$
where: $\mathfrak{E}^{\prime}$ is the (unique) normal form of $\mathfrak{E}$
where the state of the events are either $blocked$ or $enabled$;
$\mathfrak{E}^{\prime\prime}$ results from an application of the rule next-
event, choosing probabilistically one of the enabled events; and
$\mathfrak{M}^{\prime}_{\mathfrak{s}}$ is the new state after the application
of the rule corresponding to the (unique) chosen event. If the semantics of
the operators in Event-B agrees with the one defined for terms of sort EBType,
(i.e., the Event-B expression $e$ reduces to the value $v$ iff
$[\\![e]\\!]_{\texttt{e}}\rightsquigarrow^{*}[\\![v]\\!]_{\texttt{e}}$) the
set of enabled events in $\mathfrak{E}^{\prime}$ must necessarily coincide
with those enabled in state $\mathfrak{s}$ and necessarily
$p_{w}=p^{\prime}_{w}$. Under the same assumption, the set of possible values
for the parameters are the same in $\mathfrak{s}$ and
$\mathfrak{M}_{\mathfrak{s}}$. Therefore, $q=q^{\prime}$ and the term
$\mathfrak{C}_{\mathfrak{s}}~{}\mathfrak{M}^{\prime}_{\mathfrak{s}}~{}\mathfrak{E}$
necessarily corresponds to $[\\![\mathcal{M}]\\!]_{\mathfrak{s}^{\prime}}$. ∎

##  4 Case Studies and Experiments

Given a model $\mathcal{M}$, the theory $\mathcal{R}_{\mathcal{M}}$ generated
by the tool [17] can be used to perform statistical analysis. The resulting
Maude’s module includes a template to ease the specification of properties as
formulas in the Quantitative Temporal Expressions language (QuaTEx) [4].
QuaTEx expressions can query the expected value of any expression, thus
generalizing probabilistic computation tree logic (PCTL) [13].

QuaTEx formulas can be evaluated by performing a Monte-Carlo simulation with
the aid of the PVeStA tool [5]. Hence, the expected value of a given QuaTEx
expression can be obtained within a confidence interval according to a
parameter $\alpha$. PVeStA defines the operator val: Nat Configuration ->
Float that identifies the QuaTEx expression (first parameter) and, given a
configuration, returns the value of the expression as a float. The parser of
the tool accepts a section PROPERTIES, at the end of the machine definition,
including Event-B expressions that are later translated and used in equations
giving meaning to val. In the running example, the expression door=open is
translated to the following equation that reduces to $1.0$ when the doors are
open:

⬇

eq val(1, Conf < $MNAME : Machine | variables: ... ) = toFloat((($door) =b (val(elt("open"))))) .

The simulation shows that the expected value of such expression is 0.0 (the
doors are always closed after finishing the maneuver). Also, it is possible to
estimate that the probability of ending the sequence of actions with the gear
retracted (property gear=retracted) is $0.49\pm 0.01$. This is explained by
the fact that the event $pcmd$ may change the value of the handle to $up$ and
$down$ with equal probability.

As a more compelling example, consider the model of the P2P protocol in [8]. A
file partitioned into $K$ blocks is to be downloaded by $N$ clients; a client
can only download a block at a time. As a model of failure, some blocks may be
lost and then retransmitted. The context of the model includes two constants
$N$ and $K$ of type $Nat$. A deferred set $STATE=\\{emp,ok,downloading\\}$
defines the state of the blocks. The file is modeled as a variable of type
POW(Nat * State) and initialized with the expression (0 .. (N * K - 1)) *
{emp}. The pair $i\mapsto emp$ means that the block $i/N$ has not been
downloaded by the client $i\mbox{ mod }N$. Below the events for receiving and
sending blocks:

⬇

EVENT sent

WEIGHT N * K - card(file $\mathbin{\rhd}$ {downloading})

ANY block $:\in${x . dom(file $\mathbin{\rhd}$ {emp}) | ((x mod N) $\notin$ {y . dom(file $\mathbin{\rhd}$ {downloading}) | y mod N})}

WHERE True

THEN file := file $\mathbin{\lhd\mkern-9.0mu-}$ { block |-> downloading }

n := n + 1

END

EVENT receive

WEIGHT 1 + card( file $\mathbin{\rhd}$ {ok})

ANY block $:\in$ dom(file $\mathbin{\rhd}$ { downloading })

WHERE True

THEN file := file $\mathbin{\lhd\mkern-9.0mu-}$ { block |-> ok }

END

The event $sent$ selects a block $x$ s.t. $file(x)=emp$ (range restriction
$\mathbin{\rhd}$) and whose client ($x\mbox{ mod }N$) is not in the set of
clients that are currently downloading blocks. Note the nested set
comprehension expression. In that case, the variable $file$ is updated
($\mathbin{\lhd\mkern-9.0mu-}$) by changing the state of the block to
$downloading$ and incrementing the counter $n$. The event $receive$ selects
one of the blocks in state $downloading$ and updates it to the state $ok$,
signaling that it was successfully downloaded. The probability of sending
blocks decrements according to the number (card) of blocks being downloaded.

⬇

EVENT fail

WEIGHT N * K - card( file $\mathbin{\rhd}$ {ok})

ANY block $:\in$ dom(file $\mathbin{\rhd}$ { downloading })

WHERE True

THEN file := {file @ 0.6 ,

(file$\mathbin{\lhd\mkern-9.0mu-}${ block |-> emp })@ 0.4}

END

The event _fail_ leaves the file unchanged with probability 0.6 and, with
probability 0.4, it changes the state of one $downloading$ block to $emp$. In
the second case, the block needs to be retransmitted. For instance, if $N=16$
and $K=30$, PVeStA reports that the expected value for $n$ is $1554.56$ (i.e.,
each block is transmitted, in average, 3.24 times). Other experiments for
different values of $N$ and $K$ as well as more details about the simulations
can be found at [17]. The site of the tool contains also other case studies
including the probabilistic model for the emergency brake system described in
[7] and the bounded re-transmission protocol modeled in Event-B in [1, Chapter
6].

##  5 Concluding Remarks

Combining formalisms in the context of the B-method has been explored in
different directions, thus leading to more robust tools for system modeling
and verification. The authors of [2] propose a correct-by-construction
approach for hybrid systems in Event-B. The main idea is to move from an
event-triggered to a time-triggered approach because of real-life scenarios.
However, models become more difficult to verify. For this latter purpose, the
authors use a dynamic logic for refinement relations on hybrid systems to
prove that time-triggered models are refinements of event-triggered models.
There is a wide-range effort by the ANR agency and its partners in the EBRP
project [3] to enhance Event-B and the corresponding Rodin [1] toolset by
defining extension mechanisms. Their main goal is to allow Event-B models to
import and use externally defined domain theories via theory constructs
already available in Event-B and implemented in Rodin as a plug-in. The work
in [18] proposes an extension of Event-B to enable stochastic reasoning about
dependability-related non-functional properties of cyclic systems. Such an
extension integrates reasoning about functional correctness and stochastic
modeling of non-functional characteristics. Recently, the authors in [10] have
proposed B Maude, a prototype executable environment for the Abstract Machine
Notation (AMN) implemented in the Maude language. It endows the B method with
execution by rewriting, symbolic search with narrowing, and Linear Temporal
Logic model checking of AMN descriptions.

Following the lines of the aforementioned works, this paper couple Event-B
with further tools and reasoning techniques by proposing a rewriting logic
semantics for a probabilistic extension of it. The translation from an Event-B
model to a probabilistic rewrite theory has been fully automated, and it was
shown to be sound and complete w.r.t. the semantics of the model. The
translation supports a wide spectrum of operators and constructs usually
present in Event-B specifications and all sources of probabilistic behavior as
proposed in [8]. The resulting probabilistic rewrite theory can be executed in
Maude [4] and statistically model checked with the PVeStA tool [5]. A case
study has been presented to illustrate the encoding and how the statistical
analysis enabled by the translation can complement the inference-based
approach in Event-B.

Future work stems from different needs. It is worth investigating how to
incorporate other distribution functions to govern probabilistic choices
(including concurrency/interleaving in events) in Event-B models. As shown in
§3.2, probabilistic rewrite theories can incorporate arbitrary probabilistic
distribution functions. Hence, the semantics proposed here can be used to
experiment with different alternatives and propose suitable extensions for
Event-B. Support for new operators and constructs (e.g., arbitrary types in
Cartesian products) could be included in a new version of the translation.
Furthermore, a plug-in to integrate the tool proposed here to Rodin is
currently under development. The framework presented here supports also non-
probabilistic Event-B models (see the bounded re-transmission protocol [1] in
the tool’s site whose only source of probabilistic behavior is the weight on
events). It will be interesting to investigate the use of symbolic techniques,
such as rewriting modulo SMT, for synthesis of parameters in Event-B
specifications (e.g., finding the range of values for constants that makes the
invariants true).

## References

  * [1] Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)
  * [2] Afendi, M., Laleau, R., Mammar, A.: Modelling hybrid programs with Event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) Proc. of ABZ. LNCS, vol. 12071\. Springer (2020)
  * [3] Agence Nationale de la Researche: The EBRP project. https://www.irit.fr/EBRP (2020)
  * [4] Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based Specification Language for Probabilistic Object Systems. ENTCS 153(2), 213–239 (May 2006)
  * [5] AlTurki, M., Meseguer, J.: PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool. In: Algebra and Coalgebra in Computer Science, vol. 6859, pp. 386–392. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)
  * [6] Aouadhi, M.A., Delahaye, B., Lanoix, A.: A Fully Probabilistic Extension of Event-B. Research report, LINA-University of Nantes (Jan 2016)
  * [7] Aouadhi, M.A., Delahaye, B., Lanoix, A.: Moving from Event-B to Probabilistic Event-B. Research report, LINA-University of Nantes (2016)
  * [8] Aouadhi, M.A., Delahaye, B., Lanoix, A.: Introducing probabilistic reasoning within Event-B. Softw. Syst. Model. 18(3), 1953–1984 (2019)
  * [9] Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.: The landing gear case study: challenges and experiments. Int. J. Softw. Tools Technol. Transf. 19(2), 133–140 (2017)
  * [10] Braga, C., Martí-Oliet, N.: B Maude: A formal executable environment for abstract machine notation descriptions. CoRR abs/2108.07878 (2021)
  * [11] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework, LNCS, vol. 4350. Springer (2007)
  * [12] Clavel, M., Durán, F., Martí-Oliet, N.: Polytypic programming in Maude. In: Proc. of WRLA. ENTCS, vol. 36, pp. 339–360. Elsevier (2000)
  * [13] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)
  * [14] Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)
  * [15] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
  * [16] Meseguer, J.: Twenty years of rewriting logic. Journal of Logic and Algebraic Programming 81(7-8), 721–781 (Oct 2012)
  * [17] Olarte, C., Osorio, D., Rocha, C.: EventB2Maude. https://github.com/carlosolarte/EventB2Maude (2022)
  * [18] Tarasyuk, A., Troubitsyna, E., Laibinis, L.: Integrating stochastic reasoning into Event-B development. Formal Aspects Comput. 27(1), 53–77 (2015)