Neeraj Peter Riviere
email: peter.riviere@enseeiht.fr

Kumar Singh
email: nsingh@enseeiht.fr

Yamine Aït-Ameur
email: yamine@enseeiht.fr

Guillaume Dupont
email: guillaume.dupont@enseeiht.fr

Standalone

P Rivière

N K Singh

Standalone Event-B models analysis relying on the EB4EB meta-theory

Keywords: Reflection, Refinement and Proof, Meta-theory, Reachability, Deadlock-Freeness, Invariant weakness, EB4EB framework, Event-B

come

Introduction

Context. The refinement and proof state-based Event-B formal method [START_REF] Abrial | Modeling in Event-B: System and software engineering[END_REF] supports complex system development using a correct-by-construction approach. It is based on set theory and First Order Logic (FOL) for describing state transition systems. It relies on an inductive proof process to discharge a set of proof obligations (POs) expressing various properties. Basically, core Event-B offers built-in modelling constructs to express invariants, event convergence, simulation, guard strengthening and event feasibility. POs associated to these constructs are automatically generated and are discharged using automatic and interactive provers.

In order to enrich the method's expressiveness, Event-B has been extended with the ability to define new algebraic data-types resulting in a richer type system [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], through the introduction of Theories. This extension allows the formalisation of complex systems at a higher level of abstraction.

Motivation. Event-B theories make it possible to formalise new data types, but they do not allow the definition of new POs that correspond to properties other than the usual ones (i.e., invariants preservation, event convergence, etc.).

Indeed, when properties such as deadlock-freeness, event scheduling, liveness, and so on need to be proved, they are explicitly formalised by the designer, or expressed in another formal method. This process compromises reusability and is error-prone, especially on large systems. The designer shall formalise each desired property for each system under design using the native Event-B POs. This process may be cumbersome, must be repeated for each model to be analysed (not reusable) and results in formal developments scattered across multiple heterogeneous frameworks and semantics.

To incorporate such properties in Event-B once and for all and allow the automatic generation of property-specific POs, it is necessary to embed, in the Event-B engine, the POs associated to these new properties. Such embedding requires the manipulation, in Event-B, of Event-B concepts as first-order objects (i.e., through a reflexive meta-model). We have recently proposed a reflexive EB4EB framework [START_REF] Riviere | EB4EB: A Framework for Reflexive Event-B[END_REF][START_REF] Riviere | Reflexive Event-B: Semantics and Correctness the EB4EB Framework[END_REF] that formalises Event-B concepts as first-class objects in Event-B. It allows manipulating these concepts in Event-B using first-order logic and set theory. It is built on an algebraic meta-theory formalised as an Event-B theory, where each Event-B feature can be handled at the meta-model level, as first-class citizen. This framework also formalises Event-B's trace-based semantics and offers constructs for machines, states, and events together with a set of operators for manipulating them. Consequently, the EB4EB framework makes it possible to formally express, at any abstraction level (i.e. in the refinement chain), new reusable and automatically generated POs and high-level constructs, easing the development of complex systems with specific properties or semantics. Furthermore, it opens the door to formally embed Event-B's semantics in other formal methods and exploit their respective strengths.

Objective of this paper. This paper extends and enriches our previously developed EB4EB framework [START_REF] Riviere | EB4EB: A Framework for Reflexive Event-B[END_REF][START_REF] Riviere | Reflexive Event-B: Semantics and Correctness the EB4EB Framework[END_REF] to support new analysis mechanisms (possibly nonintrusive), formalised as logic properties not available in native Event-B nor in its base PO generator. It extends the EB4EB Event-B meta-theory with new operators formalising such new properties. The POs associated to each operator are automatically generated. Adding the desired property, corresponding to a specific analysis, to an Event-B model is performed by invoking an operator. Designers do not need to formalise this property explicitly in the model.

Structure of the paper. The paper is organised as follows. Section 2 describes the Event-B method and the Theory mathematical extension. Section 3 introduces the EB4EB framework and its Event-B meta-theory, as well as the case study

A(s, c) ⇒ Tctx (For contexts) (2) Mch Theorems (ThmMch) A(s, c) ∧ I(x) ⇒ T mch (x) (For machines) (3) Initialisation (Init) A(s, c) ∧ BAP(x ′ )⇒ I(x ′ ) (4) Invariant preservation (Inv) A(s, c) ∧ I(x) ∧ G(x, α)∧ BAP(x, α, x ′ ) ⇒ I(x ′ ) (5) Event feasibility (Fis) A(s, c) ∧ I(x) ∧ G(x, α)⇒ ∃x ′ • BAP(x, α, x ′ ) (6) Variant progress (Var) A(s, c) ∧ I(x) ∧ G(x, α)∧ BAP(x, α, x ′ ) ⇒ V (x ′ ) < V (x)

Event-B

Event-B [START_REF] Abrial | Modeling in Event-B: System and software engineering[END_REF] is based on set theory and FOL. It relies on an expressive state-based modelling language where a set of events models state changes.

Contexts and machines (Tables 1.a and 1.b)

A Context (Table 1.a) describes the static part of a model. It introduces carrier sets s and constants c, and their properties using axioms A and theorems T ctx . A Machine (Table 1.b) describes the model behaviour as a transition system. A set of events evt, possibly guarded by G and/or parameterized by α, is used to modify a set of state variables x using Before-After Predicates (BAP ) to record state changes. A machine may define invariants I(x), theorems T mch (x) and variants V (x) to capture particular properties (e.g., safety and convergence). Model consistency is ensured via a set of generated POs, given in Table 2.

Refinements. Refinement decomposes a machine into a less abstract one with more design decisions (refined states and events) moving from an abstract level to a less abstract one (simulation relationship). Gluing invariants relating abstract and concrete variables ensure property preservation.

Core Well-definedness (WD). In addition to machine-related POs, each operator is associated to a WD, that must be established for expressions to be meaningful. Once proved, these WD conditions are used as hypotheses to prove further POs.

Event-B extensions with Theories

To handle more complex and abstract concepts beyond set theory and FOL, an Event-B extension for externally defined mathematical objects has been proposed [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]. It introduces user data types with new types, operators, theorems and associated rewrite and inference rules, all bundled in so-called theories. Close to proof assistants like Coq [START_REF] Bertot | Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions[END_REF], 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], this capability is convenient to model, as data types, concepts unavailable in core Event-B.

Theory description (See Operators may be defined explicitly in the DIRECT DEFINITION clause (constructive definition), or axiomatically in the AXIOMATIC DEFINITIONS clause (a set of axioms). Last, a theory defines a set of axioms, completing the definitions, as well as theorems and proof rules. Theorems and proof rules are proved from the definitions and axioms used by the proof system. Many theories have been defined for sequences, lists, groups, reals, differential equations, etc.

Well-definedness (WD) in Theories. An important feature provided by Event-B theories is the possibility to define Well-Definedness (WD) conditions (close to Type-Correctness Condition (TCC) conditions in PVS [START_REF] Owre | PVS: A prototype verification system[END_REF]). TCC must be discharged before the corresponding theory types correctly. Similarly, in Event-B theories, each defined operator (thus partially defined) is associated with a userdefined condition ensuring its well-formedness. Note that, when an operator is applied, it automatically invokes its WD condition and generates a PO requiring to establish that this condition holds, i.e., the operator is used correctly and that its parameters belong to its definition domain.

Event-B proof system and its IDE Rodin. Rodin is an open source IDE 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. The Event-B theories extension 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 may be imported as hypotheses and used in proofs like other theorems. Many provers for first-order logic as well as SMT solvers are plugged to Rodin for helping the proof process.

The EB4EB framework

The main objective of the EB4EB reflexive framework [START_REF] Riviere | EB4EB: A Framework for Reflexive Event-B[END_REF][START_REF] Riviere | Reflexive Event-B: Semantics and Correctness the EB4EB Framework[END_REF] is to provide explicit manipulation of Event-B components as first-class objects, making it possible to reason on these objects and define new Event-B analyses. For this purpose, the concept of Event-B machine is formalised as a data-type in a theory (a meta-theory), together with a set of operators that guarantee the correctness, relative to Event-B semantics, of instances of this data-type. The meta-theory formalises the semantics of Event-B, as described in the Event-B Book [START_REF] Abrial | Modeling in Event-B: System and software engineering[END_REF], i.e. a set of states and guarded events defined as a relation between states. In addition, the meta-theory is equipped with relevant proved (once and for all) theorems useful for discharging the generated POs. These additional theorems are available to help users reduce proof efforts and aid in system development and analysis.

Event-B machines (models) are defined using the meta-theory mentioned above, by instantiating the machine data-type and providing appropriate values for each of its fields: states, events, guards, before-after predicates, invariants, variant and so on. At instantiation, operators of the meta-theory are used in theorems; the related POs ensure the defined machine's consistency, including invariant preservation, event feasibility, variant progress, etc.

As previously stated, the goal of this paper is to demonstrate that the metatheory can be extended with new operators for manipulating machine elements of the meta-theory, in order to define so-called analyses, expressed with new POs. Based on the work presented in [START_REF] Aït Ameur | Empowering the Event-B Method Using External Theories[END_REF], such analyses allow the system designer to check new properties, obtain feedback about their behaviour, enrich model design phases and check new properties that are not available in core Event-B.

This section summarises the main features of the Event-B meta-theory (Listings 1, 2 and 3), and presents the case study used to illustrate our approach throughout this paper.

The Event-B Meta-theory

Machine structure. Listing 1 shows the Machine data-type, defined using type Listing 1: Machine Data-type parameters for abstracting event labels (EVENTS) and states (STATES). It is built using the Cons_machine single constructor with a parameter for each machine component, and defines a state-transition system with state State (constrained by invariants Inv and theorems Thm) and a set of, possibly parameterised, events (Event), with an initialisation event Init and progress events Progress, split into ordinary Ordinary and convergent Convergent events. State changes are recorded using an after-predicate (AP ) for initialisation and a set of before-after predicates (BAP ) associated to progress events, possibly guarded (Grd ). Finally, integer variants for event convergence are introduced as well (Variant).

Well-Constructed machines. To ensure machines are structurally well-defined, the meta-theory introduces several predicate operators (Listing 2): BAP_WellCons to check that each progress event is associated to a BAP, Grd_WellCons to check that progress events are possibly guarded, and Event_WellCons to check that machine events are composed of an initialisation (Init) and progress (Progress) events. The Machine_WellCons predicate operator, defined as a conjunction of the previous operators (and others), ensures that a machine is well-structured (static semantics). Machine POs (behavioural semantics). The Machine data-type offers operators to access and handle its components. In addition to structural consistency, machine correctness is also encoded, through its behavioural semantics and correctness criteria. Formally, this is done by providing an operator for each PO of Event-B (see Table 2), as shown in Listing 3. Such operators are usually defined inductively on the structure of a machine (for initialisation and progress events). 2 are defined in the same manner.

The POs of an Event-B machine are gathered in the conjunctive predicate check_Machine_Consistency, with Machine_WellCons as well-definedness (see Listing 4). It formalises machine's behavioural semantics and general correctness. well-definedness Machine_WellCons (m)

d i r e c t d e f i n i t i o n M ch_T HM (m)∧ M ch_IN V (m) ∧ M ch_F IS(m)∧ M ch_V ARIAN T (m) ∧ M ch_N AT (m)
Listing 4: Operator encoding Event-B machine consistency When this operator is used in a theorem clause, two POs, corresponding to its definition and WD condition, are automatically generated. Proving the theorem ensures the consistency of the machine, defined as an instance of the meta-theory.

Instantiation of the meta-theory. Specific Event-B machines are defined by instantiating the meta-theory. The instantiation process presented in this paper is so-called deep, as it relies solely on set theory and FOL with a set of axioms and theorems. It consists in defining an Event-B context with witnesses (sets) for type parameters STATE and EVENT defined as sets using Cons_machine. Operators may be used in theorems, triggering the generation of POs ensuring machine consistency. Another instantiation process qualified as shallow has also been defined [START_REF] Riviere | EB4EB: A Framework for Reflexive Event-B[END_REF][START_REF] Riviere | Reflexive Event-B: Semantics and Correctness the EB4EB Framework[END_REF]. It relies on the definition of an Event-B machine and its refinement. It is not reviewed here as it is not used in this paper.

The Clock Example

This section presents a case study adapted from Lamport's clock case study [START_REF] Lamport | Specifying a simple clock[END_REF]. It is used to demonstrate the application of the proposed framework, including meta-theory instantiation and definition of new POs. Note that this simple case study is chosen to demonstrate the usability of the new extended mechanism.

The functional requirements of the clock state that minutes and hours progress by 1 and hours are represented in a 24-hour format. The clock must converge to midnight, and never stop. Listing 5 gives a model of the clock as an Event-B machine. In this model, variables m and h represent minutes and hours, respectively. A safety property (inv2) ensures that minutes m (resp. hours h) are always less than 60 (resp. 24). The clock's behaviour is expressed through three events: tick_min (progressing minutes by 1), tick_hours (progressing hours by 1) and tick_midnight (resetting the clock to midnight).

MACHINE C l o c k VARIABLES m , h INVARIANTS inv1 : m ∈ N ∧ h ∈ N inv2 : m < 60 ∧ h < 24 EVENTS INITIALISATION THEN a c t 1 : m, h :| m ′ = 0 ∧ h ′ = 0 END tick_min WHERE g r d 1 : m < 59 THEN a c t 1 : m :| m ′ = m + 1 END tick_hour WHERE g r d 1 : m = 59 ∧ h < 23 THEN a c t 1 : m, h :| m ′ = 0 ∧ h ′ = h + 1 END tick_midnight WHERE g r d 1 : m = 59 ∧ h = 23 THEN a c t 1 : m, h :| m ′ = 0 ∧ h ′ = 0 END END Listing 5: Clock as Event-B machine CONTEXT C l o c k M a c h i n e I
(clock ) = Z × Z axm4 : Event(clock ) = Ev axm5 : Init(clock ) = init axm6 : Inv (clock ) = {m → h | m ∈ N ∧ h ∈ N ∧m < 60 ∧ h < 24} axm7 : AP(clock ) = {m → h | m = 0 ∧ h = 0} axm8 : Grd(clock ) = {e → (m → h) | (e = tick _min ∧ m < 59)∨ (e = tick _hour ∧ m = 59 ∧ h < 23)∨ (e = tick _midnight ∧ m = 59 ∧ h = 23)} axm9 : BAP(clock ) = {e → ((m → h) → (m ′ → h ′ )) | (e = tick _min ∧ m ′ = m + 1 ∧ h ′ = h)∨ (e = tick _hour ∧ m ′ = 0 ∧ h ′ = h + 1)∨ (e = tick _midnight ∧ m ′ = 0 ∧ h ′ = 0)} . . . THEOREMS thm1 : check _Machine_Consistency(clock ) END
Listing 6: Clock as meta-theory instance While the previous example does not show parameterised events, however, our approach handles such events. The same approach has been successfully applied to complex case studies in [START_REF] Mendil | Non-intrusive annotation-based domain-specific analysis to certify event-b models behaviours[END_REF] for critical interactive systems.

The clock machine as an instance of EvtBT heo theory

Listing 6 shows the Event-B context ClockMachineInstance instantiating the meta-theory EvtBTheo. First, axm1 defines the clock machine with the sets Ev (set of events enumerated in axm2) and Z×Z (for m and h). axm3-axm9 define associated machine components. Note that invariant is defined (axm6) on the state as a set of pairs m → h, AP is defined on the initialisation event axm7 and guards and BAPs are associated with an event and a state and defined (axm8 and axm9) on a set of triples e → m → h. In the case of BAPs, it is necessary to record before (m → h) and after (m ′ → h ′ ) states (axm9).

Last, theorem thm1 uses check_Machine_Consistency (see Listing 4). It is associated with a well-definedness (WD) PO, M achine_W ellCons(clock), and a theorem (THM) PO for machine correctness.

POs for new properties: Extending the Meta-Theory

The meta-theory EvtBTheo presented in Section 3.1 is highly extensible: every Event-B feature is explicitly formalised, and can be manipulated using operators, making it possible to define specific development operations or new reasoning mechanisms as new operators. Doing so is non-intrusive (self-contained), in the sense that no modification is needed to the classical development of Event-B models, as machines are handled as instances of the meta-theory.

The main design principle for such Event-B machine analyses, including theories with required operators, definitions, and WD conditions, is given below.

Analysis principle: New POs

In the proposed extension to the EB4EB framework, a model analysis is defined as a PO and must meet two requirements: 1) it must be reusable, and 2) it must be generated automatically. The first requirement is met by formalising the PO at the meta-theory level, while the second one is met by leveraging automatically generated well-definedness (WD) and theorem (THM) POs.

Event-B machine analysis pattern. Listing 7 depicts a generic pattern for defining new POs for Event-B machine analysis. Theo4PO theory imports the metatheory EvtBT heo and introduces a third, optional type parameter T Args possibly needed by the analysis, depending on the nature of new POs (e.g. guards, BAP, etc.). The PO associated to the analysis is formalised as a predicate operator [PO]_Definition. Then, checking the PO is done using the check_Machine[PO] predicate, which is well-defined when machine m is consistent. Following this idea, this section introduces new reasoning mechanisms, not natively present in Event-B, based on the EB4EB framework and the EvtBT heo meta-theory, in the form of analyses that handle Event-B components. Three analyses are detailed: deadlock-freeness, invariant weakness analysis (tracking model holes) and reachability. The key points of using this framework are that: 1) WD conditions ensure elements are used correctly, 2) meta-properties on these analyses are established once and for all, and 3) these analyses can be performed without altering the machine's behaviour, in a non-intrusive way.

Note that only the definition of the [PO]_Definition operator is given, as check_Machine_[PO] is derived by replacing [PO]

with the proposed PO name.

Deadlock-freeness

Requirements. Deadlock-freeness states that a machine m can always progress; i.e., there is always at least one enabled event in machine m, or more formally when the invariant holds then the disjunction of the guards holds.

PO Definition. The PO states that, for a machine m, there exists a progress event e such that any correct state s ∈ Inv(m) verifies the guard of e (s ∈ Grd(m)[{e}]). When expressed using the meta-theory operators, it is formalised as Inv(m) ⊆ Grd(m)[P rogress(m)]. This operator does not require any additional argument for args.

Invariant Weakness as a Non-intrusive Analysis

Requirements. A deployed system may present a number of vulnerabilities, that can be exploited by opponents (or make it weak to the environment) to modify its behaviour. These vulnerabilities usually come from under-specification, i.e., "holes" in the system's requirements or in its formal specification. To address this issue, a nonintrusive analysis of the model's specification is implemented, that does not alter its behaviour. It consists in investigating the robustness of the model's invariants with regard to bad-events, that model potential attacks (under-specification) against the system (model holes). If the system's invariant is preserved by the bad-event, it implies that the invariant is not strong enough to prevent the attack. For instance, the bad event of Listing 11 can be added to the clock machine without falsifying its original invariant. Similarly, other bad-events may be introduced: the event tick_H5 guarded by h < 19 with action m, h :| m ′ = 0 ∧ h ′ = h + 5 and the event tick_HM1 guarded by h < 23 ∧ m < 59 with action m, h :| m ′ = m + 1 ∧ h ′ = h + 1. Note that a class of bad events could be added using two parameters hn ̸ = 1 and mn ̸ = 1 and a corresponding action of the form m, h

:| m ′ = m + mn ∧ h ′ = h + hn.
Bad-events PO definition. This PO is formalised with the AllowedMachineHole-Sub_Definition operator (Listing 12), with the bad-events as parameters. Listing 12: Weak specification analysis theory Each bad-event is characterised by guard nGrd and its BAP nBAP . This operator defined as nBAP [Inv(m) ∩ nGrd] ⊆ Inv(m) states that the bad-event preserves the invariant. So, if the given PO is proved, the bad-event represents a successful attack, and the defined invariant is not strong enough.

Bad events PO for clock model. The analysis to Check the clock specification forbids minutes from progressing by 5 rather than 1, is handled by theorem thmIn-spectInvEVTM5 of Listing 13, using the AllowedMachineHoleSub_Definition operator, where the bad-event is enabled when minutes are below 55 and thus progresses by 5. This corresponds to adding event tick_M5 of Listing 11. Similar theorems are written for the tick_H5 and tick_HM1 bad-events.

CONTEXT C l o c k I n s p e c t I n v EXTENDS C l o c k M a c h i n e I n s t a n c e

THEOREMS thmInspectInvEVTM5 : check _Machine_AllowedMachineHoleSub(clock , {m → h | h ∈ Z ∧ m < 55} , {(m → h) → (m ′ → h ′ ) | m ′ = m + 5 ∧ h ′ = h ∧ h ∈ Z}) thmInspectInvEVTH5 : check _Machine_AllowedMachineHoleSub • • • thmInspectInvEVTHM1 : check _Machine_AllowedMachineHoleSub • • • END
Listing 13: Performing analysis on clock model Note that the thmInspectInvEVTM5, thmInspectInvEVTH5 and thmInspect-InvEVTHM1 theorems are proven for the clock model of the ClockM achine-Instance corresponding to the Event-B machine of Listing 5. As a conclusion, the original model is insufficiently strong and does not provide sufficient constraints on the safe evolution of variables.

A strengthened machine. The designer strengthens the original machine, through instantiation, resulting in the new model shown in Listing 14. New state variables mb and hb are introduced to explicitly record the value of minutes and hours before a tick event occurs. In addition, the events are required to explicitly link these variables as m = mb + 1 and h = hb + 1.

CONTEXT C l o c k I n v S t r o n g SETS Ev , Z × Z × Z × Z CONSTANTS c l o c k , tick_min , 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 : clock ∈ Machine(Z × Z × Z × Z, Ev ) . . . axm2 : . . . axm3 : State(clock ) = Z × Z × Z × Z axm4-5 : . . . axm6 : Inv (clock ) = {m → h → mb → hb | m ∈ N ∧ h ∈ N ∧ m < 60 ∧ h < 24∧ (m = mb + 1 ∧ hb = h) ∨ (m = 0 ∧ (h = hb + 1 ∨ h = 0))} axm7 : AP(clock ) = {m → h → mb → hb | m = 0 ∧ h = 0 ∧ mb ∈ Z ∧ hb ∈ Z} axm8 : BAP(clock ) = {t → ((m → h → mb → hb) → (m ′ → h ′ → mb ′ → hb ′ )) | (t = tick _min ∧ m ′ = m + 1 ∧ h ′ = h ∧ hb ′ = h ∧ mb ′ = m ∧ mb ∈ Z ∧ hb ∈ Z)∨ (t = tick _hour ∧ m ′ = 0 ∧ h ′ = h + 1 ∧ hb ′ = h ∧ mb ′ = m ∧ mb ∈ Z ∧ hb ∈ Z)∨ (t = tick _midnight ∧ m ′ = 0 ∧ h ′ = 0 ∧ hb ′ = h ∧ mb ′ = m ∧ mb ∈ Z ∧ hb ∈ Z)} . . . THEOREMS thm1 : check _Machine_Consistency(clock ) thmInspectInvEVTM5 : ¬check _Machine_AllowedMachineHoleSub(clock , {m → h → mb → hb | mb ∈ Z ∧ hb ∈ Z ∧ h ∈ Z ∧ m < 55} , {(m → h → mb → hb) → (m ′ → h ′ → mb ′ → hb ′ ) | m ′ = m + 5 ∧ h ′ = h ∧ hb ′ = h ∧ mb ′ = m ∧ mb ∈ Z ∧ hb ∈ Z}) thmInspectInvEVTH5 : ¬check _Machine_AllowedMachineHoleSub . . . thmInspectInvEVTMH1 : ¬check _Machine_AllowedMachineHoleSub . . . END
Listing 14: Clock resulting after the strengthening of the invariant To guarantee that the identified bad-events are no longer triggerable, the predicates are negated in thmInspectInvEVTM5, thmInspectInvEVTH5 and thm-InspectInvEVTHM1. These theorems are proven to hold, demonstrating that the provided specification prohibits the presented inconsistent behaviour.

Reachability

Requirements. The reachability property is not natively available in Event-B. Such a property can be expressed using the EB4EB framework. Reachability property asserts that particular states can be attained under given constraints. The definition used below asserts that there exists a trace where a given state is reachable. This definition differs from the eventually operator of LTL. Note that a formalisation of the eventually operator of LTL is available in [START_REF] Mendil | Non-intrusive annotation-based domain-specific analysis to certify event-b models behaviours[END_REF][START_REF] Riviere | Formalising liveness properties in Event-B[END_REF].

THEORY T h e o 4 R e a c h a b i l i t y IMPORT THEORY EvtBTheory TYPE PARAMETERS ST AT E, EV EN T OPERATORS // At l e a s t one " t r g S e t " e v e n t i s t r i g g e r a b l e a f t e r " s r c " e v e n t At_Least_One_Triggerable_Evt <p r e d i c a t e > ( m : Machine(STATE , EVENT ) , src : EVENT , trgSet : P(EVENT ) ) . . . // A l l " SubSetEvt " e v e n t s d e c r e a s e t h e " v a r i a n t " VariantDecrease <p r e d i c a t e > ( m : Machine(STATE , EVENT ) , variant : P(STATE × Z), SubSetEvt : P(EVENT ) ) . . . // For a l l " SubSetEvt " e v e n t s , t h e " v a r i a n t " i s a N a t u r a l number NaturalVariant <p r e d i c a t e > ( m : Machine(STATE , EVENT ) , variant : P(STATE × Z) , SubSetEvt : P(EVENT ) ) . . . // When " v a r i a n t " i s not n u l l , t h e r e e x i s t s a " SubSetEvt " t r i g g e r a b l e e v e n t One_Next_Evt_Is_Triggerable <p r e d i c a t e > ( m : Machine(STATE , EVENT ) , variant : P(STATE × Z) , SubSetEvt : P(EVENT ) ) . . . // " t r g " e v e n t i s r e a c h a b l e from " s r c " e v e n t t h r o u g h a t l e a s t one "

SubSetEvt " e v e n t Evt_Is_Reachable_From_Definition <p r e d i c a t e > ( m : Machine(STATE , EVENT ) , src : EVENT , trg : EVENT , SubSetEvt : P(EVENT ) , variant :

P(STATE × Z) ) well-definedness Machine_WellCons(m) , trg ∈ Progress(m) , src ∈ Event(m) , Inv (m) ◁ variant ∈ Inv (m) → Z , Mch_INV (m),SubSetEvt ⊆ Progress(m) d i

r e c t d e f i n i t i o n

NaturalVariant(m, variant, SubSetEvt)∧ // P r e s e r v e t h e " v a r i a n t " n a t u r a l VariantDecrease(m, variant, SubSetEvt)∧ // " SubSetEvt " d e c r e a s e t h e " v a r i a n t "

Next_Conv _Evt_Is_Triggerable(m, variant, SubSetEvt)∧ // t h e " v a r i a n t " a r e a l w a y s p o s s i b l e t o d e c r e a s e At_Least_One_Triggerable_Evt(m, src, SubSetEvt)∧ // " s r c " can t r i g g e r a " SubSetEvt "

variant -1 [Z \ N] ∩ Inv(m) ⊆ Grd(m)[{trg}] // " v
a r i a n t "=0 can t r i g g e r " t r g " . . . END Listing 15: Thoery of reachable property in Event-B A trace σ of a machine m is a sequence of states s 0 , s 1 , . . . where s 0 is in the AP of the initialisation event and, for two consecutive state s i , s i+1 in the trace, s i must satisfy the guards of at least one event and (s i , s i+1 ) must satisfy the before-after predicate of this event. For k ≥ 0, σ(k) denotes the k-th state s k of the trace. Then, s j is reachable from s i (denoted

s i Rs j ) if and only if ∃σ, k, n • n ≥ 0 ∧ σ(n) = s i ∧ k > 0 ∧ σ(n + k) = s j .
Reachability PO definition. The reachability property s i Rs j is encoded using the Event-B meta-theory (Listing 15). The Theo4Reachability theory begins by defining the At_Least_One_Triggerable_Evt predicate, which states that, for any state reached after the source event, the guard of at least one target event is enabled. Then, the predicates VariantDecrease and NaturalVariant are defined. The former is satisfied only if, for machine m, each event of the set decreases the given variant; the latter ensures that the guards of the SubSet-Evt events imply that the variant is a natural number. The One_Next_Evt_Is_-Triggerable predicate evaluates to true in machine m if the given variant is positive and at least one event in SubSetEvt is activated.

These four operators formalise the induction-based definition of reachability. They are used to define the main predicate, Evt_Is_Reachable_From_-Definiton, stating that, in machine m, target event trg can be triggered after a (finite) sequence of SubSetEvt event triggers for the given variant, beginning with src event. Formally, triggering src activates at least one event in SubSetEvt and each event of SubSetEvt decreases the variant and enables at least one other event of SubSetEvt, and then trg is enabled when the variant reaches 0. Listing 16: Clock machine with a reachable property checked Clock machine reachability PO for clock model. In the clock model of Listing 6, it is worth checking that midnight is reachable from the initial event. This analysis is performed with theorem thmReach (see Listing 16), that checks whether the event tick_midnight is reachable from the event init, via events tick_min and tick_hours. The proposed variant is then v = 24 * 60 -2 -(m + h * 24). Proving the generated POs for this theorem establishes reachability.

Proof assessment

The defined operators of the proposed framework have been designed in the spirit of Event-B, i.e., 1) complex analyses are decomposed into simple ones (case of reachability in Section 4.4) and 2) expressed in a single semantic setting: the one of Event-B (reflexive modelling) with set theory. This formalisation is influenced by two characteristics of the proof process, that 1) the Rodin prover is efficient when handling set expressions, and 2) theories may define customised proved rewrite rules, that may be summoned manually or automatically in the proof. Automatic rewriting rules that substitute operators by definitions are automatically generated. These rules are written to extract relevant information from machine objects, add them to the hypotheses, and produce multiple simpler goals. They are defined to be applied automatically and chained together, greatly improving proof automation. Indeed, these rewrite rules are included in Rodin's user-defined proof tactics, once and for all, increasing automation when proving the theorems formalising the newly defined POs. 3 presents the proof statistics for each analysis. The important number of nodes (representing atomic steps) in the proof trees is due to the extensive use of theory operators which the prover cannot handle directly, and thus their definitions must be unfolded. The introduction of the rewrite rules in a proof tactic perform automatically these unfold and reductions, making almost all steps fully automatic despite the introduction of the meta level (An entry of 0 in the interactive nodes column of Table 3). The rightmost column provides the number of tactic applications (iterations) during the proof. Indeed, a single tactic application may not be sufficient to fully discharge the proof goals.

Positioning this approach

Related work

Formalising model analyses has been addressed by several authors: Riccobene et al. [START_REF] Riccobene | Towards an interchange language for ASMs[END_REF] presented the ASM-Metamodel (AsmM) for Abstract State Machine (ASM) models considering core modelling constructs and semantics, expressed as an API manipulating ASM-related concepts like abstract machines, signatures, terms, rules, and so on. It is used to embed ASM in another formal method. This work resulted in a number of analyses, tools, and extensions for a variety of purposes [START_REF] Gargantini | A metamodel-based language and a simulation engine for abstract state machines[END_REF]. A similar approach exists for VDM with MURAL, an interactive mathematical reasoning environment extended to support VDM [START_REF] Bicarregui | Reasoning about VDM developments using the VDM support tool in Mural[END_REF] specifications based on meta-modelling concepts, and designed to offer a theorem prover for VDM models. Similarly, the Rodin tool offers an API for handling Event-B models, intended to be used to develop plug-ins. This API is used by ProB [START_REF] Leuschel | ProB: A Model Checker for B[END_REF] as well as by plug-ins handling model development [START_REF] Hoang | A composition mechanism for refinement-based methods[END_REF] and 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].

Ebner et al. [START_REF] Ebner | A metaprogramming framework for formal verification[END_REF] described the meta-programming framework used in Lean, which is an interactive theorem prover based on dependent type theory. This framework provides a means for reflecting object-oriented expressions into a meta-language by extending Lean's object language, based on Lean's modelling constructs. In [START_REF] Van Der | Reflection in Agda[END_REF], the authors present reflection in Agda in the style of Lisp, MetaML, and Template Haskell, as well as several typed programming applications. The MetaCoq [START_REF] Sozeau | The MetaCoq Project[END_REF] project proposed a certified meta-programming environment in Coq based on meta-modelling Coq concepts, including typing and operational semantics. This certified meta-modelling environment was also used in the development of the CertiCoq [START_REF] Anand | CertiCoq: A verified compiler for Coq[END_REF] certified compiler project. Similarly, this reflection principle [START_REF] Fallenstein | Proof-producing reflection for HOL -With an application to model polymorphism[END_REF] is implemented in Isabelle/HOL to build a HOL model within HOL to analyse and reason about various modelling concepts such as infinite hierarchy of large cardinals, polymorphism, verifying systems with selfreplacement functionality, etc. In PVS, Miltra et al. [START_REF] Mitra | PVS strategies for proving abstraction properties of automata[END_REF] proposed strategies for proving abstraction relations between automata, based on theories and templates. This mechanism generalises proofs, making them highly reusable. With regard to Event-B, the formalisation of contexts (and only contexts) in the Event-B language has been proposed [START_REF] Bodeveix | Event-B formalization of Event-B contexts[END_REF]. In related approaches, the B method has been embedded in PVS [START_REF] Muñoz | Structural embeddings: Mechanization with method[END_REF], to benefit from the modelling power of B, while accessing the proving power of the PVS theorem prover. However, this embedding is not formalised, and leads to the use of two separate methods.

Abstract interpretation showed its power to check system properties (absence of runtime errors, dead code, ...). Frameworks like [START_REF] Brat | IKOS: A framework for static analysis based on abstract interpretation[END_REF][START_REF] Bühler | Structuring an Abstract Interpreter through Value and State Abstractions:EVA, an Evolved Value Analysis for Frama-C[END_REF][START_REF] Cousot | The astreé analyzer[END_REF] apply to programs through the definition of parameterised abstract domains corresponding to model analyses. The correctness of these analyses is expressed outside the framework.

The proposed approach is based on reflecting Event-B in itself i.e. its elements can be used as first-class objects in models. This is similar in Coq and HOL based approaches using dependent types, except that 1) it relies on set theory and FOL, easing transfer to other formalisms and 2) it is defined in the same setting as the state-transitions model of the system to be designed.

Advantages of the approach

This paper highlights several advantages of the EB4EB framework.

-Formal modelling and verification integrated in EB4EB. This framework enables the simultaneous use of two approaches for both modelling (operational with machines or axiomatic with contexts) and proving (meta-theorybased and model/induction-based) allowing users to use one or the other nonintrusively on pre-existing models. The proposed theories of the EB4EB framework can be easily extended following the methodology introduced in this paper, to handle new reusable models analyses by introducing, in Event-B, new automatically generated POs that preserve the semantics of Event-B.

-Easing proof process. The EB4EB reflexive framework enables the explicit manipulation of Event-B components by introducing meta-elements such as re-quired datatypes, operators and theorems, extremely useful for expressing complex problems as well as proposing new reasoning mechanisms. However, due to the lack of advanced level proof engines such as SMTs, this resulted in enormous manual proof efforts. The introduced proved proof rules reduce interactive proof efforts while increasing proof automation.

-On-the-fly analysis. The EB4EB framework, which includes reasoning extensions, enables on-the-fly model analysis as well as advanced reasoning level for each Event-B model in the refinement chain. Note that the majority of Event-B models consist of several refinement layers, where each model of a given abstraction level can be analysed; i.e, the model is lifted as an instance of the EB4EB meta-level and is submitted for performing model analyses, at an advanced reasoning level, ensured by new POs generation.

-Correctness of the defined analyses. The EB4EB framework associates a trace to any Event-B machine (trace-based semantics). Such semantics is used to prove the correctness of the defined analyses. Indeed, a theorem stating that the property specifying a given model analysis holds on the traces of a machine is defined for this purpose. Such a correctness theorem has been proved for each of the analyses introduced in Section 4.

Conclusion

This paper presented a technique allowing a designer to define new POs for Event-B corresponding to model analyses that are not available in core Event-B. It is based on the extension of the reflexive EB4EB framework and its meta-theory EvtBT heo. The defined extended reasoning mechanisms and POs are not available in core Event-B. They have been defined as Event-B metamodelling concepts allowing to express deadlock-freeness, bad-events and invariant strengthening, and reachability. It is demonstrated that non-intrusive analysis for Event-B models formalised in Event-B can be performed, at any abstraction level in the refinement chain, and without resorting to another formal method, which would require additional proofs to ensure the correct embedding of Event-B in that method. Moreover, the proof process has been enriched with relevant and proved rewrite rules, included in tactics, leading to a high level of proof automation. All the developments shown in this paper are completely formalised and all the proofs are realised 1 .

Two future directions extending this work have been identified. The first one consists in defining domain-specific engineering theories in order to define specific domain-oriented properties as POs to be satisfied by system models. Such an approach opens towards standard conformance and certification. The second future direction exploits the fact that EB4EB defines an Event-B machine as an instance of a meta-theory as a set of axioms and theorems instances in FOL and set theory. This format can be exported into the higher order framework Dedukti [START_REF] Boespflug | Dedukti: A Universal Proof Checker[END_REF][START_REF] Dowek | Deduction modulo theory[END_REF], and thus makes way for the design of correct import in, and export from Event-B of formal models through Dedukti.

BAP_WellCons

  <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_WellCons <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) Event_WellCons <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 partition(Event(m), {Init(m)}, P rogress(m)) . . . Machine_WellCons <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 ellCons(m) ∧ Grd_W ellCons(m) ∧ Event_W ellCons(m) ∧ . . .

Listing 2 :

 2 Operators to check well-defined data-type (static semantics)

Mch_THM

  <p r e d i c a t 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_One_Ev <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : EV EN T ) well-definedness 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) Mch_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 M ch_IN V _Init(m) ∧ (∀e • e ∈ P rogress(m) ⇒ M ch_IN V _One_Ev(m, e)) 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_One_Ev <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), e : Event) well-definedness 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}]) 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 M ch_F IS_Init(m) ∧ (∀e • e ∈ P rogress(m) ⇒ M ch_F IS_One_Ev(m, e)) Mch_VARIANT_One_Ev <p r e d i c a t e > . . . Mch_VARIANT <p r e d i c a t e > . . . Mch_NAT_One_Ev <p r e d i c a t e > . . . Mch_NAT <p r e d i c a t e > . . .

Listing 3 :

 3 Well defined Data-type operators (behavioural semantics) The details of the invariant preservation (INV -3 and 4 in Table

2

 2

  ) and feasibility (FIS -5 in Table 2) POs are shown in Listing 3. Three operators are associated to the definition of these POs: Mch_INV_Init, stating that an invari-ant holds at initialisation (i.e., states after the AP are included in the invariant states, AP (m) ⊆ Inv(m)); Mch_INV_One_Ev, stating that any event e characterised by its guard and BAP preserves the invariant (e.g. the image of invariant states through BAP is included in invariant states, BAP (m)[{e}][Inv(m) ∩ Grd(m)[{e}]] ⊆ Inv(m)); and Mch_INV, the conjunction of these two operators, where Mch_INV_One_Ev must hold for all progress events. Similarly, three operators Mch_FIS_Init, Mch_FIS_One_Ev and Mch_FIS_Init define the event feasibility PO (existence of a next state after AP or BAP of progress events). The other POs in Table

  check_Machine_Consistency <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ))

THEORY

  Theo4PO IMPORT EvtBTheo TYPE PARAMETERS ST AT E, EV EN T, T Args OPERATORS [PO]_Definition <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), args : T Args ) well-definedness condition . . . d i r e c t d e f i n i t i o n . . . check_Machine_[PO] <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), args : T Args ) well-definedness condition M achine_W ellCons(m) d i r e c t d e f i n i t i o n [PO]_Def inition(m, args) END Listing 7: Analyses Theory Pattern CONTEXT MachinePO EXTENDS M a c h i n e I n s t a n c e THEOREMS thmPO : check_M achine_[PO](m, args) END Listing 8: Analyses Machine Checking PO context pattern. Listing 8 shows an Event-B context pattern for checking the newly defined PO. A consistent instance machine context M achine-Instance, that defines the Event-B machine m by instantiation of the meta-theory EvtBT heo, is extended by context M achineP O instantiating the extended theory T heo4P O. Theorem thmP O performs the check of the defined PO for machine m. The associated WD and THM POs are automatically generated.

THEORY

  Theo4Deadlock IMPORT EvtBTheo TYPE PARAMETERS ST AT E, EV EN T OPERATORS DeadlockFreeness_Definition <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)] . . . END Listing 9: DeadlockFree Theory CONTEXT C l o c k D e a d l o c k F r e e EXTENDS C l o c k M a c h i n e I n s t a n c e THEOREMS thmDeadlock : check_M achine_DeadLock(clock) END Listing 10: Clock DeadlockFreeness Following the defined pattern, Listing 9 introduces a new theory Theo4Deadlock with two new operators together with the required WD condition. Deadlock-freeness PO for Clock model. Listing 10 shows the context with thm-Deadlock theorem generating WD and THM POs of the clock machine.

tick_M5 WHERE g r d 1 :

 1 m < 55 THEN a c t 1 : m :| m ′ = m + 5 END Listing 11: An Bad-event: progress by 5 min.

THEORY

  EvtBTheorySubs IMPORT THEORY EvtBTheory TYPE PARAMETERS ST AT E, EV EN T OPERATORS AllowedMachineHoleSub_Definition <p r e d i c a t e > (m : M achine(ST AT E, EV EN T ), nGrd : P(ST AT E), nBAP : P(ST AT E × ST AT E)) d i r e c t d e f i n i t i o n nBAP [ I n v (m) ∩nGrd ] ⊆ I n v (m) . . . END

  CONTEXT C l o c k R e a c h a b i l i t y EXTENDS C l o c k M a c h i n e I n s t a n c e THEOREMS thmReach : check_M achine_Evt_Is_Reachable_F rom(clock, init, tick_midnight, {tick_min, tick_hour}, {m → h → v | v = 24 * 60 -2 -(m + h * 24)}) END

1

  https://www.irit.fr/~Peter.Riviere/models/

Table 1 :

 1 Global structure of Event-B Contexts, Machines and Theories

(1) Ctx Theorems (ThmCtx)

Table 2 :

 2

Relevant POs for Event-B contexts and machines used throughout this paper. Three externally defined Event-B analyses and POs are introduced in Section 4 and applied to the case study. The positioning of this work with respect to the state of the art and its advantages are discussed in Section 5. Finally, Section 6 concludes the paper and discusses future work.

Table 1

 1

.c). Theories define new data types, operators, and theorems. Data types (DATATYPES clause) define constructors to build inhabitants of the defined type. It may define various operators further used in Event-B expressions as FOL predicates or expressions producing actual values (<nature> tag). Operators may be used in theories, contexts and machines.

  n s t a n c e SETS Ev , Z × Z CONSTANTS clock , tick_min , tick_hour , tick_midnight , init AXIOMS axm1 : clock ∈ Machine(Z × Z, Ev ) axm2 : partition(Ev , {init}, {tick _midnight}, {tick _hour }, {tick _min}) axm3 : State

Table 3 :

 3 Proof statistic for the Clock model and its analyses Table


Renaud Côte

Sergio Bellizzi

Bruno Cochelin

Philippe Herzog

Pierre-Olivier Mattei

Transferts

P O Mattéi

Transferts d'énergie acoustique dans un tube au moyen d'un absorbeur non-linéaire avec source sinusoïdale

Keywords: Réduction du bruit, modes non linéaires, équilibrage harmonique

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

Au début des années 2000, un nouveau concept de réducteurs de vibrations a été développé [START_REF] Gendelman | Energy pumping in nonlinear mechanical oscillators : Part I -Dynamics of the underlying hamiltonian systems[END_REF] [START_REF] Vakakis | Energy pumping in nonlinear mechanical oscillators : Part II -Resonance capture[END_REF]. Il s'agit d'absorbeurs de type non linéaire qui fonctionnent suivant un phénomène appelé pompage énergétique ou transfert d'énergie ciblé (appelé aussi dans la littérature Targeted Energy Transfer (TET)). L'absorbeur est constitué d'un élément élastique purement non linéaire et dissipatif qui couplé au système permet un transfert irréversible d'énergie du système primaire vers l'absorbeur qui la dissipe en limitant l'amplitude la réponse du système primaire. L'absorbeur non linéaire fonctionne, alors, comme un puits où il y a une localisation du mouvement et d'énergie (il est appelé dans la littérature Nonlinear Energy Sink (NES)). L'avantage de ce type d'absorbeur par rapport aux absorbeurs linéaires traditionnels est qu'il peut être efficace dans une bande de fréquence large grâce à sa nature non-linéaire. Par contre, le transfert d'énergie ne se produit que quand l'énergie contenue dans le système primaire a dépassé un certain seuil. On trouvera une description complète du concept dans [START_REF] Vakakis | Nonlinear targeted energy transfer in mechanical and structural systems[END_REF]. Des applications en vibration sont décrites par exemple dans [START_REF] Gourdon | Nonlinear energy pumping under transient forcing with strongly nonlinear coupling : Theoretical and experimental results[END_REF] [START_REF] Nucera | Application of broadband nonlinear targeted energy transfers for seismic mitigation of a shear frame : Experimental results[END_REF].

Dans le cadre de la réduction du bruit, le concept de TET constitue une opportunité de développer des systèmes passifs de réduction du bruit efficaces à basse fréquence. La mise en évidence du TET en acoustique a été présentée dans [START_REF] Cochelin | Experimental evidence of energy pumping in acoustics[END_REF]. Le système primaire était un milieu acoustique, le NES une membrane viscoélastique soumise à des grandes amplitudes et fixée sur une paroi d'une boîte reliée sur le coté apposé au milieu acoustique. L'air contenu dans la boîte permettait le couplage entre le milieu acoustique et le NES. L'étude expérimentale complète est décrite dans [START_REF] Bellet | Experimental study of targeted energy transfer from an acoustic system to a nonlinear membrane absorber[END_REF]. Plus récemment, des travaux ont montré qu'un haut-parleur utilisé comme piston suspendu et travaillant au-delà de son domaine linéaire pouvait être utilisé comme NES [START_REF] Mariani | Toward an adjustable nonlinear low frequency acoustic absorber[END_REF]. Le principal avantage de la technologie hautparleur par rapport à la technologie membrane réside dans la perspective de pouvoir ajuster de façon indépendante divers paramètres du NES (par exemple la masse mobile ou l'amortissement).

Ce travail concerne l'étude de l'efficacité d'un NES quand il est utilisé sans boîte de couplage. Le milieu acoustique est constitué d'un tube incluant un évent latéral recouvert d'une membrane viscoélastique. La modélisation retenue permet de considérer le milieu acoustique comme un système multimodal. Une analyse modale non linéaire du système complet (milieu acoustique+NES) non amortie et non forcée est réalisée. Elle permet d'analyser l'influence de la position de la membrane le long du tube. Une analyse des réponses forcées périodiques permet de mesurer l'efficacité du NES sur les résonances successives du tube. Le lien entre modes non linéaires et réponses forcées est mis en évidence sur l'ensemble des résonances. Ce travail numérique est réalisé dans le domaine des fréquences à l'aide la méthode par équilibrage harmonique.

Description du problème 2.1 Géométrie

On considère ici le milieu acoustique schématisé sur la figure 1. Il est constitué d'un tube de section S t , fermé à son abcisse x = 0 et ouvert à son extrémité x = L. A l'abcisse x = αL le tube présente une ouverture, fermée par une membrane de section S m , de masse m m . Une pression acoustique p s (t) est imposée en x = L. Le tube peut être décomposé en 3 parties. Dans les parties 1 et 3, le comportement est celui d'un tube classique. Dans la partie 2 la membrane affecte le comportement acoustique. Afin de simplifier les notations, nous considérerons la partie 2 comme étant de largeur nulle. Le problème n'est pas modifié, mais la description acoustique dans la zone autour de x = αL s'écartera probablement de la réalité physique.

0 αL L x Centre Gauche Droite p - v - p + v + S t S m p s 0 αL L x Amplitude de p

Equations de base

Nous utilisons les équations classiques de l'acoustique

∂ 2 p(x,t) ∂t 2 = c 2 0 ∂ 2 p(x,t) ∂x 2 , ρ ∂v(x,t) ∂t = -∂p(x,t) ∂x (1)
avec les notations usuelles : p(x, t) la pression, x la variable d'espace, t le temps, c 0 la célérité des ondes acoustiques dans l'air, et v(x, t) la vitesse de l'air.

Les conditions aux limites sont : côte fermé -vitesse nulle, côté ouvert -pression nulle v(0, t) = 0, p(L, t) = 0.

(

) 2
Nous utilisons la décomposition de la pression acoustique p(x, t) = p p (x, t) + p r (x, t) sous la forme d'une onde progressive p p (x, t) et d'une onde rétrograde p r (x, t).

En x = αL, nous imposons les lois de continuité de la pression et de conservation du débit

p -(t)(= p p (α -L, t) + p r (α -L, t)) = p + (t)(= p p (α + L, t) + p r (α + L, t)) = p(t) (3)
S t [v + (t) -v -(t)] = 1 2 S m q (4)
avec respectivement p -et v -la pression et la vitesse prises en x = αL par valeurs inférieures, et p + et v + la pression et la vitesse prises en x = αL par valeurs supérieures et les relations suivantes pour

p p et p r p p (α -L, t) = p r (α -L, t - 2α -L c 0 ), (5)
p p (α + L, t) = p s (t + 2(1 -α + )L c 0 ) -p r (α + L, t - 2(1 -α + )L c 0 ). ( 6
)
Le comportement non linéaire de la membrane est décrit par l'équation du mouvement (voir [START_REF] Bellet | Experimental study of targeted energy transfer from an acoustic system to a nonlinear membrane absorber[END_REF])

m m q + C q(t) + k 1 q + k 3 q 3 = 1 2 S m p(αL, t) (7)
où q représente le déplacement du centre de la membrane suivant la normale extérieure et m m , C, k 1 et k 3 caractérisent la masse, l'amortissement et l'élasticité de la membrane.

Le problème acoustique peut être appréhendé intuitivement en représentant graphiquement la forme de l'onde suivant le tube. Pour une vibration de fréquence proche du premier mode de la cavité sans membrane, en présence de la membrane l'amplitude de vibration prend la forme représentée figure 1.

Equations du mouvement dans le domaine des fréquences

En combinant l'équation (3) et l'équation (4) préalablement dérivée par rapport au temps, la pression acoustique p(t) et le déplacement de la membrane q(t) sont reliés dans le domaine des fréquences par la relation

P (ω) = ω S m S t ρc 0 cos ω αL c0 sin ω (1-α)L c0 cos ω L c0 Q(ω) + P s (ω) cos ω αL c0 cos ω L c0 (8)
où P (ω) (respectivement Q(ω) et P s (ω)) désigne la transformée de Fourier de p(t) (respectivement q(t) et p s (t)).

En reportant, l'expression (8) dans l'équation [START_REF] Bellet | Experimental study of targeted energy transfer from an acoustic system to a nonlinear membrane absorber[END_REF], le déplacement de la membrane vérifie la relation

Q(ω)   iωC -m m ω 2 + k 1 - ω 2 S 2 m S t ρc 0 cos ω αL c0 sin ω (1-α)L c0 cos ω L c0   + k 3 T F (q 3 )(ω) = S m 2 P s (ω) cos ω αL c0 cos ω L c0 (9)
où T F (f ) désigne la transformée de Fourier de la fonction temporelle f .

Les équations (8)(9) modélisent le système vibroacoustique représenté sur la figure 1 dans le domaine des fréquences. L'équation (8) est simplement linéaire alors que l'équation (9) est une fonction implicite du déplacement de la membrane. Cette formulation permet d'étudier le système pour les fréquences de résonance successives. Les modes non linéaires associés au système étudié sont caractérisés par le système (8)(9) pour C = 0 et P s (ω) = 0.

3 Analyse du comportement acoustique L'étude est menée ici pour les valeurs numériques suivantes des paramètres : L = 1 m, S t = 0, 63 m 2 , S m = 0, 063 m 2 , m m = 14 g, k 1 = 0, k 3 = 1, 18 × 10 6 N/m 3 et C = 3 × 10 -4 kg/s. Ces valeurs numériques correspondent à la configuration nominale discutée dans [START_REF] Bellet | Experimental study of targeted energy transfer from an acoustic system to a nonlinear membrane absorber[END_REF]).

Modes non linéaires

Dans un premier temps nous nous intéressons aux modes non-linéaires. Nous choisissons de résoudre l'équation (9) par équilibrage harmonique en ne considérant qu'un seul terme dans le développement en série Fourier des solutions périodiques. On peut alors exprimer Q à partir de l'équation (9) sous la forme

Q = 1 3k 3   m m ω 2 -k 1 + ω 2 S 2 m S t ρc 0 cos ω αL c0 sin ω (1-α)L c0 cos ω L c0   . (10)
L'analyse de l'expression ci-dessus, illustrée par la figure 2, donne plusieurs informations. En premier lieu, on identifie une asymptote linéaire d'expression mm 3k3 ω. Ensuite on remarque l'annulation du dénominateur du terme de droite pour les modes propres du tube d'ordre impair, correspondant à des asymptotes verticales à ces fréquences. Enfin, le numérateur de ce même terme présente la possibilité de changer de signe selon les valeurs de α et ω, ce qui ouvre la possibilité de solutions nulles ou non existantes à certaines valeurs de ω. Ces annulations correspondent à un changement de signe entre Q et P la première composante de Fourier de p(t). C'est le passage d'une situation où q(t) et p(t) sont en phase (Q + ) à une situation où ils sont en opposition de phase (Q -). Autour de chaque fréquence de résonance, ces observations sont compatibles avec le comportement d'un système de type masseressort à un degré de liberté. La particularité du système étudié ici est qu'il présente une infinité de résonances, avec un passage continu d'une résonance à l'autre. Figure 2 -Gauche : composante de Fourier de q(t). Droite : fréquence en fonction de l'énergie mécanique du système et de ses éléments (α = 0, 9). La partie droite de la figure présente la fréquence en fonction de l'énergie mécanique du système (E m ) et de ses composantes E mN ES , E m (x < αL) et E m (x > αL), respectives à la membrane, à la partie gauche et droite du tube. Son comportement est lui aussi semblable à d'autres systèmes non-linéaires. On remarque en particulier les zones au dessus des modes impairs du tube où le rebroussement de E - m est compatible avec un phénomène de pompage.

La figure 3 illustre l'effet de α. Pour α = 1/3 on constate la disparition du mode de résonance dont le noeud est situé à l'emplacement de la membrane. Pour les autres valeurs de α le rebroussement observé sur E - m est plus ou moins marqué. On peut aussi remarquer qu'il existe des fréquences auxquelles l'énergie s'annule pour l'une des deux portions du tube. A ces fréquences, l'énergie est localisée sur la membrane et sur une unique portion du tube. La phase relative des composantes à droite et à gauche de la membrane s'inverse -leurs composantes de Fourier changent de signe relatif-, et comme leur expression est continue l'une d'elles s'annule nécessairement.

Le cas extrême α = 1 annule le terme en √ ω dans l'expression (10), il ne reste plus qu'une courbe continue proche de l'asymptote en ω.

Réponses forcées périodiques

On s'intéresse maintenant aux réponses forcées périodiques résultant d'une source acoustique sinusoidale. L'équation (9) est toujours résolue par équilibrage harmonique en ne considérant qu'un seul terme dans le développement en série Fourier des solutions périodiques. Les solutions sont valables dans le cadre des hypothèses de l'acoustique linéaire non dispersive, en particulier avec une amplitude et une fréquence source suffisamment faibles devant les dimensions du problème. Pour α = 0.9, les figures 4 et 5 illustrent l'effet de l'amplitude de la source sur les réponses suivant la pression (figure 4) et le déplacement de la membane (figure 5) autour des trois premières résonances du système acoustique. Pour faciliter l'analyse de ces courbes, nous avons reporté en rouge l'évolution des modes non linéaires. Pour les trois zones en fréquence, on constate qu'à faible niveau d'excitation le système résonne à la pulsation du système acoustique seul. Passé un certain seuil d'excitation, la résonance se décale sur la gauche avec une limitation de l'amplitude de la pression (zone de pompagedeuxième colonne de la figure 4). Pour des niveaux supérieurs d'excitation, le système résonne suivant l'autre mode non linéaire. Ces comportements sont typiques du comportement TET.

Conclusions

Les modes non linéaires du système décrit ici présentent certaines similitudes (asymptotes et résonances) avec des systèmes de type masse-ressort. Le couplage tube-membrane direct est particulier, ainsi que la localisation de l'énergie mécanique préférentiellement dans les portions résonantes du tube. On note aussi l'annulation de la résonance dont le noeud de pression est placé sous la membrane. La réponse forcée montre la possibilité de pompage à plusieurs fréquences avec un seul NES, pour des paramètres accessibles expérimentalement. Des travaux numériques et expérimentaux abordant la stabilité, ou des réponses spectrales plus complexes, sont envisagés.

Figure 1 -

 1 Figure 1 -Milieu acoustique avec le NES (gauche) et forme d'onde (droite).

Figure 3 -

 3 Figure 3 -Q(ω) et ω(E m ) pour α valant respectivement 0,3 ; 1/3 ; 0,4.

Figure 4 -

 4 Figure 4 -Réponses forcées périodiques en pression P (ω) (α = 0.9)

Figure 5 -

 5 Figure 5 -Réponses forcées périodiques en déplacement Q(ω) (α = 0.9)


Vincent Fréour

Louis Guillot

Hideyuki Masuda

Christophe Vergez

Bruno Cochelin

Numerical continuation of periodic solutions with constraints: application to a physical model of wind musical instrument

. Nevertheless, one problem often encountered concerns the uncertainty on some parameters of the model, the values of which are set arbitrarily because too difficult to measure experimentally. In this work we propose a novel approach where constraints based on experimental measurements are added to the system, as well as the uncertain parameters of the model relaxed. This approach allows the continuation of the periodic solution with constraints to be performed, together with the calculation of the variation of the relaxed parameters along the solution branch. A successful application of this technique to a physical model of a trumpet is presented in this paper.

Physical model of the {player-trumpet} system and continuation

We consider a one-dimensional lip model, coupled to the resonator impedance described by a series of complex modes similar to what is proposed in [START_REF] Fréour | Numerical continuation of a physical model of brass instruments: Application to trumpet comparisons[END_REF]. The coupling between the mechanical oscillator and the acoustic resonator is achieved by a stationary Bernoulli flow equation, considering turbulent mixing in the mouthpiece with no pressure recovery. The mechanical and acoustic equations are given in system 1, where y is the vertical lip position (y 0 is the lip position at rest), ω l , Q l , µ l and b the lip mechanical parameters, s k and C k with k ∈ [1, N ] the modal parameters of the N resonances of the acoustic impedance of the instrument, Z c the characteristic impedance, u the volume flow, p the downstream pressure at the input of the instrument (in the mouthpiece), and p 0 the upstream (mouth) static pressure.

ÿ(t) + ω l Q l ẏ(t) + ω l 2 (y(t) -y 0 ) = 1 µ l (p 0 -p(t)) ṗk (t) = Z c C k u(t) + s k p k (t), ∀k ∈ [1, N ] (1)
with p(t) = 2 The case of a negative opening of the lips is managed by introducing the function θ(y) which enforces u = 0 if y < 0. The modal parameters of the N modes of the impedance are extracted from the measured input impedance using the high resolution method ESPRIT [START_REF] Roy | Esprit: Estimation of signal parameters via rotational invariance techniques[END_REF]. In this model, the values of the lip parameters are critical but particularly difficult to set, as it is extremely difficult to evaluate them experimentally. We choose to work with the Asymptotic Numerical Method (ANM) implemented in the software MANLAB [START_REF]MANLAB web site[END_REF]. This method is based on the expansion of the solutions under the form of truncated Taylor series, providing analytical formulations of the branch of solution. Recently, this method has been associated to the Harmonic Balance Method (HBM) for the search of periodic solutions of oscillating systems [START_REF] Cochelin | A high order purely frequency-based harmonic balance formulation for continuation of periodic solutions[END_REF]. One requirement of MANLAB relies on the recast of nonlinearities of the model into, at most, quadratic nonlinearities. The complete quadratic dimensionless model can be found in [START_REF] Fréour | Numerical continuation of a physical model of brass instruments: Application to trumpet comparisons[END_REF].

Continuation with constraints

Two constraints are introduced as follows:

p L2 = Sγ + I, (2)
where γ = p 0 /P M is the dimensionless mouth pressure with P M = µ l ω l 2 y 0 , S and I are constant values, and

p L2 = 2 N k=1 ℜ(p k ) L2
. The second constraint simply writes as follows:

f 0 = F, (3)
where F is a constant value. Adding two equations to the system requires two parameters of the model to be relaxed, that is two unknowns to be introduced. We choose to relax Q L and ζ = Z c by 0 2 ρP M (ζ can be seen as an "embouchure" parameter). This requires to recast the system of equations in order to preserve the quadratic property of the model.

Figure 1 shows the result of continuation with constraints applied to the physical model described in previous section. In the bottom plot, the evolution of p L2 with respect to γ measured on a trumpet player during a slow crescendodecrescendo maneuver is represented in red. A linear fit of the red curve is applied, which gives S and I (Eq. 2) and defines the constraint on p L2 . The constraint on f 0 is such as it remains constant and equal to the value at the initial calculation point (about the playing frequency of a Bb4). It can be seen that the two constraints are well respected: f 0 is constant with respect to γ, and p L2 evolves linearly with respect to γ (the solution branches, in blue, are superimposed with the target constraint on Fig. 1 bottom plots). The stability of the branch was computed and the branch was found stable across the whole range of γ. The variations of ζ and Q L are represented on the two top plots. Significant variations of these two variables are observed, showing the importance of adapting these parameters in order to match the constraints. These results highlight the ability of the ANM to calculate the evolution of some parameters of the model while applying some mathematical constraints to the output of the continuation calculation. By defining these constraints from experimental data, this approach can be seen as an inversion method, allowing to retrieve the parameter values of the model necessary to achieve a given performance (playing a crescendo-decrescendo at completely constant playing frequency). This method then shows great perspectives for the parametrisation of physical models of brass instruments, as well as for objective comparison of brass instruments.

N

  k=1 ℜ(p k (t)) and u = 2|p0-p| ρ b • sign(p 0 -p) • θ(y), where θ(y) = |y|+y 2 , b is the lip width and ρ is the air density.

  Figure1: Results from continuation with constraints. Evolution of ζ, QL, f0 and p L2 with respect to the dimensionless mouth pressure γ. In red is the evolution of p L2 with respect of γ measured on trumpet player during a slow crescendo-decrescendo maneuver.

	0.15
	0.1
	0.05
	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6
	8
	7
	6
	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6
	480
	479
	478
	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6
	2
	1
	0
	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6