Neeraj Peter Rivière
email: peter.riviere@toulouse-inp.fr

Kumar Singh

Yamine Aït-Ameur
email: yamine.aitameur@toulouse-inp.fr

EB4EB: A Framework for Reflexive Event-B

Keywords: Reflection, refinement and proof, meta-models, model instantiation, new proof obligations, theories, Event-B

Event-B is a correct-by-construction rigorous statebased method offering features for formal modelling and proof automation. An inductive proof schema allows to prove system properties, in particular invariants.In the current setup, verifying other properties such as deadlock-freeness, reachability, event scheduling, liveness, etc., requires adhoc modelling.These properties can be established partially using model checkers or by using third party interactive provers.Other crucial aspects, such as deadlock-freeness, are difficult to express. The availabilty of a meta-modelling mechanism for explicit manipulation of Event-B concepts would allow to deal with higher order modelling concepts and to define generic properties and associated proof obligations.

In this paper, we propose EB4EB, an Event-B based modelling framework allowing to manipulate Event-B features explicitly based on meta modelling concepts. This framework relies on a set of Event-B theories defining data-types, operators, welldefined conditions, theorems and proof rules. It preserves the core logical foundation, including semantics, of original Event-B models. Based on the instantiation of the introduced features at meta level, deep and shallow modelling approaches are proposed to exploit this framework. In addition, a case study is developed to demonstrate the use of our framework applying the deep and shallow embedding approaches. The whole framework is supported by the Rodin platform handling Event-B models and proofs.

I. INTRODUCTION

Motivation. Metamodelling is an engineering activity offering the capability to describe the core abstraction and properties to which models must adhere together with model analysis techniques. It has been widely adopted in the field of software engineering, particularly in model-driven engineering. Nowadays, formal methods have adopted such metamodelling techniques for developing theories axiomatising metamodels to represent higher level reasoning concepts used in the specification, development and verification of complex systems [START_REF] Bertot | Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions[END_REF], [START_REF] Fallenstein | Proof-producing reflection for HOL -with an application to model polymorphism[END_REF], [START_REF] Muñoz | Structural embeddings: Mechanization with method[END_REF], [START_REF] Sozeau | The MetaCoq Project[END_REF].

Event-B [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] is a state-based formal method supporting the development of complex systems following a correct-byconstruction approach. It is based on set theory and first-order logic, and it uses the Rodin [START_REF] Abrial | Rodin: an open toolset for modelling and reasoning in Event-B[END_REF] integrated development environment. Currently, the core modelling features of the Event-B language enable abstract system modelling as state-transitions systems, refinement based development, and interactive and automatic proofs. There are also a number of other RODIN plugins available to help with other modelling requirements, such as composition/decomposition [START_REF] Silva | Shared Event Composition/Decomposition in Event-B[END_REF], Theory plug-in [START_REF] Abrial | Proposals for mathematical extensions for Event-B[END_REF], [START_REF] Butler | Mathematical extension in Event-B through the Rodin theory component[END_REF], code generation [START_REF] Fürst | Code Generation for Event-B[END_REF], [START_REF] Méry | Automatic code generation from Event-B models[END_REF] etc.

Among these plugins, the Theory plug-in [START_REF] Abrial | Proposals for mathematical extensions for Event-B[END_REF], [START_REF] Butler | Mathematical extension in Event-B through the Rodin theory component[END_REF] offers powerful means to extend Event-B enabling for the development of additional data types, theories, and operators to extend the core modelling concepts and features of Event-B. For example, Dupont et al. [START_REF] Dupont | Event-b hybridation: A proof and refinement-based framework for modelling hybrid systems[END_REF], [START_REF] Dupont | Formally verified architecture patterns of hybrid systems using proof and refinement with event-b[END_REF] have developed a set of theories to integrate continuous features in the Event-B modelling language for modelling differential equations.

Currently, Event-B framework only offers standard proof obligations (POs) that are generated automatically: invariant preservation, theorems proofs, variant decreasing, event feasibility, guard strenghtening, etc. For additional verifications, such as deadlock freeness, liveness, reachability, and domain specific properties, the designer relies on other tools based on interactive proof systems and model checkers. They require ad hoc modelling from the designer for each formalised model. There is a lack of access and explicit manipulation of Event-B concepts, thus it is impossible to express generic properties at a higher order level associated with extra reusable POs in a theory that permits automatic generation of such POs for any designed model. Our claim. We claim that it is possible to express additional POs schemas using meta-modeling techniques without changing Event-B or Rodin, to automatically generate new POs for each Event-B model. Our contribution. This paper proposes an Event-B-based modelling framework, EB4EB, that allows for the explicit manipulation of Event-B features using meta modelling concepts. To cover Event-B modelling language semantics, this framework relies on a set of Event-B theories that define data-types, operators, well-defined conditions, theorems, and proof rules. It allows for the manipulation of static and dynamic aspects of Event-B modelling features, to encode new proof obligations related to other types of properties once and for all. Deep and shallow modelling approaches are proposed to exploit this framework based on the instantiation of the introduced features at the meta level. In addition, a case study demonstrating the use of our framework using the deep and shallow embedding approaches is developed. The Rodin platform, which handles Event-B models and proofs, underpins the entire framework.

As far as we know, this is the only reflection framework in the Event-B language that allows explicit meta-level manipulations of Event-B concepts, including the support of higher level reasoning mechanisms by defining datatypes, operators, well-definedness, and new POs in theories.

Organisation of the paper. This paper is organised as follows. Section II presents related work and the core concept of Event-B language is described in Section III. Sections IV describes EB4EB framework. Section V illustrates the development of meta-theories for Event-B. In Section VI, we present an application of the Event-B meta-theories by applying deep and shallow embedding on the clock model. We demonstrate a new reasoning mechanism related to deadlock freeness in Section VII. In Section VIII, we provide an assessment and Section IX concludes the paper with future work.

II. RELATED WORK

When two languages have the same or different semantics, one language can be mechanized into another by embedding the source logic of the first modelling language into the host modelling language. Deep and shallow embeddings are two widely used methods. Deep embedding describes explicitly the semantics and syntax of the source language in the host logic, whereas shallow embedding simply translates the semantics of the source language in the host logic [START_REF] Boulton | Experience with embedding hardware description languages in HOL[END_REF] (i.e. the translator carries the semantics). Both approaches have their own pros and cons. Deep embedding requires more modelling effort to address structural and semantic elements of the source language. As a result, while this approach may be difficult to grasp and tedious, it offers full access, in the host logic, to the elements of the source modelling language for formal verification. On the other hand, the shallow embedding approach is straightforward and easy to use once the semantics of the source modelling language is encoded in the modelling language transformation. It leads to a limited access to the source modelling language constructs for formal verification, in particular when tracing verification results (e.g. counterexamples). Munoz et al. [START_REF] Muñoz | Structural embeddings: Mechanization with method[END_REF] proposed a structural embedding approach in which only the language structure is deep/shallow embedded in the host logic and the source language expression is replaced by the host logic expression.

There are few formal modelling languages that allow for abstract reasoning about models characteristics while also working on concrete models. In our case, the source and host modelling languages are the same (i.e. Event-B); it is a reflexive relationship. Such work has already been carried out in various formal techniques, such as in Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions[END_REF] with the syntactic representation of Coq in Coq with Template Coq [START_REF] Anand | Towards certified meta-programming with typed template-coq[END_REF] and the semantics in MetaCoq [START_REF] Sozeau | The MetaCoq Project[END_REF]. Similarly, a reflection API has been developed in Agda [START_REF] Van Der | Reflection in Agda[END_REF], HOL [START_REF] Fallenstein | Proof-producing reflection for HOL -with an application to model polymorphism[END_REF], Idris [START_REF] Christiansen | Elaborator reflection: Extending idris in idris[END_REF], and Lean [START_REF] Ebner | A metaprogramming framework for formal verification[END_REF] to automate and/or simplify the definition of tactics. Some of them are motivated by other factors such as code generation and meta-programming.

Here, we discuss some approaches for Event-B. In [START_REF] Mehta | Proofs for the Working Engineer[END_REF] [20], the authors provided a comprehensive description of the logic's syntax with a type discipline and the intended semantics, including soundness, for an untyped first-order fragment of logic. In [START_REF] Schmalz | The logic of event-b[END_REF], Event-B logic is defined in order to describe modelling components like guards and invariants, as well as to express and discharge proof obligations. In this work, the abstract syntax of Event-B, including the concepts of theory and proof, is provided as a three-valued semantics in terms of a shallow embedding in Isabelle/HOL. Note that the above mentioned work mainly address the semantics of Event-B modelling components, whereas our work targets the verification of important properties such as liveness, deadlock freeness, and event scheduling, among others, by developing meta-modelling concepts in order to manipulate Event-B concepts using deep and shallow embedding. In addition, it is developed in the Even-B language itself, using Event-B theories expressed using the Theory plugin.

III. EVENT-B

Event-B [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF] method is based on set theory and first order logic (FOL). It relies on a powerful state-based modelling language where a set of events models state changes.

A. Event-B Contexts and Machines

Contexts (Tables I(a)) describe all the static elements of the models through the definition of carrier sets s, constants c, axioms A and theorems T ctx .

Context

Machine Refinement I(b)) describe model behaviour. It consists of Variables x, Invariants I(x), Theorems T mch (x) and Variants V (x). It defines a transition system represented as a set of guarded events evt recording state changes using a Before-After Predicates (BAP ). Events which decrease the variant are tagged as convergent otherwise they are ordinary. Invariants I(x) and Theorems T mch (x) ensure safety properties, while Variant V (x) ensures convergence properties for convergent events.

CONTEXT Ctx MACHINE M A MACHINE M C SETS s SEES Ctx REFINES M A CONSTANTS c VARIABLES x A VARIABLES x C AXIOMS A INVARIANTS I A (x A ) INVARIANTS THEOREMS T ctx THEOREMS T mch (x A ) J(x A , x C ) ∧ I C (x C ) END VARIANT V (x A ) EVENTS EVENTS EVENT evt C EVENT evt A REFINES evt A ANY α A ANY α C WHERE G A (x A , α A ) WHERE G C (x C , α C ) THEN WITH x A :| BAP A ( x A′ , α A : W (x A′ , α A , α A , x A , x A ′ ) x A , α C , x C , x C ′ ) END THEN END x C :| BAP C ( α C , x C , x C ′ ) END END (a) (b) (c)
(1) Theorems (THM) -Core Well-definedness (WD). The WD POs are associated to all built-in operators of the Event-B modelling language. Once proved, these WD conditions are used as hypotheses to prove other POs related to invariants, theorems, feasibility, etc.

A ⇒ TctxA ∧ I A (x A ) ⇒ T mch (x A ) (2) Initialisation (INIT) A ∧ G A (α A ) ∧ BAP A (α A , x A′ ) ⇒ I A (x A′ ) (3) Invariant A ∧ I A (x A ) ∧ G A (x A , α A ) preservation (INV) ∧BAP A (x A , α A , x A′ ) ⇒ I A (x A′ ) (4) Event A ∧ I A (x A ) ∧ G A (x A , α A ) feasibility (FIS) ⇒ ∃x A′ • BAP A (x A , α A , x A′ ) (5) Variant A ∧ I A (x A ) ∧ G A (x A , α A ) progress (VAR) ∧BAP A (x A , α A , x A′ ) ⇒ V (x A′ ) < V (x A ) TABLE II: Machine Proof obligations (6) Event A ∧ I A (x A ) ∧ J(x A , x C ) ∧ G C (x C , α C ) Simulation ∧W (α A , α C , x A , x A′ , x C , x C′ ) (SIM) ∧BAP C (x C , α C , x C′ ) ⇒ BAP A (x A , α A , x A′ ) (7) Guard A ∧ I A (x A ) ∧ J(x A , x C ) Strengthening ∧W (α A , α C , x A , x A′ , x C , x C′ ) (GRDS) ∧G C (x C , α C ) ⇒ G A (x A , α A )

B. Event-B extensions with Theories

END

TABLE IV: Global structure of Event-B Theories

In order to handle more complex modelling concepts not supported by native Event-B, an extension of Event-B based on the mathematical definitions has been proposed in [START_REF] Abrial | Proposals for mathematical extensions for Event-B[END_REF], [START_REF] Butler | Practical theory extension in Event-B. In Theories of Programming and Formal Methods -Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday[END_REF]. This extension, like Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-order Logic[END_REF] or PVS [START_REF] Owre | PVS: A prototype verification system[END_REF], allows to define new theories by introducing new datatypes, operators, theorems and proof rules. They can be further used in the core development of Event-B models.

-Theory description. Table IV shows core modelling elements for developing new theories. The core modelling elements are classified in different clauses known as datatypes, operators, axiomatic definitions, axioms, theorems and proof rules. A theory can be parameterized by Type in the clause TYPE PARAMETERS. The description of the data-type, operator, theorems and proof rules use the type parameters. Datatypes (DATATYPES clause) can be defined with constructors, and each constructor can have some destructors. Note that the destructors can also have inductive definition.

A theory may contain several operators of different nature (<nature> tag), expression or predicate. These new defined operators extend the capabilities of the Event-B core language and can be used directly in core modelling components like expression and predicate. Operators may be defined in two ways. First, explicitly in the direct definition clause where the operator is equivalent to an expression, and second, axiomatically in the AXIOMATIC DEFINITIONS clause where the behaviour of the operator is expressed by a set of axioms. Last, a theory defines a set of theorems proven with the help of defined operators and axioms.

Many theories have been defined for sequences, lists, groups, reals, differential equations, and so on [START_REF] Butler | Practical theory extension in Event-B. In Theories of Programming and Formal Methods -Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday[END_REF], [START_REF] Dupont | Event-b hybridation: A proof and refinement-based framework for modelling hybrid systems[END_REF].

-Well-definedness (WD) in Theories. For each defined operator, a useful clause is well-definedness (WD) conditions. This clause ensures that the definition is correct. A WD proof obligation is generated when the operators are used in an Event-B expression. A correct definition is related to mathematical correctness, but it is also related to any other condition necessary if the operators guarantee some properties.

All the WD POs and theorems are proved using the Event-B proof system.

-Event-B proof system and its IDE Rodin. The theories extension for Event-B is available as a plug-in. Theories are tightly integrated in the proof process. Depending on their definition (direct or axiomatic), operator definitions are expanded either using their direct definition (if available) or by enriching the set of axioms (hypotheses in proof sequents) using their axiomatic definition. Theorems can be imported as hypotheses and used in proofs just like any other theorem. The proof system is partially automatic, the other parts are interactive. Many tools are available to help the proof like predicate provers or SMT solver.

IV. OUR FRAMEWORK

The primary objective of the developed framework is to offer the capability to explicitly manipulate Event-B features as first-order objects.

A. Methodology

For this purpose, we define a three steps methodology. At the first step, we rely on the definition of Event-B theories describing states and events as data-types associated to a set of operators allowing to manipulate them. In addition, a couple of axioms defining these operators are introduced. These axiomatic definitions formalise the state-based semantics of Event-B models (contexts and machines). Finally a set of proven theorems are given. They formalise relevant properties on states, events and operators. The result of this step is a Meta-theory for Event-B defined once and for all.

In the second step, any specific Event-B model is obtained by instantiating the above mentioned theory to define states, events and related properties. Two possible instantiations are identified: shallow and deep embeddings.

Last, the third step entails proving the correctness of the instantiated models, i.e. proving that models are well-defined, invariants and theorems of the specific Event-B model hold, and other user expressed properties are true. In the meantime, the theorems of the theory are instantiated as well, they are useful for the proofs as they provide, for free, additional hypotheses.

B. Deep or Shallow modelling

As depicted in Figure 1, once the Event-B Metatheory(D.1&S.1) is described, Event-B models are described following two approaches.

1) Deep embedding (see Figure 1a): It consists in defining machine instances as an Event-B context (D.2) where the generic type parameters of the meta-theory are instantiated by sets describing machines state variables and events. Similarly, all Event-B machine constructs such as event guards and before-after predicates, invariants, theorems and so on are formalised. They are defined using the operators introduced in the Meta-theory. This instantiation generates two kinds of POs. First, it generates the WD POs for each operator application to ensure that the Event-B machine is well-defined. Second, the POs related to the predicate operators that define machine consistency like invariant preservation, variant decreasing corresponding to WD POs are produced.

These obtained POs are proved using the Event-B Rodin theorem prover or other theorem provers.

2) Shallow embedding (see Figure 1b): In shallow embedding, an additional generic machine (S.2) is defined at the meta-theory level. In the same line of TLA + [START_REF] Lamport | Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers[END_REF] this machine formalises the behavioural semantics of Event-B. Using the meta-theory features, this machine defines abstract state variables and two abstract events Init and Progress recording respectively state variables initialisation and state transitions. Then, instantiation is defined using the native Event-B refinement where the first Init event is refined using the initialisation after-predicate and second for each event of the concrete machine (model), the Progress event is refined using the before-after predicates issued from the meta-theory. Note that the Progress is a collection of ordinary and convergent events used directly in the generic abstract model.

In this case, unlike from the deep modelling approach, proving the generated proof obligations relies on the Event-B inductive principle introduced by this generic machine.

Our framework provides meta-theory for deep modelling (D.1) and shallow modelling (S.1), and an abstract machine for shallow instantiation (S.2). Deep instantiation (D.2) and shallow instantiations (S.3 and S.4) need to be developed by users.

All of the developments presented in this paper can be found on http://singh.perso.enseeiht.fr/ Conference/ICECCS2022/EB4EB_Models.pdf.

V. META-THEORIES FOR EVENT-B

In this section, we describe the development of metatheories by defining data-types and operators ensuring welldefined conditions and proofs. This development allows to Fig. 1: EB4EB framework define different Event-B modelling components as first-order objects that can be accessed and manipulated using the defined data-types and operators. Note that the given definition for modelling components are derived from the Event-B book [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF].

Listings 1, 2, 3 and 4 show meta-theory structure that can include several elements as follows:

A. Type Parameters and Datatypes

The Event-B meta-theory EvtBTheo introduces two polymorphic type parameters ST AT E and EV EN T in the TYPE PARAMETERS clause (see Listing 1). These parameters are similar to carrier sets in contexts. The first attempt to represent the variables is with the type parameter ST AT E. An explicit description of each variable is not required at this abstract level. In fact, the type parameter ST AT E abstracts the state as a cartesian product of all variables. At instantiation step, this abstract type is replaced with concrete variables of the considered Event-B model. The second type parameter EV EN T is used to abstract the label of events. These type parameters are used in the definition of a new datatype M achine in the DATATYPES clause. A constructor Cons_machine is defined in the CONSTRUCTOR clause associated to destructors, i.e, Event, State, Init and so on, to represent and to access different constituents of Event-B components. All these destructors define accesses for: Event -machine events; State -machine states; Init -initialisation event; V ariant -machine variants; Convergent -convergent events; Ordinary -ordinary events; AP -after-predicates; BAP -before after-predicates; Grd -event guards; Invmachine invariants; and T hm -machine theorems.

In our approach, we express the semantics of Event-B models and we use set comprehension to express different modelling components using ST AT E and EV EN T . For example, Invariant is defined as a set of states that satisfy a set of properties. We also use quantification to express event parameters in the set comprehension's predicate. Listing 1: Machine Data-type (D.1&S.1)

B. Theory operators

In the Event-B meta-theory, EvtBTheo, we introduce several operators to manipulate the modelling objects as well as checking the well-defined conditions.

1) Manipulation operators: Listing 2 shows a list of manipulation operators. We introduce isInit, isProgress, and Progress operators. isInit is declared as a prefix operator with two arguments represented by machine m and event e. In terms of existing expression language, the direct definition clause defines the predicate e = Init(m). Similarly, another isProgress prefix operator is declared with two arguments, machine m and event e. Its direct definition clause, expressed as a predicate, states that the predicate holds if the event e is not the initialisation event and is a progress event of the machine m. The last operator Progress is declared as prefix operator with one argument machine m. Its direct definition clause is the expression Event(m) \ Init(m) identifying a set of progress events. Note that our defined operators handle the ordinary and convergence events. 2) Well-defined operators: The DATATYPES clause defines a constructor and destructors to access the Event-B modelling components. These destructors contain typing information only and may lead to be an ill-defined datatype definition. For example, the BAP destructor is a relation between events and states, but the initialisation event is not one of the events of this before-after relation. In order to avoid such ill-defined typing definitions, we introduce a set of new operators in Listing 3 equipped with WD conditions. Due to space constraints, we only show an extract of the set of well-defined operators.

In Listing 3, the first well-defined operator BAP_WellDefined is declared with one argument machine m, and its direct definition shows that all events in the domain of the BAP relation are progress events, implying that the event set contains no initialisation event. The next well-defined operator Grd_WellDefined is also defined with single machine m argument. Its direct definition states that all events in the domain of the Grd relation are progress events. To check the well-defined condition of Init operator, the Init_WellDefined operator is declared. Its direct definition states that the initialisation event belongs to machine events and is an ordinary event. The direct definition of the next Variant_WellDefined operator shows that all the states belonging to the variant states are convergent and identified from the set of invariant states, i.e. each variant state element is associated with an integer. Note that the variant is a total function in the invariant states. The direct definition of the Tag_Event_WellDefined operator shows that the union of convergent and ordinary events are equal to the progress events, and are exclusive sets of events. The last Machine_WellDefined operator is important; the direct definition shows the conjunction of all other well-defined operators. It represents the global well-defined condition associated with an Event-B machine m.

3) Proof obligation operators: Once the notion of machine is defined, the last set of operators deal with the explicit definition of Event-B POs (see Listing 4). They help to discharge the generated proof obligations as given in Section II, such as INV, FIS, NAT and VAR. Their definitions are inductive as they apply on the initialisation and then on all other events.

All guarantees that if invariants and guards hold, then the BAP decreases the variant associated with the convergent event e. The WD clause defines other well-defined operators to ensure the correctness as well as the required WD conditions for the variants. Similarly, the operator All_Convergent_VAR generalises the definition of convergence, it checks the required properties for all convergent events of machine m. Then, the next two operators, Mch_NAT and All_Convergent_NAT, define a variant for an event e as a natural number and all convergent events have a natural number as variant, respectively.

The predicate operator, Machine_PO is the most important. It allows to generate, thanks to the WD PO mechanism, all possible POs related to a machine. Its direct definition is the conjunction of all the other PO operators related to Event-B constituents previously defined. Its welldefinedness clause uses the Machine_WellDefined operator. This operator is associated to the last defined operator check_Machine_WellDefined ensuring that all the destructors are well-defined and the machine satisfies POs. Observe that there is no direct definition for this operator as it shall always be true ⊤. The well-definedness clause contains the required condition that allows to check the machine welldefinedness and machine POs together. When this operator is used, it generates a PO for this WD condition.

VI. APPLICATION OF EVENT-B META-THEORIES

In this section, we describe a simple case study, the clock, to demonstrate how our developed meta models can be applied.

A. Case Study: The Clock

The main functionalities (FUN) and requirements (REQ) of the clock case study are given as follows:

• FUN1 A minute can progress • FUN2 An hour can progress • REQ1
The hours are represented in a 24-hour format.

• REQ2 The clock must converge on midnight.

• REQ3 The clock never stops. In Listing 5, we describe the clock model that is formalised in native Event-B language. In this model, two variables are defined, minute m and hour h, in inv1 -inv2. Two safety properties are introduced in inv3 -inv4. The first safety property (REQ1) states that the minute m is always less than 60 and hour h is less then 24. The next safety property (REQ3) is defined as a theorem that is a disjunction of all guards to state that the clock never stops means always the guard of at least one event is true. The last safety property (REQ2) is related to convergence (variant) expressed by the number 24 * 60 -1 -(m + h * 60). In this model, we introduce three events: tick min -to model the minute progress by 1; tick hour -to model the hour progress by 1; and tick midnight -to reset the clock at midnight. The required guards are added in the defined events to update the minute m and hour h.

MACHINE C l o c k VARIABLES m , h INVARIANTS i n v 1 -2 : m ∈ N ∧ h ∈ N i n v 3 -4 : m < 60 ∧ h < 24 THEOREMS thm1 : m < 59 ∨ (m = 59 ∧ h < 23) ∨ (m = 59 ∧ h = 23) VARIANT 24 * 60 -1 -(m + h * 60) EVENTS INITIALISATION THEN a c t 1 : m, h :| m ′ = 0 ∧ h ′ = 0 END tick

B. Deep embedding of the clock model

We describe the development of the clock case study using the deep modelling instantiation technique of Section IV-B using the meta-theory introduced in Section V. All constituents of the Clock model are explicitly expressed in terms of the EvtBTheo Meta-theory constructs. The Clock Event-B model is represented as an Event-B context, and POs are described either as theorems or as well-definedness POs.

The deep modelling resulting context of the Event-B clock model given in Listing 5 is presented in Listing 6. In this context, a set Ev lists all the clock events in axm1. The clock machine clock is defined by axiom axm2 as a member of M achine(Z × Z, Ev), where the first argument defines machine state as Z × Z and the second one machine events Ev. Furthermore, three axioms (axm3 -axm5) are used to instantiate Event with the enumerated set Ev, Init with the event label init, and State with Z × Z.

CONTEXT C l o c k D e e p I n s t a n c e SETS Ev CONSTANTS c l o c k , t i c k m i n , t i c k h o u r , t i c k m i d n i g h t , i n i t AXIOMS

axm1 : partition(Ev , {init}, {tick midnight}, {tick hour }, {tick min}) axm2-3

: clock ∈ Machine(Z × Z, Ev ) ∧ Event(clock ) = Ev axm4-5 : Init(clock ) = init ∧ State(clock ) = Z × Z axm6 : Thm(clock ) = {m → h | m < 59 ∨ (m = 59 ∧ h < 23) ∨ (m = 59 ∧ h = 23)} axm7 : Inv (clock ) = {m → h | m ∈ N ∧ h ∈ N ∧ m < 60 ∧ h < 24} axm8 : AP(clock ) = {m → h | m = 0 ∧ h = 0} axm9 : BAP(clock ) = {t → ((m → h) → (mp → hp)) | (t = tick min ∧ = m + 1 ∧ hp = h)∨ (t = tick hour ∧ mp = 0 ∧ hp = h + 1)∨ (t = tick midnight ∧ mp = 0 ∧ hp = 0)} axm10 : Grd(clock ) = {t → (m → h) | (t = tick min ∧ m < 59)∨ (t = tick hour ∧ m = 59 ∧ h < 23)∨ (t = tick midnight ∧ m = 59 ∧ h = 23)} axm11 : Convergent(clock ) = {tick min, tick hour } axm12 : Ordinary(clock ) = {tick midnight, init} axm13 : Variant(clock ) = {m → h → v | v = 24 * 60 -1 -(m + h * 60)} THEOREMS thm1 : check Machine WellDefined(clock ) END Listing 6: A deep instance of the clock machine (D.2)
The next two axioms (axm6 and axm7) are defined to instantiate theorem T hm and invariant Inv using comprehensive sets derived from thm1 and inv1 -inv4 of Listing 5. Axiom axm8 instantiates the after-predicate AP derived from the action of the initialisation event (act1) in the Clock machine. Similarly, axioms axm9 and axm10 are used to instantiate the before-after predicate BAP and the guard Grd with a set of actions and guards of all events derived from the Clock machine using comprehensive sets. The next axioms axm11 -axm12 instantiate the Convergent and Ordinary with a list of convergent and ordinary events, respectively. In this model, we have only two convergent events tick min and tick hour and two ordinary events init and tick midnight. Axiom axm13 is used to instantiate the V ariant with the defined variant of the Clock model. Machine correctness. It is important to note the introduction of a theorem thm1 to invoke the check M achine W ellDef ined operator, which is used to check the welldefinedness and POs generation of the Clock machine. This theorem shall be proved, it entails machine correctness.

C. Shallow embedding of the clock model

We describe the development of the clock case study using the shallow modelling instantiation technique of Section IV-B using the meta-theory introduced in Section V.

All constituents of the Clock model are explicitly expressed in terms of the EvtBTheo Meta-Theory constructs. The Clock Event-B model is represented as an Event-B context and machine, and POs are described either as theorems or as guard strengthening POs. It is inspired from shallow embeddings [START_REF] Boulton | Experience with embedding hardware description languages in HOL[END_REF] used in other interactive provers like Isabelle/HOL and PVS. In the same vein as the shallow embedding, we use the Event-B to preserve semantics and the supporting syntax. Thus, we describe an abstract Event-B model formalising the required properties for Event-B models correctness: a context for the static part and properties and a generic machine for the dynamic parts i.e. transitions represented by events.

1) Abstract generic model: Listings 7 and 8 show the context and machine of the Clock generic model. The context contains sets Ev and S for events and states. A constant machine is introduced as a member of M achine(S, Ev).

CONTEXT C l o c k S h a l l o w G e n SETS Ev , S CONSTANTS m a c h i n e AXIOMS

axm1 : machine ∈ Machine(S, Ev ) END Listing 7: A static element of abstract machine (S.2) In the generic machine model, we declare two variables s and InitDone in invariants inv1 -inv2. These variables are set in the INITIALISATION event. To ensure that the invariant is satisfied, we introduce a new invariant inv3. In this model, we define three events Do_Init, Do_Ordinary, and Do_Convergent whose actions modify the state using the AP and BAP operators (act1). The first event is used to initialise state variables in actions (act1 -act2). Its guards ensure that InitDone is F ALSE (grd1), and the feasibility and invariants hold for the Init event. The Do_Ordinary event updates the machine state s for an event e annotated as Ordinary. Its guards state that InitDone is TRUE; the machine state s belongs to Grd of e (grd2); the event e is a progress and ordinary event (grd3 -grd4); and feasibility and invariant properties of machine hold for the event e (grd5 -grd6). Similar to the ordinary event, the last event Do_Convergent contains additional guards grd3 to tag the event e as convergent and grd7 -grd8 to ensure that the variant properties of machine for the event e hold.

Note that our generic abstract model contains initialisation, ordinary and convergent events, whereas we may only have initialisation and progress events, in the same of spirit of TLA + , where the progress event can be refined by ordinary and convergent events later in further refinement. Static constituents. In the context of Listing 9, we define a constant pr in axm1 as a bijection relation between (Z × Z) and S to maintain an exact correspondence between abstract and concrete states. We enumerate the set Ev with clock events in axm2. Axioms (axm3-axm5) are used to instantiate Event with enumerated set Ev, Init with the event init, and State with S. Axiom axm6 is defined to instantiate invariant Inv using comprehensive sets derived from Inv1 -inv4 of Listing 5. Variant of the clock machine is introduced in axm7. Then two axioms (axm8 -axm9) are used to instantiate Convergent and Ordinary with a set of convergent and ordinary events. The last axiom axm10 instantiates theorem concrete machine T hm derived from Listing 5. Context correctness. Four theorems thm1 -thm4 are introduced to check the POs associated with theorems, and well-definedness for variant and machine events (initial and tagged events). Once proved, these theorems guarantee that the context is well-defined and the required properties hold. Listing 9: Instances for static elements: clock machine (S.3) Dynamic constituents. The abstract machine is refined in Listing 10 to introduce the events of the Clock Event-B machine. In this model, we declare two new variables m and h and a gluing invariant inv1 to link (glue) concrete and abstract variables. No new event is added but each abstract event has been refined by concrete ones by providing concrete guards and actions. The newly introduced variables are set in the refined INITIALISATION event, and a witness is provided to map the abstract and concrete variables. In the Do_Init event, we introduce a new guard (grd2) to instantiate AP operator and a witness is provided for the state s ′ . The action of this event modifies the concrete clock variables m and h.

Inv (machine) = pr [{m → h | m ∈ N ∧ h ∈ N ∧ m < 60 ∧ h < 24}] axm7 : Variant(machine) = {s, v, m, h • s = pr (m → h)∧ v = (
The event Do_Convergent is refined by two concrete clock events Tick_min and Tick_hour, and the event Do_Ordinary is refined by the concrete event Tick_midnight. In Tick_min event, grd1 is similar to the abstract event, grd2 is updated according to the concrete variables m and h, and two new guards (grd3 -grd4) are added to instantiate Grd and BAP operators for tick min, respectively. In this event, two witnesses are provided for the abstract parameter event e and the state s ′ . The action of this event uses BAP operator to update concrete variables m and h. Note that the other refined events are similarly modeled by providing witnesses and appropriate instantiations. Machine correctness. Gluing invariant (inv1), witnesses and guard strengthening are introduced to check the POs associated with machine events (initial and tagged events). New generated POs are proved to guarantee that the machine is correct and the required properties hold. The complete development of meta theory, instantiations of deep and shallow clock models, and the Event-B clock model are available at http://singh.perso.enseeiht.fr/ Conference/ICECCS2022/EB4EB_Models.pdf. VII. NEW REASONING: DEADLOCK FREENESS Currently, modelling deadlock freeness (FUN1) is achieved manually by the model designer using an additional theorem stating that the disjunction of all events guards holds. Proceeding this way is error prone if the user does not write it correctly. Generating this theorem as a new PO would avoid the designer of the burden of writing this theorem.

MACHINE ClockShallowMac REFINES ClockShallowGenMac SEES C l o c k S h a l l o w VARIABLES m , h , InitDone INVARIANTS i n v 1 : s = pr (m → h) EVENTS INITIALISATION WITH s ′ : s ′ = pr (m ′ → h ′ ) THEN a c t 1 : m, h :| m ′ ∈ Z ∧ h ′ ∈ Z a c t 2 : InitDone := FALSE END Do Init REFINES Do Init WHERE g r d 1 : InitDone = F ALSE g r d 2 : pr[{ms → hs | ms = 0 ∧ hs = 0}] = AP (machine) WITH s ′ : s ′ = pr (m ′ → h ′ ) THEN a c t 1 : m, h :| pr(m ′ → h ′ ) ∈ AP (machine) a c
′ : s ′ = pr (m ′ → h ′ ) THEN a c t 1 : m, h :| pr(m ′ → h ′ ) ∈ BAP(machine)[{tick min}][{pr(m → h)}] END Tick hour REFINES Do Convergent . . .
Expressing such a PO (and others) at the Meta-theory level is possible provided that a specific operator with its WD condition is introduced. Listing 11 shows the formalisation of the PO_DeadlockFreeness operator in a theory extension EvtBTheoDeadlock. Then, checking the machine operator check_Machine_DeadLock is redefined so as to handle deadlock freeness in addition to the other WD conditions provided by check_Machine_WellDefined issued from the extended EvtBTheo. To generate the deadlock freeness PO for a concrete model, it is enough to state that predicate operator check_Machine DeadLock is a theorem in the context of the concrete model. V: Proof Statistics as expected, we observe that the clock model is automatically proved using Rodin provers. The proofs of correctness of the same case study using both deep and shallow modelling resulted in a greater number of proof obligations, some of them being proved interactively. Although the number of POs and interactive proofs are increasing, we believe that our framework offers two other complementary proving techniques (using deep and shallow instantiation) to the classical Event-B provers.

2) Deep and shallow modelling: In deep modelling, all Event-B concepts related to variables, events, guards, invariants, substitutions and so on are defined as instances of the developed meta-theory. For shallow modelling, a context and an abstract generic model instantiating the meta-theory with Event-B concepts are defined. They exploit the builtin inductive proof process offered by Event-B/Rodin. Both approaches allow us to double-check, based on different proof mechanisms, design decisions during system development.

Last, such approaches offer a shared format for Event-B models. Indeed, deep modelling style relies on first-order logic and set theory in contexts that can be exported to any other proof assistant, like Coq, PVS and Isabelle/HOL. For shallow modelling, export to other close modelling techniques like TLA is straightforward. Such export makes it possible to exploit other proof assistants than Event-B/Rodin.

3) Extensible framework: The EB4EB framework allows for the extension of the core reasoning mechanism of Event-B by including new POs defined as predicates in theories. Our theories for reflexive Event-B, for example, allowed us to reason about deadlock freedom, reachability, and so on. This capability makes Event-B/Rodin extensible as it can be enriched with additional POs not available in native Event-B.

IX. CONCLUSION

The EB4EB framework we presented allows users to manipulate Event-B features explicitly using reflection and metamodelling concepts. It relies on Event-B theories that define data-types, operators, WD, theorems, and proof rules to formalise the semantics of Event-B. The developed theories enable manipulation of the static and dynamic properties of Event-B, including new POs associated to deadlock freeness, liveness, reachability, composition/decomposition, and so on. Deep and shallow embedding are used to instantiate the defined theories of the EB4EB framework. Furthermore, the Rodin tools have been used to formalise the development of EB4EB-related activities. We have demonstrated the approach on the clock model developed in both core modelling language and deep and shallow modelling. Both deep and shallow instantiated clock models preserve the required safety properties and functional behaviour encoded in theories.

Note that the EB4EB modelling concepts are formalised once and for all, meaning that they are reusable and don't need to be proven again. However, these theories must be instantiated in new developments, and the generated WD POs must be discharged to check instantiation is correct.

The developed theories have been applied on several case studies to assess the expressiveness, effectiveness, portability, and scalability of our approach. Our future goal is to analyse and identify Event-B refinement operations and its semantics to be included in the EB4EB framework. We plan to deploy the EB4EB framework to enhance and extend the reasoning mechanism by supporting other externally defined POs. In particular, we target the definition of domain specific POs issued from domain specific analyses of Event-B models, like continuous behaviours, human machine interaction, and so on. Analyzing and certifying existing plug-ins, such as code generation and composition/decomposition, is on the agenda. Our long-term goal is to use Dedukti [START_REF] Boespflug | Dedukti: A Universal Proof Checker[END_REF] to import/export the Event-B theory and models into proof assistants like Coq, PVS and Isabelle/HOL using the deep modelling approach.

1 :

 1 T 1 , ...) OPERATORS Op1 <nature> (p 1 : T 1 , ...) well-definedness WD(p 1 , ...) direct definition D 1 AXIOMATIC DEFINITIONS TYPES A 1 , ... OPERATORS AOp2 <nature> (p 1 : T 1 , ...): Tr well-definedness WD(p 1 , ...) AXIOMS A 1 , ... THEOREMS T 1 , ...

  Rodin 1 is an open source Eclipse-based Integrated Development Environment for modelling in Event-B. It offers resources for model editing, automatic PO generation, project management, refinement and proof, model checking, model animation and code generation.

  (a) Deep Modelling (b) Shallow Modelling

OPERATORS isInit <p rListing 2 :

 2 e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : EV EN T ) d i r e c t d e f i n i t i o n e = Init(m) isProgress <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : EV EN T ) d i r e c t d e f i n i t i o n ¬isInit(m, e) ∧ e ∈ Event(m) Progress <e x p r e s s i o n > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n Event(m) \ {Init(m)} Destructor operator of Data-type (D.1&S.1)

BAP

  WellDefined <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n dom(BAP (m)) = P rogress(m) Grd WellDefined <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n dom(Grd(m)) = P rogress(m) Init WellDefined <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n Init(m) ∈ Event(m) ∧ Init(m) ∈ Ordinary(m) Variant WellDefined <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n Inv(m) ◁ V ariant(m) ∈ Inv(m) → Z Tag Event WellDefined <p r e d i c a t e > (m : M achine(EV EN T, ST AT E)) d i r e c t d e f i n i t i o n Convergent(m) ∪ Ordinary(m) = Event(m)∧ Convergent(m) ∩ Ordinary(m) = ∅ Machine WellDefined <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n BAP W ellDef ined(m)∧ Grd W ellDef ined(m)∧ Init W ellDef ined(m)∧ T ag V ariant W ellDef ined(m)∧ V ariant W ellDef ined(m) Listing 3: Operator of well defined Data-type (D.1&S.1)

  the defined operators have a machine m as argument. The first declared operator Mch_THM shows that the invariants are a subset of theorems. The next two operators, Mch_FIS_Init and Mch_FIS, represent the base case and induction case for the feasibility POs, respectively. The direct definition for the induction case ensures that the invariants and guards of the progress event e are a subset of the domain of the BAP of e. Similarly, the next three predicate operators, Mch_INV_Init, Mch_INV and All_Progress_INV, define the initialisation, the induction case of the invariant PO for a single event e, and the induction case of invariant properties for all progress events, respectively. The direct definition of Mch_INV ensures that BAP of progress event e preserves the invariants if guards and invariants are true before. The next two operators Mch_VARIANT and All_Convergent_VAR are declared to represent convergent properties. The Mch_VARIANT definition

MchListing 4 :

 4 THM <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n Inv(m) ⊆ T hm(m) Mch FIS Init <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n Inv(m) ∩ AP (m) ̸ = ∅ Mch FIS <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : Event) w e l l -d e f i n e d n e s s e ∈ P rogress(m) d i r e c t d e f i n i t i o n Inv(m) ∩ Grd(m)[{e}] ⊆ dom(BAP (m)[{e}]) All Progress Mch FIS <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n ∀e • e ∈ P rogress(m) ⇒ M ch F IS(m, e) Mch INV Init <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n AP (m) ⊆ Inv(m) Mch INV <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : EV EN T ) w e l l -d e f i n e d n e s s e ∈ P rogress(m) d i r e c t d e f i n i t i o n BAP (m)[{e}][Inv(m) ∩ Grd(m)[{e}]] ⊆ Inv(m) All Progress INV <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n ∀e • e ∈ P rogress(m) ⇒ M ch IN V (m, e) Mch VARIANT <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : EV EN T, s : ST AT E) w e l l -d e f i n e d n e s s V a r i a n t W e l l D e f i n e d (m) , A l l P r o g r e s s I N V (m) , BAP WellDefined (m) , T a g V a r i a n t W e l l D e f i n e d (m) , e ∈ Convergent(m)∧ s ∈ State(m) ∧ s ∈ Inv(m) ∧ s ∈ Grd(m)[{e}] d i r e c t d e f i n i t i o n ∀sp • sp ∈ BAP (m)[{e}][{s}] ⇒ (Inv(m) ◁ V ariant(m))(s) > (Inv(m) ◁ V ariant(m))(sp) All Convergent VAR <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) w e l l -d e f i n e d n e s s V a r i a n t W e l l D e f i n e d (m) , A l l P r o g r e s s I N V (m) , BAP WellDefined (m) , T a g V a r i a n t W e l l D e f i n e d (m) d i r e c t d e f i n i t i o n ∀e, s • e ∈ Event(m) ∧ e ∈ Convergent(m)∧ s ∈ State(m) ∧ s ∈ Inv(m) ∧ s ∈ Grd(m)[{e}] ⇒ M ch V ARIAN T (m, e, s) Mch NAT <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : EV EN T ) w e l l -d e f i n e d n e s s e ∈ Convergent(m) d i r e c t d e f i n i t i o n V ariant(m)[Inv(m) ∩ Grd(m)[{e}]] ⊆ N All Convergent NAT <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n V ariant(m)[Inv(m) ∩ Grd(m)[Convergent(m)]] ⊆ N Machine PO <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) w e l l -d e f i n e d n e s s M a c h i n e W e l l D e f i n e d (m) d i r e c t d e f i n i t i o n M ch T HM (m) ∧ M ch F IS Init(m) ∧ M ch IN V Init(m)∧ All P rogress M ch F IS(m) ∧ All P rogress M ch IN V (m)∧ All Convergent M ch V ARIAN T (m)∧ All Convergent M ch N AT (m) check Machine WellDefined <p r e d i c a t e > (m : M achine(EV EN T, ST AT E)) w e l l -d e f i n e d n e s s M achine W ellDef ined(m) ∧ M achine P O(m) d i r e c t d e f i n i t i o n ⊤ Operator of well defined Data-type (D.1&S.1)

  min <c o n v e r g e n t> WHERE g r d 1 : m < 59 THEN a c t 1 : m :| m ′ = m + 1 END tick hour <c o n v e r g e n t> WHERE g r d 1 : m= 59 ∧ h < 23 THEN a c t 1 : m, h :| m ′ = 0 ∧ h ′ = h + 1 END tick midnight <o r d i n a r y > WHERE g r d 1 : m = 59 ∧ h = 23 THEN a c t 1 : m, h :| m ′ = 0 ∧ h ′ = 0 END ENDListing 5: A machine of clock Once the theory for Event-B concepts is designed, two main approaches to instantiate it are envisioned, namely deep modelling and shallow modelling as described below.

2 :

 2 MACHINE ClockShallowGenMacSEES C l o c k S h a l l o w G e n VARIABLES s , InitDone INVARIANTS i n v 1 -2 : s ∈ S ∧ InitDone ∈ BOOL i n v 3 : InitDone = TRUE ⇒ s ∈ Inv (machine) EVENTS INITIALISATION THEN a c t 1 : s :| s ′ ∈ S a c t 2 : InitDone := FALSE END Do Init WHERE g r d 1 : InitDone = FALSE grd2-3 : M ch F IS Init(machine) ∧ M ch IN V Init(machine) THEN a c t 1 : s :| s ′ ∈ AP(machine) a ct 2 : InitDone := TRUE END Do Ordinary ANY e WHERE grd1-InitDone = TRUE ∧ s ∈ Grd(machine)[{e}] grd3-4 : e ∈ P rogress(machine) ∧ e ∈ Ordinary(machine) grd5-6 : M ch F IS(machine, e) ∧ M ch IN V (machine, e) THEN a c t 1 : s :| s ′ ∈ BAP(machine)[{e}][{s}] END Do Convergent ANY e WHERE grd1-2 : InitDone = TRUE ∧ s ∈ Grd(machine)[{e}] grd3-4 : e ∈ P rogress(machine) ∧ e ∈ Convergent(machine) grd5-6 : M ch F IS(machine, e) ∧ M ch IN V (machine, e) g r d 7 : M ch V ARIAN T (machine, e, s) g r d 8 : M ch N AT (machine, e) THEN a c t 1 : s :| s ′ ∈ BAP(machine)[{e}][{s}] END END Listing 8: A generic abstract machine (S.2) 2) Concrete model: The concrete model refines the abstract generic model introduced above. The static elements of the clock model are described by the context of Listing 9 and dynamic elements are described in machine of Listing 10.

CONTEXT

  C l o c k S h a l l o w EXTENDS C l o c k S h a l l o w G e n CONSTANTS t i c k m i n , t i c k h o u r , t i c k m i d n i g h t , i n i t , p r AXIOMS axm1-2 : pr ∈ (Z × Z) ↣ → S ∧ State(machine) = S axm3-4 : Event(machine) = Ev ∧ Init(machine) = init axm5 : partition(Ev , {init}, {tick midnight}, {tick hour }, {tick min}) axm6 :

  24 * 60 -1 -(m + h * 60)) | s → v} axm8 : Convergent(machine) = {tick min, tick hour } axm9 : Ordinary(machine) = {tick midnight, init} axm10 : Thm(machine) = pr [{m → h | m < 59 ∨ (m = 59 ∧ h < 23) ∨ (m = 59 ∧ h = 23)}] THEOREMS thm1-2 : P O T HM (machine) ∧ Init W ellDef ined(machine) thm3 : Variant WellDefined(machine) thm4 : T ag Event W ellDef ined(machine) END

THEN a c t 1 :

 1 m, h :| pr(m ′ → h ′ ) ∈ BAP(machine)[{tick hour }][{pr(m → h)}] END Tick midnight REFINES Do Ordinary . . . THEN a c t 1 : m, h :| pr(m ′ → h ′ ) ∈ BAP(machine)[{tick midnight}][{pr(m → h)}] END END Listing 10: A shallow instance of the clock machine (S.4)

THEORY

  EvtBTheoDeadlock IMPORT EvtBTheo TYPE PARAMETERS ST AT E, EV EN T OPERATORS / / A p r e d i c a t e f o r m a c h i n e D e a d l o c k f r e e n e s s PO DeadlockFreeness <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) d i r e c t d e f i n i t i o n Inv(m) ⊆ Grd(m)[P rogress(m)] / / W e l l -d e f i n e d m a c h i n e s w i t h d e a d l o c k f r e e n e s s . check Machine DeadLock <p r e d i c a t e > (m : M achine(ST AT E, EV EN T )) w e l l -d e f i n e d n e s s c h e c k M a c h i n e W e l l D e f i n e d (m) ∧ P O D e a d l o c k F r e e n e s s (m) d i r e c t

TABLE I :

 I

Global structure of Context, Machines and Refinements

Machines (Table

TABLE III

 III

	: Refinement Proof obligations
	-Refinements. Refinement (see Table I(c)) enables incremental
	design by introducing characteristics such as functionality,
	safety, reachability at different abstraction levels. It decom-
	poses a machine, a state-transition system, into a more con-
	crete model, by refining events and variables (simulation rela-
	tionship). Introduction of gluing invariants preserves already
	proven properties.
	-Proof Obligations (PO) and Property Verification. Several
	POs are associated with the Event-B models shown in Table II
	and III. These POs are generated automatically, and all of them
	must be successfully discharged to guarantee the correctness
	of an Event-B model, including refinements. Two additional
	POs related to refinement, guard strengthening and simulation,
	are required in our shallow modeling approach.

  d e f i n i t i o n ⊤ END Listing 11: A theory about Deadlock Freeness VIII. ASSESSMENT We evaluate our EB4EB framework in terms of proof effort and benefits of such extension. Rodin supports all the theories and case study. All the resulting POs were successfully discharged. The complete developments can be found on http://singh.perso.enseeiht.fr/Conference/ ICECCS2022/EB4EB_Models.pdf. 1) Proof effort: Proof statistics for all the developed models (i.e clock, deep, shallow generic, shallow context, and shallow machine) are presented in Table V. Due to its simplicity and

	Models	Total	Automatic	Interactive
		POs	POs	POs
	Clock Event-B model (Listing 5)	25	25 (100%)	0 (0%)
	Clock Deep model context (Listing 6)	2	0 (0%)	2 (100%)
	Shallow generic machine (Listing 8)	14	8 (57%)	6 (43%)
	Clock Shallow context (Listing 9)	5	1 (20%)	4 (80%)
	Clock Shallow machine (Listing 10)	54	26 (48%)	28 (52%)

TABLE

Rodin Integrated Development Environment http://www.event-b.org/index. html


Baojie Dou

Xuejie Li

Junsoo Han

Nick Birbilis

Kevin Ogle
email: kevin.ogle@chimieparistech.psl.eu

Operando kinetics of hydrogen evolution and elemental dissolution Ⅱ:A time resolved masscharge balance during the anodic dissolution of magnesium with variable iron content

The rates of hydrogen evolution, magnesium (Mg) dissolution and electron exchange were monitored individually, in situ, and in real time during anodic and cathodic polarization of Mg in 0.1 M NaCl. Under all conditions, the anodic charge correlated with Mg 2+ dissolution while hydrogen formation was independent and led to insoluble Mg(II). Increased iron (Fe) impurity promoted hydrogen evolution, but was not necessary for the negative difference effect. These results suggest that electrochemical dissolution occured across an intact Mg(II)-based film, while hydrogen evolution occurred in regions where the film breaks down induced by anodic polarization.

Introduction

The anodic polarization of Mg results in an enhanced hydrogen evolution reaction (HER) rate which increases with increasing anodic current, commonly referred to as the negative difference effect (NDE). Despite having been discovered more than 150 years ago [ 1 ], the origins of the NDE remain under debate. Possible mechanisms have emerged and have been recently reviewed [ 2 , 3 , 4 ]. Although the effect has been observed on other materials such as Al [ 5 ] and rare earth elements [ 6 ], hydrogen evolution during anodic polarization is especially intense for Mg. Understanding this effect is important on the basis that Mg is the lightest structural metal, and corrosion limits its use for many applications in which it would otherwise be an ideal candidate. More specifically, the evolution of hydrogen during Mg dissolution also limits the use of Mg as an anode material in batteries or sacrificial anodes [ 7 , 8 , 9 , 10 ]. In such applications, hydrogen evolution is a parasitic reaction on the anode, resulting in a loss of efficiency.

A key to understanding the mechanism of so-called NDE, which refers to hydrogen evolved during anodic polarization, is obtaining the correct stoichiometry between charge passed, hydrogen evolved, and oxidized Mg. The term "NDE" refers to the mass-charge balance [ 11 ], the observation that the total quantity of oxidized Mg formed as a result of anodic polarization, is greater than that predicted by the anodic charge consumed during polarization. The excess Mg oxidation is, of course, compensated by hydrogen evolution (NDE). The stoichiometry of the reaction requires considering the oxidation of Mg to form either dissolved Mg ions (Mg 2+ (aq), Eq. 1), or insoluble Mg oxide/hydroxide (Mg(II), in this case Mg(OH) 2 (s), Eq. 2). The oxidation is balanced by hydrogen (H 2 (g)) evolution (Eq. 3) and electron transfer (Eqs. 1-3). A simple overall reaction scheme highlighting these processes is as follows:

Mg  Mg 2+ (aq) + 2 e -

[1]

Mg + 2 OH - Mg(OH) 2 (s) + 2 e - [2] 2 H 2 O + 2 e - 2 OH -+ H 2 (g) [START_REF] Yuwono | Aqueous electrochemistry of the magnesium surface: Thermodynamic and kinetic profiles[END_REF] J o u r n a l P r e -p r o o f

If the rates of the above reactions are expressed electrical currents according to Faraday's law, the total electrical current measured during anodic polarization in the absence of any competing redox reactions, is written as:

i e = i Mg 2+ + i Mg(II)-oxi H 2 [START_REF] Esmaily | Fundamentals and advances in magnesium alloy corrosion[END_REF] where i e is the faradaic electrochemical current, i Mg 2+ and i H 2 , are the dissolution rate of Mg and the hydrogen evolution rate, expressed as electrochemical currents. The difference, expressed as a current i Mg(II)-ox , is the formation of insoluble Mg oxidation products. Much of the literature regarding NDE has focused on average mass balance measurements that may be obtained by total charge, total hydrogen produced, and mass loss following removal of corrosion products obtained after relatively long periods of time. This was the case for the original experiments of Beetz (i Mg 2+ ) using atomic spectroelectrochemistry [ 12,13,14,15,16 ], or hydrogen evolution (i H 2 ) using the gravimetric technique originally developed by Curioni [ 17 , 18 , 19 , 20 ]. These methods have provided considerable insight into the nature of the reactions, but leave one of the elementary processes undetermined.

The time resolved measurement of the three physical quantities; electric current, elemental dissolution, and hydrogen evolution; was first attempted by Lebouil et al.

[ 13,14 ]. A micro-fluidic system was equipped with a video recorder and a specialized image analysis software to quantitatively measure hydrogen bubbles in transit to a downstream inductively coupled atomic emission spectrometer (ICP-AES) for measuring Mg 2+ concentration. Such work revealed that Mg dissolution rate (i Mg 2+ ) and J o u r n a l P r e -p r o o f the anodic faradaic current (i e ) were in good correlation, with a stoichiometry consistent with a direct, n = 2, dissolution step (Eq. 1). By contrast, the rate of anodic hydrogen production (the rate of the NDE, i H 2 ) increased throughout the experiment and did not seem to be directly associated with the Mg dissolution rate. These results strongly suggested that the electrochemical Mg dissolution (Eq. 1) and the NDE were not directly related.

It was proposed that the electrochemical Mg dissolution (Eq. 1) occurred across an intact oxide/hydroxide film leading to a time independent stoichiometry of n = 2 between e -and Mg 2+ (aq) [ 13, 14 ]. Concomitantly, the passage of anodic current would lead to the formation of defects within the film where Mg(0) would contact H 2 O, leading to an essentially instantaneous reaction to form insoluble corrosion products due to the high thermodynamic affinity of Mg to react with water (E° = -2.38 V vs. SHE):

Mg + 2 H 2 O  Mg(OH) 2 (s) + H 2 (g) [5]
Mg + H 2 O  MgO(s) + H 2 (g) [START_REF] Liu | An experimental survey of the cathodic activation of metals including Mg, Sc, Gd, La, Al, Sn, Pb, and Ge in dilute chloride solutions of varying pH[END_REF] This close relationship between i e and i Mg 2+ had also been observed in previous studies with in-line dissolution experiments, albeit in which hydrogen was not measured [ 12-14 ].

Further, in the original 19 th century work of Beetz [ 1 ], it was noted that the solid oxidized Mg products formed were stoichiometrically in agreement with the hydrogen produced. However, the complete time resolved mass-charge balance experiments of

AESEC measurements

The principles of the AESEC technique and flow cell have been described in detail previously [ 23 ]. The dissolution rate of each element in the specimens studied was The electrolyte was 0.1 M NaCl (unbuffered) and samples were exposed to the flowing electrolyte with a 1 cm 2 surface. The rate of H 2 evolution was calculated using a moving average of 150 s, and data treatment was according to methods described in Part I of this study.

Results and Discussion

J o u r n a l P r e -p r o o f and the hydrogen evolution rate (i H 2 ), determined from the spectroscopic and gravimetric data, respectively. The elemental dissolution rate is presented as an equivalent current assuming n = 2, whereby i M = nF υ M , and υ M is the rate of production for M, and F is Faraday constant (96500 C mol -1 ). Note that for simplicity i H 2 is defined as a positive value.

The overall effect of the applied potential on the HER and Mg dissolution, as well as their stoichiometry relative to electron exchange, may be readily observed from the experiments herein (Fig. 1). In the region of cathodic polarization, the HER rate decreased with increasing potential and closely followed the cathodic current revealing the anticipated e -/H 2 stoichiometry of 2 (Eq. 3). In this region of cathodic polarization, i H 2 at a given potential was approximately a factor of two less intense for the Mg -25 ppmw Fe alloy (Fig. 1a), but was similar for the other two Fe concentrations (Figs. 1b and1c), indicative of the enhanced cathodic reaction rate due to the presence of Fe.

In the region of anodic polarization, the Mg dissolution rate (i Mg ) closely followed the anodic current demonstrating an e -/Mg 2+ (aq) stoichiometry of 2 as was observed in prior studies [ 12-16 ]. The NDE was clearly visible as the i H 2 increased with increasing potential in this region of anodic polarization. The NDE was most pronounced for higher Fe containing specimens (Figs. 1b and1c) for which the HER (i H 2 ) was more

HER and Mg dissolution during cathodic polarization

Fig. 2 shows the rate vs. time profiles obtained for a series of cathodic galvanostatic experiments. The HER rate (i H 2 ) varied within experimental error as predicted from the applied cathodic current by Faraday's law for the reduction of water (Eq. 3) and was stable throughout. This confirms the reliability of the measurements for i H 2 of Mg using J o u r n a l P r e -p r o o f the AESEC-gravimetric technique both in terms of the quantitative nature of the measurement as well as its stability. This is important as no such reference prediction is possible for i H 2 during an anodic polarization. The Mg dissolution rate in this potential domain remained negligible as compared to the HER rate and was not further investigated in this work.

Anodic polarization and the negative difference effect

The anodic galvanostatic experiments are shown in Fig. 4 for the three alloys.

Several points are immediately clear from inspection of these data. For all alloys, the Mg dissolution rate was relatively stable and followed closely the applied current as predicted by Faraday's law, assuming Eq. 1, n = 2. This is in agreement with the potentiodynamic results of Fig. 1. The HER rate was readily measurable for all applied currents and increased proportionally to the applied current, indicative of the NDE. The HER rate was noticeably less stable than for the cathodic experiments of Fig. 2 at equivalent currents, especially for the higher Fe containing materials.

For the 25 ppmw Fe material, the HER rate was nearly constant on average although there was significantly more variation around the mean than was observed for an equivalent cathodic current (Fig. 2). The HER rate dropped down to near zero after the applied current was removed and the system returned to the open circuit potential for the 25 ppmw Fe material. For the higher Fe containing alloys, the HER rate increased with time during the galvanostatic pulse and did not return to the previous

J o u r n a l P r e -p r o o f

open circuit value when the current was stopped but remained at a higher level. The most probable interpretation of this result is that the build-up of Fe in the corrosion products enhances the catalytic activity of the surface for hydrogen reduction. The effect is most apparent for the 220 ppmw Fe material as the initial HER rate was very low while the final rate was nearly equivalent to that of the 13000 ppmw Fe sample (2 ~ 7 mA).

The stoichiometric results for i Mg and i H 2 vs. i app , obtained from the anodic galvanostatic curves in Fig. 4 are summarized in Fig. 5. Note that the red solid line indicates the hypothetical n = 2. The data presented in Fig. 5 were obtained as a 200 s average early (800 to 1000 s) and late (1400 to 1600 s) in Fig. 4. The discrepancy between the two points therefore reflects the increase of the rate over a 600 s time period. The agreement between i Mg and i e in the anodic domain is clearly demonstrated with a e -/Mg 2+ (aq) stoichiometry very close to 2 for the three alloys. For the Mg -13000 ppmw, the lower currents should be related to excessive Mg dissolution, however, this was probably due to the significant open circuit corrosion rate observed for this material. There was little variation between the early and late measurements demonstrating the stability of the electrochemically driven Mg dissolution reaction, Eq.

1.

The HER rate also showed a consistent correlation with the applied current. For Mg -25 ppmw Fe, a least squares fit to the data of demonstrates a correlation of H 2 /e -of approximately 0.49. The absence of an apparent steady state for the 220 and 13000 ppmw Fe samples makes interpretation difficult. Nevertheless, the data sets give a nearly 1:1 relationship between i H 2 and i app for the early time period, which increases as the background corrosion rate increases. J o u r n a l P r e -p r o o f The exposed surface area was 1 cm 2 .

J o u r n a l P r e -p r o o f

Potentiostatic dissolution

Potentiostatic experiments were performed (Fig. 6) with Mg -25 ppmw Fe and Mg -13000 ppmw Fe to represent the two extremes at anodic potentials of -1 V and 0 V vs. SCE. Throughout these experiments the anodic current was fairly stable indicating that the resistance changes were small, and as before, the Mg dissolution rate followed the (i H 2 ) and the total current, (i e ). The exposed surface area was 1 cm 2 .

Spontaneous corrosion, repassivation, and the catalytic effect

The steady increase in the HER rate at a constant applied anodic current and the resulting increase in the open circuit spontaneous corrosion rate was only observed for the higher Fe containing alloys. Notably, no enhancement in the Mg dissolution rate J o u r n a l P r e -p r o o f was observed and even for the 13000 ppmw material, the Mg dissolution rate returned to its near zero initial value after the imposition of an anodic current (Fig. 4). These results are consistent with the hypothesis that the electrochemical dissolution of Mg (Eq. 1) proceeds by an independent mechanism than that of the HER (Eqs. 5 and 6)

although they may be coupled indirectly. The electrochemical anodic current gives rise to predominantly dissolved Mg 2+ cations, while the HER would yield essentially solid oxidation products as in Eqs. 5 and 6.

The increasing HER rate profile as a function of the measurement time for the higher Fe content samples is probably due to the build-up of metallic Fe in the oxide film due to the selective oxidation of Mg, as Fe is well known for its catalytic properties for hydrogen evolution [ 16, 24, 25, 26 ]. The effect is most apparent for the 220 ppmw Fe These results confirm that for materials containing noble impurities, the enhanced reactivity may be largely due to the build-up of those impurities during the anodic polarization. This would of course be the case for most practical Mg alloys in use. The enhancement of hydrogen evolution is more significant than Mg dissolution, however, indicating that the autocatalytic effect favors the formation of insoluble oxidation products over dissolved Mg ions.

The consistency of the Mg dissolution rate is shown in Fig. 8 where the Mg dissolution rate has been normalized to the applied current, i Mg / i app . It is clear that within experimental error the profiles are nearly identical and the decay process is independent of the applied current. Also shown is the calculated decay rate that we

Discussion

A clear understanding of the stoichiometry of anodic Mg dissolution and H 2 generation is a necessary first step in clarifying the reaction mechanisms. Table 2 compares the results of this study with that of experimental stoichiometric measurements prior to this work. Some caution is necessary in using this table in that the stoichiometery was in some case variable with time although the majority of the experiments were detemrined from average values after variable time periods. From inspection of the table, it is clear that the e -: H 2 mole ratio of 1 : 0.25 (i e : i H 2 ≈ 1:0.5) for the purest sample (25-ppmw Fe, Fig. 5) is similar to the results obtained by the majority of researchers working with high purity Mg.

For the less pure materials (220 and 13000 ppmw Fe) the e -: H 2 mole ratio was ≈ 1 : 0.5 (i e : i H 2 ≈ 1:1), but was not stable, increasing steadily during the experiment (see Fig. 4) reaching approximately 1:0.7 at longer times. The instability was especially J o u r n a l P r e -p r o o f visible in the potentiostatic profiles although the 1:0.5 stoichiometry of e -: Mg 2+ was quite stable. This variation is reflected in the literature with values reaching e -: H 2 mole ratio ≈ 1 : 0.8 which also correlates with the Fe content of the materials and the applied anodic current. The high variability indicates that the HER was not directly related to the electrochemical current, the counter example, being cathodic hydrogen reduction the expected e -: H 2 mole ratio of 1 : 0.5 was obtained under all conditions of this work.

The important contribution of this work is to confirm the previously reported e -: Mg 2+ (aq) mole ratio = 1 : 0.5 over a wide range of Mg purity and applied current/potential conditions. This stoichiometry was observed with good reproducibility over all the conditions of these experiments and was stable throughout the experiments, and independent of the HER. There is little data in the literature with which to compare this result other than from previous publications of the present authors, since the measurement requires an online analysis of the dissolved Mg. Also many authors use Mg(OH) 2 saturated electrolytes for these experiments in which case Mg 2+ dissolution is unlikely and would be unmeasureable in any case. A similar stoichiometry was observed in Rossrucker et al. [START_REF] Rossrucker | Investigating the real time dissolution of Mg using online analysis by ICP-MS[END_REF] using ICP mass spectrometer although the point was not discussed therein.

This n = 2 stoichiometry suggests that the formation of aqueous Mg 2+ ions occurs via an n = 2 mechanism (Eq. 1) with a near 100% faradaic efficiency in unbuffered 0.1 M NaCl. It follows from a mass-charge balance that of Eq. 4, that if |i e | = i Mg 2+, then i H 2 = i Mg(II)-ox . Therefore, if Mg dissolution occurred via a direct electrochemical reaction, it would follow that the hydrogen evolution reaction must occur by a different mechanism involving the direct reaction of Mg with H 2 O (Eq. 5 and/or 6) leading to the formation of insoluble Mg corrosion products [ 13, 14 ]. Indeed, the reduction of H 2 O in the unbuffered solution would lead to an increase in interfacial pH favoring the precipitation of Mg hydroxides and oxides, and would not be detected by ICP-AES. Fe impurities were shown to have a strong accelerating effect on J o u r n a l P r e -p r o o f the HER but did not affect the stoichiometry of the electrochemical dissolution mechanism, e -/Mg 2+ (aq).

By contrast, electrochemically driven Mg dissolution (Eq. 1), with the cathodic reaction localized on the counter electrode, would not produce a similar pH increase and therefore, we would expect the dominant product to be Mg 2+ (aq) ions (Eq. 1) that may be detected in solution by ICP-AES. It is probable that this reaction occurs across the naturally formed oxide / hydroxide film. The breakdown of this naturally protective film would result in defects where metallic Mg(0) comes into contact with the electrolyte, a direct reaction will occur, Eq. 5 and/or 6. This would give rise to the hydrogen evolution reaction which would increase with increasing potential (i.e., the NDE). This reaction would not be detected directly by ICP-AES nor contribute to the electrochemical current. This demonstrates the need for simultaneous gravimetric H 2 and dissolved Mg measurement to quantify the contribution of H 2 evolution rate for a complete mass-charge balance of Mg corrosion.

The objective of this article is to demonstrate the methodology of real time kinetics for hydrogen evolution and Mg dissolution by determining the stoichiometry as a function of time for anodic Mg dissolution. Nevertheless, this stoichiometry of the reaction process sets a boundary condition for any mechanistic speculation. As was discussed in Lebouil et al. [ 13,14 ] these observations are in good agreement with a very early explanation of the NDE proposed by U.R. Evans in 1946 [ 28 ], and elaborated by Robinson and King [ 29 ] and Tunold et al. [ 30 ] in 1977. It is well known that when Mg is exposed to water, a passive film of hydroxide and/or oxide forms spontaneously. This film serves to separate the metallic Mg from the aqueous solution as indicated by the typical corrosion potential in acidic solution is generally much more positive than the thermodynamic -2.38 V vs. SHE [ 31 ]. In this hypothesis, the NDE arises when, under anodic polarization, the passive film breaks down locally and the Mg reacts directly with water. This produces Mg 2+ , H 2 and OH -, with the resulting pH increase leading to the precipitation of Mg(OH) 2 .

J o u r n a l P r e -p r o o f

The latter would most likely correspond to the black film associated with the cathodic areas observed on the surface [ 32 , 33 ]. In other words, the NDE would be explained by what is analogous to a pitting mechanism. In fact, hydrogen production from pits has been observed on Al [ 34 ], Fe-20Cr, and stainless steel even for imposed potentials as noble as 1.4 V vs. SHE [ 35 ]. This mechanism has been elaborated in detail for the NDE on Al [ 5 ]. In this hypothesis, we would therefore expect to see an NDE effect on any metal for which the pitting potential (or the potential at the bottom of a pit) is below the thermodynamic potential of hydrogen formation. As a consequence, the only thing that makes Mg unique is the degree to which hydrogen production is observed which is no doubt a result of the aforementioned thermodynamic affinity to react with water, coupled with the poorly passivating nature of most Mg corrosion products. This effect is enhanced by the presence of noble impurities (Fe in this work) which have been shown to have an accelerating effect on anodic hydrogen production (NDE) [ 16 ] and the accelerating effect continues even after the polarization.

J o u r n a l P r e -p r o o f



The negative difference effect (NDE) increased with increasing anodic current.

Hydrogen evolution was markedly enhanced for Mg when the Fe impurity concentrations were appreciable. However, even the most pure material tested (25 ppmw Fe) revealed a significant HER rate during anodic polarization. The HER rate in this case is stable and returns to nearly the original open circuit value once the applied current is removed.

 By contrast, the Fe enriched specimens showed a steadily increasing HER rate which remained elevated, even following the removal of an applied anodic polarization.

However, Mg dissolution was not enhanced or affected by the presence of Fe, demonstrating that the NDE results almost exclusively in the formation of insoluble Mg oxidation products, in contrast to the applied anodic current which results almost exclusively in dissolved Mg 2+ ions.



These results are consistent with a mechanism involving an electrochemical Mg dissolution mechanism across an intact protective film, with hydrogen evolution occurring at areas where the film has broken down and H 2 O reacts directly with Mg to form insoluble corrosion products.

☐The authors declare the following financial interests/personal relationships which may be considered as potential competing interests:

Highlights

• The rates of hydrogen evolution, Mg dissolution, and electron transfer were measured simultaneously in real time during the anodic polarization of magnesium. • The Mg 2+ /e -ratio is equal to an expected 1:2 consistent with a two-electron transfer mechanism for dissolution.

• The Mg 2+ /H 2 was 2:1 for the nominally pure (25 ppmw Fe) Mg material; but was approximately 1:1 and unstable for higher Fe content. • For the high Fe containing specimens, the corrosion rate was enhanced following anodic polarization. This effect was not observed for nominally pure Mg.

  [ 1 ]. Time resolved measurements are more insightful for identifying possible mechanisms, as they permit direct correlation between the different terms during transient experiments. A complete time dependent evolution of a Mg alloy during anodic polarization requires measuring at least three of the aforementioned coupled phenomena, along with the total electron transfer rate. Time resolved measurements have been recently presented involving two of the terms in Eq. 4, electron transfer (i e ) and coupled with either Mg dissolution rate

  measured independently and simultaneously, as a function of time, using an inductively coupled plasma atomic emission spectrometer (ICP-AES) downstream from an electrochemical flow cell. This technique permits the direct measurement of elements entering the electrolyte either spontaneously or with electrochemical polarization. In this work, an Ultima 2C TM spectrometer (Horiba Jobin Yvon, France) was used for the online elemental analysis. The emission of Mg and Fe were measured at 279.08 nm and 259.94 nm respectively.The coupling of the gravimetric hydrogen system with AESEC was described in Part I of this study[ 21 ]. Mass changes were recorded using a Mettler Toledo ME204 TM balance with ± 0.1 mg sensitivity and time resolution of 1 point per second. A Gamry Reference 600 TM potentiostat / galvanostat was used to perform the electrochemical experiments. A saturated calomel electrode (SCE) reference electrode and a Pt foil counter electrode with a dimension of 25 × 20 × 0.2 mm were used in all experiments.

  [ 21 ]

3. 1 .

 1 Potential dependence of Mg dissolution An overview of the Mg dissolution and hydrogen evolution rates as a function of potential of the three Mg materials was obtained by consideration of the potentiodynamic elemental polarization curves, shown in Fig. 1, for 0.1 M NaCl. The spontaneous Mg dissolution rate in open circuit conditions is shown before and after the potentiodynamic polarization (which is defined as linear sweep voltammetry, LSV). The electrical current density (i e ) is displayed, along with the Mg dissolution rate (i Mg 2+ )

J o u rFig. 1 .

 1 Fig. 1. Potentiodynamic linear sweep voltammetry (LSV) curves of Mg alloys in 0.1 M NaCl solution at 1 mV s -1 scan rate from -4.5 V to 1.0 V vs. SCE. (a) Mg -25 ppmw Fe, (b) Mg -220 ppmw Fe, and (c) Mg -13000 ppmw Fe. Data in dots are from galvanostatic / potentiostatic measurements shown in Figs. 2, 4 and 6. The error bars are obtained from the standard deviation of the signal.

Fig. 2 .

 2 Fig. 2. Galvanostatic cathodic step for Mg -25 ppmw Fe in 0.1 M NaCl solution. Left: Mg dissolution rate (i Mg ); and right: HER rate (i H 2 ). The applied current (|i e |) is shown for reference. Note the scale difference for the two curves.

Fig. 3 .Fig. 3

 33 Fig. 3. Variation of i H 2 and i Mg as a function of i app in the cathodic domain from Fig. 2. The dashed lines give a least squares fit to the data while the solid lines show the theoretical (n = 2) for HER and (n = 0) for Mg dissolution.

Fig. 4 .

 4 Fig. 4. Anodic galvanostatic dissolution Mg -Fe alloys at variable applied anodic current, i e . Shown are the Mg dissolution rate (i Mg , left) and HER rate (i H 2 , right). The rectangular curves show the applied current, i e . The exposed surface area was 1 cm 2 .

Fig. 5 . 4 .

 54 Fig. 5. HER and Mg dissolution rates expressed as equivalent currents (i H 2 and i Mg , respectively) as a function of the applied anodic current (i app ) from the galvanostatic experiments of Fig. 4. The red solid line is the hypothetical n = 2. The early (lower) and late (upper) rate of HER are shown as separate points.

J o u rFig. 6 .

 6 Fig. 6. Anodic potentiostatic dissolution of Mg -25 ppmw Fe (left) and Mg -13000 ppmw Fe (right) at -1 V vs. SCE (upper) and 0 V vs. SCE (lower). Shown are the Mg dissolution rate (i Mg ) and the HER rate

  because the surface concentration of Fe is initially low due to the low Mg dissolution rate in the first open circuit measurement. Therefore, the Fe build-up leads to a marked increase in active surface site for HER. For the 13000 ppmw Fe, the initial open circuit HER rate is already quite significant, probably due to the high initial Mg dissolution leading to form a metallic Fe enriched layer catalytic to HER. In this case, the effect of the Fe build-up throughout anodic polarization is less pronounced than the case of 220 ppmw Fe.The decay of the HER and Mg dissolution rates following anodic polarization may be considered as a form of repassivation, as the activated surface returns to its original, less reactive state. The decrease of the Mg dissolution and HER rates represents a measure of the repassivation rate. This is shown in Fig.7which compares the rates during open circuit potential (OCP) trace before (solid curves) and after (dashed curves) the LSV experiments of Fig. 1. For the latter, the t = 0 point is defined as the time at which the potential returns to open circuit. In all three cases the Mg dissolution rate profile is nearly identical and returns very close to its near zero initial value. The HER rate returns to its initial near zero value only for the 25 ppmw Fe alloy; the two others show a markedly enhanced HER rate. The solid red curve in Fig. 7 is a trace of the Mg J o u r n a l P r e -p r o o f dissolution rate for Mg -25 ppmw Fe, offset to account for the enhanced background HER rate. From this analysis, it appears that the decay kinetics have not changed significantly, only the increase in the background HER rate.

Fig. 7 .

 7 Fig. 7. Mg dissolution rate (i Mg ) and hydrogen evolution rate (i H 2 ) before LSV (E oc1 , solid curves) and after LSV (E oc2 , dashed curves) (from Fig. 1) in a 0.1 M NaCl solution. The open circuit dissolution and HER rate profiles were recorded for 600 s for the three alloys as indicated. The solid red line curve gives the time variation of the HER for the 25 ppmw case, offset to account for the enhanced open circuit corrosion rate. For E oc1 , t < 0 indicates a time period when electrolyte was not in contact with the electrode; and for E oc2 t < 0 indicates the last time period of the LSV measurement.

  would expect for the flow cell based on measurements and simulations of the residence time distribution of ions in the flow cell [ 27 ]. The result demonstrates that Mg leaching J o u r n a l P r e -p r o o f from the flow cell is slower than would be the case based purely on hydrodynamics of the flow cell.

Fig. 8 . 4 .

 84 Fig. 8. Normalized Mg dissolution rate (i Mg / i app ) for Mg -25 ppmw Fe in 0.1 M NaCl solution during the second OCP period following variable anodic galvanostatic exposures, from Fig. 4. The calculated decay predicted by previous evaluations of the flow cell residence time distributions (RTD) measured for nominally pure Cu in 1.0 M HCl with 1 mA galvanostatic pulse is shown in purple for comparison based on [ 27 ].

Table 2 . 5 

 25 Summary of previous stoichiometric measurements for the anodic dissolution of Mg under similar conditions to this work. * = Authors stated in the paper; ** = authors gave a figure indicating the stoichiometry; *** = authors gave a figure, stoichiometry calculated by us; and Ͳ : Variable with time ) Stoichiometry based on charge (e -), dissolved Mg (Mg(aq)) and H2; or charge and dissolved Mg It was determined that Mg dissolution closely follows the anodic faradaic current, with n = 2, consistent with Mg  Mg 2+ (aq) + 2 e -, for all currents and potentials, whilst being independent of the Fe impurity concentration.

  both refine and supplement the conclusions of Lebouil et al.[ 13,14 ]. Further, Mg specimens with a varying concentration of Fe were considered, ranging from ultra-high purity (25 ppmw Fe), typical (220 ppmw Fe), and high impurity (13000 ppmw Fe; 1.3

	Mg-25 ppmw Fe	Bal.	0.0025 0.017	0.007	<0.002 <0.005 0.085
	Mg-220 ppmw Fe	Bal.	0.022 0.008	0.001	<0.002 <0.005 0.002
	Mg-13000 ppmw Fe Bal.	1.30	0.022	0.001	<0.002 <0.005 0.005
	wt.% Fe) so as to separate the intrinsic NDE from that due to the enrichment of noble
	impurities such as Fe.
	2. Experimental
	J o u r n a l P r e -p r o o f 2.1. Materials Magnesium specimens with different concentrations of Fe (25 ppmw Fe, 220 ppmw Fe and 13000 ppmw Fe) were fabricated using a resistance furnace and a crucible capable of producing 300 g ingots. The impurity of 25 ppmw Fe was chosen as this would be approximately the technological limit level of purity of Mg alloys. The 220 ppmw may be equivalent to an approximate technical grade that would be used in most Mg alloy applications. The 13000 ppmw Fe sample represents a high impurity Mg sample. A complete description is available in a previous publication [ 16 ] and the composition of each alloy used in this work is summarized in Table 1. A nominally pure Mg (25 ppmw Fe) was used as the raw material, and a small amount of Fe was added with regular stirring to achieve a specific Fe level in the final casting. AM-Cover TM was employed as a cover gas to reduce oxidation during the melting and casting process. The melt was poured into a graphite-coated cast Fe mold and allowed J o u r n a l P r e -p r o o f
	to air cool. Prior to experiments, the alloys were ground with P2400 grit SiC paper
	under ethanol and then dried under flowing high purity N 2 gas. All solutions were
	In part I of this work [ 21 ] a novel adaptation of the AESEC -gravimetric hydrogen prepared from analytical grade reagents and with high purity deionized water of 18.2
	experiment [ 22 ], was demonstrated. The quantitative relationship between hydrogen MΩ cm resistivity supplied from Millipore TM system.
	production either by application of cathodic polarization or due to spontaneous open
	Table 1. Composition of Mg alloy used in this study. Compositions are given in wt.%, circuit dissolution of a galvanized steel was demonstrated. The objective of the present adapted from [ 16 ].
	study is to determine the complete stoichiometry (electron transfer, Mg dissolution, and Sample Mg Fe Mn Zr Ni Cu Al
	hydrogen evolution) for Mg in 0.1 M NaCl over a wide range of potential and current to

Lebouil et al.

[ 13,14 ]

were conducted over a limited range of conditions and with only one Mg specimen containing a non-negligible impurity level of Fe (280 ppm). The generality of the mechanisms proposed therein was not fully demonstrated.

  • The kinetics of spontaneous repassivation of Mg following anodic polarization were obtained. REFERENCE 1 W. Beetz, "On the development of hydrogen from the anode", Phil. Mag., 32 (1866) 269-278. https://doi.org/10.1080/14786446608644179 2 S. Thomas, N.V. Medhekar, G.S. Frankel, and N. Birbilis, "Corrosion mechanism and hydrogen evolution on Mg", Curr. Opin. Solid State Mater. Sci., 19 (2015) 85-94. https://doi.org/10.1016/j.cossms.2014.09.005

	Simultaneous H 2 evolution & elemental dissolution rates	i Mg	15 20		Mg  Mg 2+ (aq) + 2e -
	Elemental AESEC dissolution	gravimetry H 2 evolution	i / mA	5 10				jMg i Mg je i e
	Mg 2+ (aq)	2OH -+ H 2 (g) 2H 2 O	i H 2	0	0	1000	2000	3000
		Mg(OH) 2		20		2 H 2 O + 2 e - H 2 (g) + 2OH -
	0 5 J o u r n a l P r e -p r o o f 0 1000 2000 3000 i / time / s Initial surface NDE Active Surface Electrochemical current 2e -i e 10 15 mA je jH2 i e Mg i H 2 2e

- CRediT authorship contribution statement BD: Investigation, methodology, visualization, writingfirst draft, validation. XL: Methodology, investigation JH: Methodology, investigation, visualization, validation, writing, review & editing ND: Review & editing, validation, resources KO: Methodology, visualization, writing, review & editing, validation, supervision, resources, funding acquisition.

J o u r n a l P r e -p r o o f

Acknowledgements

Author Baojie Dou would like to express his gratitude to China Scholarship Council (CSC) for financial support. 1 J o u r n a l P r e -p r o f

Conclusions

In this study, the stoichiometry of anodic Mg dissolution and hydrogen evolution were investigated using a novel approach incorporating element-resolved electrochemistry (AESEC) coupled with a gravimetric hydrogen detection system. The stoichiometry was investigated over a wide range of applied anodic currents and potentials, for Mg specimens with widely varying Fe impurity concentrations.

J o u r n a l P r e -p r o o f

Declaration of interests

☒ The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.

J o u r n a l P r e -p r o o f