Aznam Yacoub
email: aznam.yacoub@lsis.org

Maamar El

Amine Hamri
email: amine.hamri@lsis.org

Claudia Frydman
email: claudia.frydman@lsis.org

Chungman Seo
email: cseo@rtsync.com

Bernard P Zeigler
email: zeigler@rtsync.com

DEv-PROMELA : An Extension of PROMELA for the Modeling, Simulation and Verification of Discrete-Event Systems

Keywords: DEv-PROMELA, Simulation, Formal Verification, Verification and Validation

PROMELA is a well-known formalism for the modeling and the verification of concurrent systems. PROMELA deals with high-level specifications. As a result, PROMELA models are expressed in a high-level abstraction which not considers explicit representation of time or events for example. But, the efficiency of the processes of Verification and Validation relies on the accuracy of the models. That is why we propose in this paper work to develop a new extension of PROMELA for the modeling of discrete-event systems. The verification of these models is then done by combining formal verification and simulation-based verification using SPIN and the tool DEv-PROMELA Studio, or using any existing DEVS simulators.

Introduction

Verification & Validation (V&V) is becoming a critical point in the understanding and design of large systems like weather events, traffic lights, aircraft autopilot, smart systems, etc. Developing software or hardware without failure and in which people can put their trust is a big challenge for experts and designers. Many research fields have explored solutions to this problem for many years, and two domains have emerged. On the one hand, theory of Modelling & Simulation (M&S) [START_REF] Bernard | Theory of Modeling and Simulation[END_REF] provides an intuitive way to model systems by specifying inputs, outputs, states and a time-advance function expressing the evolution of the model through time, then encapsulating this simple behaviour into black boxes and reusing them to design more complex systems. Even the harder system can thus be quickly analyzed, but the efficiency of simulations strongly depends on the hypothesis made on the system under study and on the played scenarios. Indeed, testing the entire state space appears like impossible, due to the impossibility for designers to think to all possible cases; or it will take a too long time as simulation can deal with big inputs.

On the other hand, Formal Methods (FM), especially model-checking [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in cesar[END_REF], are well-known to systematically explore the total state space of a model in order to check that it satisfies behavioural properties. However, formal methods can encouter some limits: for example, Timed Automata (TA) are not able to represent systems with non-linear clock constraints [START_REF] Alur | A theory of timed automata[END_REF]. The main problem is that the formal verification models need to focus on the conceptual aspects of a design that are relevant to the properties one wants to verify for two reasons: this guarantees the efficiency of the model-checking algorithms within a reasonable time when the state space may be huge, and it is shown that many problems are undecidable, resulting that the model-checking cannot be performed in these cases.

The literature thus provides some techniques on combining formal verification and simulation for specific fields like validation of integrated circuit design [START_REF] Li | Integrated design validation: Combining simulation and formal verification for digital integrated circuits[END_REF] or system-level performance analysis [START_REF] Kunzli | Combining simulation and formal methods for system-level performance analysis[END_REF], and shows the benefit of combining simulation and formal verification. These approaches propose to enhance V&V process by partitioning the model and using on each part either formal verification or simulation if the first is not applicable. However, there is no guarantee that each part is expressed in the right level of abstraction. These methods generally imply remodelling part of systems which one wants to check, or provide some morphism rules between multiple formalisms to get a verification model from a simulation model. In this context, we propose another methodology to combine simulation and model checking. In our approach, we build a new specification language (called the target formalism) upon a verifiable language (called the source formalism) by integrating semantics which comes from simulation. This increases the expressiveness of the source formalism without breaking its formal verification capabilities. Then, simulation is used in order to verify and validate some properties that formal verification could not verify and without remodelling the considered part of the system under study. Thereby, each part of a system can be verified and validated at many levels of abstraction. Moreover, thanks to the power of the Discrete-EVent system Specification (DEVS) Framework, each submodel can be combined into another complex model which can represent the entire system at a level of abstraction. The behaviour of the global model is thus verified and validated by simulation, overcoming the weakness of formal methods applied to complex systems.

One result of our proposed approach is the Discrete-Event PROMELA (DEv-PROMELA) which we introduced in DEv-PROMELA is based on the well-known PROcess MEta LAnguage [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF] and on the Classic DEVS semantics [START_REF] Bernard | Theory of Modeling and Simulation[END_REF]. It allows accurate modelling of discrete-event systems (DES) in a syntactical way and their verification and validation by using both formal verification and simulation. Another advantage of DEv-PROMELA is that specifying a DES model into a syntactic formalism makes easier the translation from the conceptual model to a computerized simulation model. Indeed, transformation rules can easily be defined and verified between two syntactic formalisms. This advantage is crucial because it also allows a kind of interoperability between existing simulators. By using the DEv-PROMELA Studio which integrates the SPIN model checker [START_REF] Gerard | The model checker spin[END_REF] and a DEVS simulator on the one hand, and the MS4 Me environment [START_REF] Seo | Devs modeling and simulation methodology with ms4 me software tool[END_REF] to illustrate the interoperability on the other hand, DEv-PROMELA has been successfully applied in order to model, verify and simulate designs of simple algorithms, but also more complex conceptual models of video games.

sciences" [START_REF] Cousot | A gentle introduction to formal verification of computer systems by abstract interpretation[END_REF], and whose the objective is to check whether a model is correct against some formal specifications. Formal verification methods are based on rigorous and mathematical proof techniques. Indeed, Formal Methods are a set of formal notation and tools that allow a strict and rigourous description of the system under study, with formal semantics and an automatic proof mechanism [START_REF] Bowen | Applications of Formal Methods[END_REF]. Formal Methods are divided into two families:

• Automated theorem proving methods [START_REF] Chang | Symbolic Logic and Mechanical Theorem Proving[END_REF][START_REF] Loveland | Automated Theorem Proving: A Logical Basis[END_REF][START_REF] Duffy | Principles of Automated Theorem Proving[END_REF] show that a set of statements of a system can be deducted from another set of statements. Formally, we consider Γ, a set of logical properties describing the system (we called them axioms and hypothesis), and φ a set of specifications (that we called conjectures).

Theorem proving methods try to find a proof that Γ φ, in other words, that we can syntactically deduce specifications from properties of the system.

• Model Checking methods [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in cesar[END_REF] show that a system satisfies a set of properties. Formally, we consider M , a model (in the mathematical sense) of the system, and φ, a set of logical properties. Model Checking methods check whether M |= φ : all models M syntactically and semantically satisfy φ. In fact, because the system is generally modelled by a finite automaton, model checking tools systematically explore the entire state space of the system model, inducting to the well-known state space explosion problem, which is extensively treated in the literature [START_REF] Clarke | The birth of model checking[END_REF][START_REF] Huth | Logic in computer science: modelling and reasoning about systems[END_REF][START_REF] Baier | Principles of Model Checking[END_REF].

With these definitions, we can easily understand why formal methods are powerful methods to check the correctness of a system. Indeed, whatever the family of formal methods, they are based on logics that is the best way to describe properties in an unambiguous manner, and on mathematical formalisms, most of the time state machines, that are also the best way to describe systems in an unambiguous manner. However, it is well-known that these techniques could become very heavy, time and effort consuming because they require advanced mathematical skills and knowledge [START_REF] Heitmeyer | On the need for practical formal methods[END_REF], and are not very practicable in large and complex systems. Although model checking research is focusing on efficiency and scalability, formal methods are faced with the complexity of systems and data domains [START_REF] Zervoudakis | Cascading verification: An integrated method for domain-specific model checking[END_REF].

The complexity of systems comes from the complexity of their behaviour and interactions between their internal components, on the one hand, and their environment, on the other hand. Consequently, in order to be efficient and effective, formal methods have to apply some restrictions to their modelling and specifications languages, reducing their expressive capabilities. Consequently, some assumptions can lead to a certain idealisation or rigorous hypothesis which are not representative of the real environment of the system. The obtained model is certainly simpler than the real design, but it also increases the requirement of some expertise to ensure the level of abstraction is appropriate. The problem does not arise from the abstraction process itself, because making models is making abstraction, but the way in which we do abstraction and how we simplify models in order to make them fit the tools' requirement. Abstraction [START_REF] Clarke | Model checking and abstraction[END_REF] has many advantages: it guarantees, for instance, that the model system is finite (or finitely represents an infinite-state system [START_REF] Widjaja | Model checking infinitestate systems: generic and specific approaches[END_REF]), which is a condition for model checking techniques work [START_REF] Baier | Principles of Model Checking[END_REF]. Consequently, this means that a set of problems cannot be checked with formal verification methods, without making strong assumptions. For instance, it is shown in [START_REF] Alur | A theory of timed automata[END_REF] that certains classes of timed automata are undecidable and not computable for model checking. Another example is given by [START_REF] Zeigler | Combining devs and model-checking: Using system morphisms for integrating simulation and analysis in model engineering[END_REF] for the Cyber-physical Autonomous Cooperative System of Systems (CACSoS). The authors state that "Despite these drastic simplifications, state space explosion prevents employing more than a handful of Uninhabited Air Vehicles (UAVs) and sensors". Finally, only strong expert knowledge can guarantee that the semantics and restrictions of the model checker tool is enough to make a correct abstraction of the system. Furthermore, it is relevant to consider how models are built. Abstraction-Refinement (A-R) process [START_REF] Hsieh | Model abstraction for formal verification[END_REF][START_REF] Clarke | Model Checking[END_REF][START_REF] Grumberg | Abstraction and refinement in model checking[END_REF] is commonly used to approximate more effectively the behaviour of the original system, by iteratively adding details to abstract states, abstract algorithms and types and constants, before verifying the newly obtained model [START_REF] Draper | The refinement of embedded software with the bmethod[END_REF]. However, A-R loop involves a problem: when the abstraction does not satisfy a property, it does not mean that the real model does not satisfy this property. And because refinement involves restrictions, refinement is perhaps representative of only a part of the checked problem. This is especially true when it is difficult to prove that the correctness of a refinement against a property implies the correctness of the real model against this same property. Indeed, it is a vicious circle: the more the model is refined, the less it represents the real system because of restrictions that the modellers add, although it makes the verification easier. Conversely, the less a model is refined, the more it is imprecise or not verifiable with formal methods (that is the generalisation problem stated by [START_REF] Baier | Principles of Model Checking[END_REF]). Finally, according to Baier, "complementary techniques, such as testing, are [thus] needed to find fabrication faults (for hardware) or coding errors (for software)", although testing is not possible all the time. The latter point leads to a discussion of the interoperability and universality of formal methods. There exists many formal methods, each having an appropriate expressiveness power to describe specific models. This is particularly problematic because experts may have strong knowledge in each formal method, but also because formal methods could return different results for the same design: [START_REF] Owen | Combining Complementary Formal Verification Strategies to Improve Performance and Accuracy[END_REF] shows, for instance, Cadence SMV and NuSMV give two different results for the same requirement and the same input model. In that sense, we can state that each formal method is specialised as regards a type of system. This can be a problem to justify the use of a formal method instead of another.

Introduction to Discrete-Event Simulation

M&S domain has been explored since the early 1960s, but was really theorised in [START_REF] Bernard | Theory of Modeling and Simulation[END_REF]. This theory tried to make uniform these two notions used extensively in many disciplines like medicine, physics, etc; it also defines a global and universal framework and methodology that is not dependent on the domain of application. As the name suggests, the two key concepts behind M&S are "Model" and "Simulation". The most popular definition of "model" is perhaps the one given in [START_REF] Minsky | Matter, mind and models[END_REF]: "To an observer B, an object A* is a model of an object A to the extent that B can use A* to answer questions that interest him about A". Model is then an abstraction, a simplification, a representation of the reality. This definition joins the one given in formal verification domain, even in the mathematical sense. Indeed, a model is a semantic interpretation of a structure. Simulation is thus "executing a model to generate its behaviour" [START_REF] Bernard | Theory of Modeling and Simulation[END_REF], by acting on inputs and parameters of the model. Experimental Frame (EF) is a set of conditions under which the real system is observed. This notion is also important because it implies a certain abstraction. From this, a model will be valid in a specific EF (i.e. the model generates the same behaviour as the real system in the given conditions) but not in another. This is the main limitation of simulation. Indeed, we can easily deduce that simulation strongly depends on the played scenarios. Unlike formal methods which explore the entire statespace, simulation focuses only on an identified part of the statespace. In other words, doing an exhaustive verification with simulation is hard and maybe impossible.

Another advantage of M&S is that Zeigler defines a unique and universal formalism to describe discreteevent system in a generic manner. DEVS formalism and its extensions allows modelling a full-range of discreteevent systems as simple transition system. All these contribute to make the M&S framework very easy to use for modelling and simulation of many types of systems, like complex natural phenomena [START_REF] Wainer | The cell-devs formalism as a method for activity tracking in spatial modelling and simulation[END_REF].

In the V&V terminology, an analogy can be made between testing and simulation. The weakness of simulation is due to this being an empirical method. Correctness of the simulation essentially comes from the precision of the assumptions made on the EF. Then, simulation-based verification depends on specific scenarios and conditions under which it is tested. This does not mean the entire state space cannot be checked as for formal verification, but it would be probably more costly (and because efficiency of a simulation model can only be evaluated by comparing its outputs with those of the real system for specific inputs). Note that because simulation is evaluated under specific EF, this enforces the notion of determinism; in other words, for the same set of inputs, the model must generate the same behaviour and the same outputs.

Complementarity between Simulation and Formal Verification

In order to overcome the weakness of formal methods and simulation, the litterature explores some techniques which combine these methodologies. Firstly, papers concerning formal verification and model checking clearly consider simulation. According to [START_REF] Baier | Principles of Model Checking[END_REF] : "In order to improve the quality of the model, a simulation prior to the model checking can take place. Simulation can be used effectively to get rid of the simpler category of modeling errors." [ISS + 06] note that "UPPAAL provides an integrated simulation tool. It allows the user to examine the dynamic system behavior in a graphical manner either interactively, [...] or randomly to let the system run on its own." And SPIN and NuSMV model checkers also integrate a "simulator" [Hol97, CCGR99]. These simulators are not in the sense of M&S concepts because simulation involves determinism of models; however, they can be seen as the result of the need of "executing formal specifications" for the purpose of validation. PROMELA and SMV are based on an operational semantics that allows the execution, but that is not the case for all specification languages. [START_REF] Leuschel | Prob: A model checker for b[END_REF] prefers the term "animation of specification" for their ProB Model Checker.

The need of increasing the credibility of simulation models leads researchers to apply formal methods in M&S [START_REF] Richard Kuhn | Practical application of formal methods in modeling and simulation[END_REF] in order to verify simulation models. Many methods to transform certain DEVS subclasses into Timed Automata for purpose of static verification were developed [START_REF] Hernán | A formal verification approach for devs[END_REF][START_REF] Saadawi | Verification of real-time devs models[END_REF]. Other approaches tend to integrate Z into DEVS models [START_REF] Trojet | Practical application of lightweight z in devs framework[END_REF][START_REF] Trojet | Approche de vérification formelle des modèles DEVS à base du langage Z[END_REF] also by transformation.

What is the problem with existing methodologies ? These techniques combining formal verification and simulation like in [START_REF] Abdulhameed | An approach combining simulation and verification for sysml using systemc and uppaal[END_REF] derive the verification model from the simulation model in order to verify it, or derive a verification and a simulation model from a conceptual model. In the second case, the derivative does not guarantee that the obtained models are related to each other [START_REF] Li | Integrated design validation: Combining simulation and formal verification for digital integrated circuits[END_REF]. In the first case, the verification is about the simulation model (meaning the implementation of the simulator) and not the initial design. Moreover, it implies to apply some restrictions on the simulation model in order to enable the verification. Thus, there is no guarantee that the verification model represents the initial design.

Combining Formal Verification and

Simulation with Discrete-Event PROMELA

Overview

Our proposed methodology tries to reduce and overcome the previous disadvantages. The main idea is introducing the semantics of a discrete-event simulation language into a verifiable language. A similar approach was recently described in [START_REF] Olanrewaju Aliyu | The high level language for system specification: A model-driven approach to systems engineering[END_REF]. The general approach that we propose is as follow:

• Choose a verifiable formalism (like PROMELA, Timed Automata...) called the source formalism.

Identify the missing notions among the three main concepts related to discrete-event simulation: event mechanisms, state lifespan, types of transition (internal or external).

• Introduce syntactical elements into the source formalism in order to enable modelling of these notions. Add a new datatype to model infinite values if needed. If the source formalism is based on state machines, make sure that adding these concepts does not change the structure of the underlying automaton.

• Define the new operational semantics based on the targeted discrete-event simulation formalism (DEVS, G-DEVS [START_REF] Giambiasi | Gdevs: a generalized discrete event specification for accurate modeling of dynamic systems[END_REF], Temporal Sequential Machine [START_REF] Giambiasi | From sequential machines to devs formalism[END_REF]...)

• Use the obtained formalism to design systems.

Then, we can be sure that we are able to easily define a morphism which translates models expressed in the new formalism into models expressed in the source formalism and which conserve all their structural properties. Indeed, the automaton underlying the new formalism is built upon the automaton underlying the source formalism. Moreover, we are also sure that it exists a simulation model which has the same behaviour than the behaviour of the model expressed in the new formalism. Thus, we can easily define a morphism which transforms models expressed in the new formalism into models expressed in the targeted simulation formalism.

In order to illustrate our approach, we apply it to extend PROMELA.

Recall about PROMELA

PROMELA is a specification language with an operational semantics and initially designed for the modelling and verification of concurrent protocols, involving synchronous or asynchronous communication between processes. Based on Djikstra's Guarded Command Language, its syntax is close to any imperative language, making their use very easy, compared with others formal methods. Because the language is very complete, we will focus there only on interesting concepts for the scope of this paper.

A PROMELA specification is thus a set of two separate parts: the system specification, on the one hand, which describes the behaviour of the model, and on the other hand, the properties to verify on the model.

System Specifications

A PROMELA system is a finite set of components: instances of processes. These instances can communicate with each other thanks to different mechanisms as buffered messages, shared global variables or rendez-vous handshakes. Each instance of each process is modelled by a finite set of guarded or labeled command called statements. A statement is said non-blocked if the state of the system allows its execution, otherwise it is said blocked. Then, one execution of the specifications, at any time t i , corresponds to the execution of one among all of non-blocked statements, without any assumption about duration of the statement execution.

Instructions are divided into two categories: statements that modify the system state and controlflow instructions. If none of them is satsfied, the control-flow structure is blocked. PROMELA also provides a timeout instruction (usable as a guard) which is enabled if all instructions are blocked in the whole system.

Datas in PROMELA are represented by local and shared variables. Local variables are those which are relative to only the process which they belong to, whereas global variables are shared by all processes. A variable is characterized by its value and its type, or any finite combination (structures) or finite arrays of these types. Each PROMELA type represent a finite set of values.

The immediate result is that a PROMELA model can be represented by an underlying finite automaton.

Properties Specifications

SPIN supports the verification of Linear Temporal Logic (LTL) properties on the PROMELA models. LTL properties are converted into a never-claim process (comparable to any normal processes) which don't "participate" to the behaviour of the system. The goal of a never-claim process is only to guarantee the system satisfies the property which is encoded in it. In this sense, a never-claim process acts as a monitor. The study of LTL encoding is out-of-scope of this paper. Thus, we recommand the SPIN Reference Manual [START_REF] Holzmann | The SPIN Model Checker : Primer and Reference Manual[END_REF] to the interested readers for further informations.

Then, the formal verification of PROMELA specifications intuitively corresponds to the checking of all executable paths against a given property, without any assumptions of duration. It results that the next state of a PROMELA model does not depend on the time elapsed in a previous state. Because it is not possible to model this elapsed time, timed extensions were developed.

Executability of a Process

A PROMELA process with a set of statements L is thus a finite state machine P = (Q, T, s 0 , F ) where -s 0 ∈ Q, the initial state of the process;

-Q = {q i = (l 1 , ..., l m , g 1 , ..., g n , c 1 , ..., c o ) ∈ m i=1 L i n j=1 G j o k=1 C k },
-F ⊂ Q, the finite set of final states of the process; Denote (q i , q j ) ∈ Q 2 and l ∈ L a statement (i.e. an instruction in the PROMELA program). Then, t ∈ T iff the process can change its state from q i to q j by executing l only. In other words, a statement denotes two consecutive states and t = (q i , l, q j ) (we will note q i l → q j ). Given two states (q i , q j ) and a labelled transition t = q i l → q j , t is enabled iff -l is a non-blocking instruction: an assignment, a conditionnal instruction with a satisfying guard or any control-flow atomic instruction (break, skip, timeout, etc); -l is an asynchronous message sent over a non-full channel;

-l is an asynchronous message received from a nonempty channel;

-l is an unblocking rendez-vous message.

Executability of a Program

A PROMELA program with n processes is a subset of the cartesian product of the state graph of each process. Thus, a PROMELA Program M is a Kripke Structure

[Kri63] K =< S, s 0 , R, L > with -S ⊆ n i=1 Q i , where Q i is the statespace of the process p i (1 ≤ i ≤ n);
-s 0 = (s 01 , ..., s 0n ) where ∀i ∈ [1; n], s 0i is the initial state of the process p i ;

-R ⊆ S × S, the set of transitions. By definition, R is left-total, meaning ∀s ∈ S, ∃s ∈ S such as (s, s ) ∈ R;

-L : S → 2 AP , the labeling function, which gives an interpretation of atomic logic propositions (p ∈ AP ) for each state;

Denote r = (s m , s n ) ∈ S 2 . We note q mi , the state of the process p i in s m , and q ni , the state of the process p i in s n . Thus, r ∈ R =⇒ ∃t ∈ T i \ t = (q mi , l i , q ni ), where T i is the set of transitions of the process p i and l i ∈ L i (here, L i is the set of statements of the process p i ). By this, we mean r is a transition of a PROMELA program only if it exists a transition t that changes the state of one of the processes composing the program. r is said enabled if ∃t ∈ T i which is enabled. If at least two transitions are enabled for any state s, thus the system is said nondeterministic.

Finally, we call run any finite or infinite alternating sequence w ∈ W of states and transitions: w = s 1 r 1 s 2 r 2 ....r n-1 s n . Formal verification thus consists to check all runs w against the desired property. Verification methods and algorithms are out-of-scope of this paper, and we suggest [START_REF] Baier | Principles of Model Checking[END_REF] as reference for the interested reader.

DEVS Concepts

Discrete-Event Systems (DES) are a specific class of timed systems, whose state changes at various time instants, depending on instant occurrences of events. Thus, a DES evolves along the events that it emits or consumes. For the modelling of such systems and their analysis, [START_REF] Bernard | Theory of Modeling and Simulation[END_REF] introduced the DEVS formalism, which can be seen as a generalization of the Moore Machine formalism by associating each state with a lifespan. The traditional DEVS thus relies on the following notions:

• Each state is associated with a real number called lifespan. This real number can take its value on [0; +∞]. When the lifetime of a state has expired, the system emits an output and changes its current state according to the transition table;

• When an input is consumed, the state of the system changes according to the transition table, regardless of the current lifetime of the current state;

• As a result of the previous point, transitions can be characterized as internal or external transitions. Internal transitions model autonomous behaviours while external transitions correspond to reactions to any external events;

• Events are well-dated and can be ordered;

• There is no non-deterministic behaviour. If two events occur at the same time, thus either they are equivalent events (e 1 = e 2 ) or they are prioritized;

• The state, input and output trajectories are piecewise segments; the distribution of events can follow any non-linear function, unlike for discretetime systems in which the time is determined by a linear function of periods;

More formally, a DEVS model is a coupling of DEVS atomic and coupled models. A DEVS atomic model is the smallest simulable unit defined by A = (X, Y, S, δ int , δ ext , λ, ta), where:

• X is the set of input values;

• Y is the set of output values;

• S is the set of states;

• δ int : S → S is the internal transition function;

• δ ext : Q × X → S is the external transition function;

• λ : S → Y is the output function;

• ta : S → R + is the time advance function;

• Q = {(s, e) | s ∈ S, e ∈ [0, ta(s)
]} is the total state set; e is the time elapsed since the last transition.

The meaning of a DEVS can easily be depicted as follows. At any time t, the system is in a state s. If no external event occurs, the system stays in s for time ta(s). If the lifetime expires, meaning the elapsed time e from the last event is equal to ta(s), the system outputs the value λ(s) and changes to the state δ int (s). If an external event x occurs before the expiration time, meaning that the system is in a state q = (s, e) with e ≤ ta(s), then the system changes its state to δ ext (q, x). The event can transit into the coupled model using the previously defined coupling: an external event coming in the system is transmitted to the components using EIC, while an output generated by a component transits using EOC or IC.

Discrete-Event PROMELA

Using our approach, we developed an extension of PROMELA called DEv-PROMELA [YHF + 15], which is the result of introducing the semantics of DEVS into PROMELA. We extended the syntax of PROMELA as shown in [START_REF] Yacoub | Using dev-promela for modelling and verification of software[END_REF], in order to be able to specify DES concepts and real values. DEv-PROMELA is thus a syntactic language which allows modelling, simulating and verifying discrete-event models by formal verification and simulation. Indeed, the methodology implies that we can encode any DEv-PROMELA model into a DEVS model, which can be implemented and simulated in any DEVS environment. Because it always exists a PROMELA model structurally equivalent to a DEv-PROMELA model, the model checker SPIN can be used to check time-invariant properties. The semantics alignement between DEv-PROMELA and DEVS is not the object of this paper, which is only focusing on the structural relationship between DEv-PROMELA and PROMELA.

DEv-PROMELA Syntax

As said in the previous section, some syntactic elements were added to PROMELA in order to model the essential notions of discrete-event models: clocks and types of transitions. Because DEVS allows real valuation, a new data type real was introduced. Each statement of PROMELA denotes a transition between two states. Then, in order to define types of transitions and types of events (internal or external), events descriptors prefix any statement. The reader is encouraged to read [START_REF] Yacoub | Using dev-promela for modelling and verification of software[END_REF] for more details about the syntactic changes.

DEv-PROMELA Semantics

The operational semantics of DEv-PROMELA corresponds to the semantics of DEVS.

Semantics of a DEv-PROMELA process. A DEv-PROMELA process P with a set of statements L is an automaton T = (S τ , E, δ i , δ e , s 0 , F ) where

• S τ = {s i = (t s , i, l 1 , ..., l m , ∈ N × m i=1 L i × n j=1 G j × o k=1 C k )}
is the set of states. i is the identifier of the state related to the statement l which defines it; the sets L i (resp. G j ) are the sets of values of each local (resp. global) variable l i (resp. g j );

• E is the set of events; E contains at least the silent event denoted ;

• δ i : Q f → Q 0 × E is the internal transition partial function;
• δ e : Q × E → Q is the external transition partial function;

• s 0 is the initial state;

• F is the set of final states.

Moreover, we define:

-ta : S τ → R + ta(s) → t s is the state lifetime function; the lifetime of each state is given by the delay before executing the next statement in the specifications;

-Q = {q = (s, dt), ∀s ∈ S τ } such that 0 ≤ dt ≤ ta(s) is the set of total states; dt denotes the time elapsed in the state s;

-Q 0 = {q = (s, 0), ∀s ∈ S τ } ⊂ Q; -Q f = {q = (s, ta(s)), ∀s ∈ S τ } ⊂ Q.
Consider a DEv-PROMELA process P in a state s at time t, and the next statement l with its event descriptor. We can admit the process P is in fact in a state q = (s, t) (if t denotes the elapsed time since the last event). If l denotes an internal transition and if t = ta(s), then the statment l is enabled. The event associated with the transition is emitted to all the other processes composing the program, before the transition is triggered, and the next event for the process P is defined by : d e = getCurrentDate + ta(s ) with ((s , 0), e ) = δ i (s). If l denotes an external transition on an event e, then the transition is triggered only if the process receives the event e. In this case, denote t the date of the event e. The next state is given by q = δ e (q, e) with q = (s , 0). If δ e is not syntactically defined for (s, e), then the next state is given by q = (s, dt) and ta(s) = t s .

Semantics of a DEv-PROMELA program. A DEv-PROMELA program P r is a transition system T = (S, Λ, →) where S is the cartesian product of the set of states of each process, the set of global variables and channels that compose the program, Λ is the set of all statements and → the set of transitions. Consider a program P r at time t and two states s = (s pi , s qj , ...) and s = (s pi , s qj , ...). Then, s l → s with l ∈ Λ if it exists a transition from s pi to s pi , from s qj to s qj , ... and if it does not exist any other transition which can be triggered before the date t. In other words, the next event of P r is the minimum value of all the next events of each process and external events.

Structural Relationship between DEv-PROMELA and PROMELA

Denote P a DEv-PROMELA process with L the set of statements. As previously introduced, P is an automaton A = (S τ , E, δ i , δ e , s 0 , F A ). Denote P , a PROMELA process represented by a finite state machine B = (S, T, s 0 , F B ). If P is a structural equivalent to P , that means it exists a morphism M that transforms P to P , such as:

-∀s i = (l 1 , ..., l n , g 1 , ..., g m ) ∈ S, ∃s i ∈ S τ , s i = (t s , l 1 , ..., l n , g 1 , ..., g m ); we denote S ⊂ S τ by abstraction and φ : S τ → S, the abstraction function;

(1) -∀t s ∈ R + , s i = (t s , l 1 , ..., l n , g 1 , ..., g m ) ∈ S τ =⇒ ∃! s i ∈ S such as s i = φ(s i ) = (l 1 , ..., l n , g 1 , ..., g m );

(2) -∀t = (s i , l, s j ) ∈ T, ∃(s i , s j , e) ∈ S τ × S τ × E such as δ i (s i ) = (s j , e) or δ e (s i , e) = s j , and φ(s i ) = s i and φ(s j ) = s j ; (3)

-∀(s i , s j , e) ∈ S τ × S τ × E, δ i (s i ) = (s j , e)
or δ e (s i , e) = s j =⇒ ∃(s i , s j ) ∈ S × S \ ∃t = (s i , l, s j ) ∈ T and φ(s i ) = s i and φ(s j ) = s j ; (4)

-s 0 = φ(s 0 ); (5) -F = φ(F ). ( 6
)
(1) and ( 2) mean that we can always make a projection of any state of S τ to a corresponding state of S. Moreover, all states s of S τ sharing the same memory state are projected to an unique state s of S with the same memory representation. φ is thus a surjective function.

(3) and ( 4) mean that if it exists a transition function, either internal or external, from any state s i to any state s j , and if s i (resp. s j ) is a projection of s i (resp. s j ) by φ, then it exists a transition from s i to s j . ( 5) and ( 6) means that initial and final states are preserved by abstraction.

Suppose M is constructed by only removing the event descriptors of P. By this, we mean that we delete the concepts of event, state lifetime and the characterization of each transition, in other words the notion of internal and external transition. M is thus an time-abstraction function such as (1) and (2) are verified (all timed states are projected to their untimed equivalent depending only on their memory state). Because we don't remove any statement, (3) and (4) are trivially verified. Indeed, even if a DEv-PROMELA (internal or external) transition is defined between two states q i = (s i , dt i ) and q j = (s j , dt j ) in Q, a such transition exists only if there is a relationship between s i and s j . However, a such relationship is defined syntactically (transitions are defined by the statements). Because we don't remove any statements, a such relationship is always existing, and even for the branching structures. For the same reason, (5) and ( 6) are also true.

Because a PROMELA program is a synchronized product of each automaton that composes it, the graph of DEv-PROMELA program P is included in the one of P . Indeed, the graph of P is composed by the all possible permutation between statements, whereas the graph of P is only composed by the permutation of ordered events. That means, given two events e 1 and e 2 associated to two statement l 1 and l 2 , if date(e 1 ) < date(e 2 )), the graph of P will semantically not take into account the path where l 1 is executed before l 2 (the path may exists, but may be not valid). Thus, the morphism M defined previously is also valid for the entire program.

Discussions

Before presenting applications of DEv-PROMELA, we must shortly answer two questions: why discreteevent simulation and why PROMELA ? For the former question, discrete-event approach has many advantages comparing real-time execution or discretetime approach. The discrete-event nature assumes that a system is constant between two occurences of events. Then, the evaluation of the system is needed only when an event occurs. This substantially reduces the statespace compared to discrete-time approaches which generates a state at fixed rate. Moreover, while real-time execution enforces to really wait an amount of time, discrete-event approach allows jumping from a time to another.

Concerning the second question, we would effectively have been able to extend Timed Automata (TA) and the UPAAL model checker, considering there are already many efforts and a lot of works to encode DEVS into Timed Automata [START_REF] Dacharry | Formal verification with timed automata and devs models: a case study[END_REF]. However, among all the problems we could encouter, the main problem with TA would be about clock constraints. DEVS allows modelling systems with non-constraint clocks, which will be also done in DEv-PROMELA, while TA impose that clocks constraints are linear relations. Then, extending TA would be possible only with the Time Constrained DEVS (TCDEVS) [START_REF] Hernán | Discrete event modeling through a multiformalism approach, from a user-oriented perspective[END_REF].

Applications

A Soccer Video Game

Numerous works try to improve video games development environments [EAMS14, CSC + 15]. In this context, DEv-PROMELA was applied to model, verify, and validate a design of a soccer video game. Indeed, a video game can be seen as a discrete-event system at three levels. At a lower level (the implementation level), a game is a finite automaton in which each instruction is executed after an amount of time (the time needed by the CPU or the GPU to execute an instruction). Thus, an executable statement denotes two states with a defined lifespan. The lifespan can be fixed or can evolve through the time. Moreover, in a higher level (the conceptual level), the design of a game is reactive, because software must react to inputs coming from the player. Each input is an event which is well-dated. If the game is a multiplayer game, events can come from many players. In this case, each player is a component of the system. At a middle level, the game is composed by several components like a graphics engine, a physics engine... which interact with each other. The communications are generally done through mechanisms of events in order to synchronize components. Moreover, we know that a game is just a set of images which are computed with a defined frequency. Thus, each image depends on the time needed to compute it. By extension, we can consider that a new picture is shown when their computation time is done. This corresponds to stay in a state for a defined time, and go to another state in an autonomous manner when the lifespan of the current state is over. If we want to verify the implementation, it seems that a verification model is enough. Indeed, we can easily transform an implementation in a PROMELA model to check liveness properties. Indeed, the verification model will check all of the possible executions to check deadlock states, unreachable states... One can argue also we can use timed automata to model time (i.e. the time needed to compute an image for exemple). However, if modelchecking can check dynamics which depend on time, it is not able to check properties on states that depend themselves on time. For instance, the avatars of a soccer video game move with a defined speed. Because of the discrete nature of software, the new position of the avatar is computed by taking the speed and the time elapsed in a previous state (i.e. the time taken by the CPU/GPU to compute the new image.) By making an linear or a polynomial interpolation (depending on the physics rules), the new positions are computed. In other word, each state of the game itself depends not only on the timed dynamics but also on the time elapsed in a previous state. Then, if we want to verify a property related to collision detection, model-checking cannot be applied because the problem become undecidable [START_REF] Alur | A theory of timed automata[END_REF]. In fact, verification languages will enforce strong abstractions which ensure that the problem remain verifiable (for instance, by enforcing that the domains of values are finite). Then, such cases cannot even be modelled. And even designers makes an abstraction of such properties, this one would not be representative of the real implementation.

With DEv-PROMELA, that kind of properties can be express through the DEVS semantics, like show in Algorithm 2. The clt event descriptors (l.4, l.7) defines the elapsed time before the execution of the next statement. This corresponds to an autonomous behaviour. The value can be a constant or a variable, or any function evaluated to real. However, we introduce also a reactive transition like in DEVS through the evt descriptor (l.12). When the goalkeeper receives an event "MOVE" from any other components of the game, the instruction l.13 is executed. The new state depends on the elapsed time from the last evaluation, because it is defined by the goalkeeper's new position which is computed according to the time. The obtained model is structurally equivalent to the initial model and the classic model-checking can be used to check structural deadlocks and unreachable states (because the structure of software does not depend on time). For instance, the PROMELA model ensures that the score is always a positive value. For behavioural properties (like collision, speed, constraints on position, deadlocks due to absence of events or infinite-life states...), the model is simulated. A simulation-based verification is then performed by checking several scenarios. Scenarios can be randomly generated or defined by the designer.

A Crossroad

Another application of DEv-PROMELA is the classical crossroad problem. We consider a crossroad with four traffic lights. Each traffic lights stays in a state (red, yellow, green) for a defined time, and only two of them can be green at the same time. We want to verify that a controller software respects this constraint.

The problem is verifiable with Timed Automata [START_REF] Alur | A theory of timed automata[END_REF] and timed extensions of PROMELA if the clock of each traffic light evolves linearly. But in the case in which the time elapsed in each state is

A Manufacture Chain

Manufacture problems were classical and already intensively studied in the litterature [DY00, [START_REF] Longo | An application of modeling and simulation to support industrial plants design[END_REF][START_REF] Tajini | Modelling methodology for the simulation of the manufacturing systems[END_REF]. This problem consists on a set of thousand processes which are executed on several batches of products. At each stage of the production, a controller performs some operations which take an amount of time. When an operation is finished, a signal is sent to the controller which leads the batch to the next operation. Operations are just encoded with Bash-like instructions, like shown in Figure 5. In order to show the potentiel of our proposed methodology, we model a chain with only two operations and one sensor, successively using PROMELA, Real-Time PROMELA [START_REF] Tripakis | Extending promela and spin for real time[END_REF] and DEv-PROMELA. Then, we check if there is any unreachable state and that, in any cases, the attribute batch attr1615 is equal to 0 at end of the manufacturing process when attribute 1001 is equal to 0. While the PROMELA and RT-PROMELA models are checked using model-checking, the DEv-PROMELA model is verified using model-checking and discrete-event simulation. The translation from the Bash instruction to PROMELA is very easy. Each operation is encoded using a PROMELA process.

Batches' attributes are modelled using integers variables batch *. The sensor is modelled using a process that randomly changes the values of attributes. Communications between sensors and processes are modelled using channels. With PROMELA, quantitative delays are totally abstracted, because they cannot be modelled, while RT-PROMELA allows modelling of time using clock, as shown in Algorithm 5.

The DEv-PROMELA model 4 is slightly different. Because DEv-PROMELA is based on DEVS, the event mechanism is directly expressed by the transitions, and each event are well-dated. Moreover, even the sensor can be also modelled using DEv-PROMELA, we decided to use a classic DEVS model to represent it. Then, the model-checking is only applied of the model of operations. Then, by coupling the DEv-PROMELA model and the DEVS model of the sensor, we check by simulation the potential deadlocks, while the safety property concerning the attribute 1615 is always checked using model-checking. Results are presented in Table 2. Models Generation. Two subsequent models are generated from the DEv-PROMELA models. The formal verification model is generated using Classic PROMELA by removing the event descriptors, and using the mapping previously defined. The obtained untimed model represents all the possible event permutations, but does not include the time. This level of abstraction is enough to verify structural properties or untimed properties like the one that we want to verify: "Is the attribute 1615 equal to 0 at the end of the manufacturing process ?".

The second model is a DEVS abstract model independant of the target simulator. This model has the same semantics than those of the DEv-PROMELA model. This DEVS abstract model is then implemented in a DEVS simulation model (in this case, in the MS4 Me Environment [START_REF] Seo | Devs modeling and simulation methodology with ms4 me software tool[END_REF]) and simulated to check timed properties. skip; // Log Event PRMCHECWID 10: STEP8511: if 11: ... 12: } Results. As expected, clocks in RT-PROMELA generate a huge statespace compared with PROMELA and DEv-PROMELA. Indeed, both model generated by PROMELA and DEv-PROMELA for formal verification are untimed model. In the three cases, model-checking was able to detect that the event PRMCHECWID is never generated by the model. But, the main difference in this case is about the deadlock found by the checkers. In the case of PROMELA and RT-PROMELA, no deadlock were detected in the model, while DEv-PROMELA allows us to detect some deadlocks. In fact, the problem comes from the model of the sensor. The level of abstraction of time used in PROMELA and RT-PROMELA does not allow modelling cases in which the sensor does not send the laser event. But, the discrete-event simulation shows that it exists some cases in which this event is never generated. In these cases, the model stays locked, and the operation cannot progress. It is important to note that if simulation could detect the deadlock, it was mainly because scenarios were well-chosen. Indeed, simulation-based verification depends on the played scenarios.

The other important aspect of DEv-PROMELA is that we can combine different discrete-event simulation formalisms for the simulation-based verification. Indeed, as we said previously, even we could model the sensor fi;

13: event!PRMCHECWID; 14: ... 15: } using DEv-PROMELA, it is possible to use Petri Nets or any others discrete-event simulation formalisms to model the sensor and combine it with the DEv-PROMELA model (thanks to the DEVS Bus concept). However, in this case, model-checking is like a supportive method to the simulation-based verification.

Discussion about High-Level Verification, Validation and Test Techniques

In brief summary, the literature about Verification, Validation and Test (V&VT) expresses the necessity of improving modelling, implementation, verification and validation techniques, since new systems are increasingly complex. However, it is also admitted that V&VT best practices must focus on high-level specifications and abstractions. For instance, new model-based programming paradigms emerge for the implementation of event-driven systems [START_REF] Milicevic | Model-based, event-driven programming paradigm for interactive web applications[END_REF]. The main goal of such techniques is to reduce the number of errors due to the gap between abstraction and implementation. These methodologies thus focus on separating the problems related to the behaviour of the design on the one hand, from the problems related to the implementation on the other hand (low-level messages, queue, data structures...). In other words, these works are not focusing on how improving existing V&V techniques, but how encouraging developers to focus on specifying the core part of the program under implementation, i.e the event model. DEv-PROMELA is in this spirit by introducing these event-driven aspects in a verification language. However, we think that, if operational details (for example, how real values are implemented into the program) are not relevant for a design and its verification, data abstraction is a source of losing accuracy.

Other works [START_REF] Vakili | Temporal logic model checking in alloy[END_REF] state that, if high-level declarative specification languages like Alloy [START_REF] Jackson | Software Abstractions: Logic, Language, and Analysis[END_REF] are really suitable for high-level modelling of transition systems (i.e the structure), their lack of operational semantics enforce designers to translate models to other tools in order to carry out full model-checking. Vakili and al. [START_REF] Vakili | Temporal logic model checking in alloy[END_REF] also state that "However, if we wish to provide analysis support for these models to increase their quality and utility, we must be able to express the models precisely."

This statement shows that the models need to embed details about how they will behave, independantly of their implementation, but also with respect to their implementation. Especially, the need of encoding temporal logic into declarative specifications shows that untimed models are insufficient to represent systems with accuracy. DEv-PROMELA goes in this direction by adding timed aspects into untimed models. However, DEv-PROMELA goes further by not only focusing on the ordering of event, but also on the relation between the elapsed time, states and properties, by using DEVS and not only temporal logic.

Finally, DEv-PROMELA is a part of this trend that combines model-checking and simulation for enhancing formal verification and formal validation [START_REF] Gore | Conceve: Conceptual modeling and formal validation for everyone[END_REF]. However, while these works focus on the conceptual modelling at the Subject Matter Expert (SME) level, DEv-PROMELA is designed to be used at different specification levels. We mean that our goal is not to make easier the conceptual modelling for a SME. We improve the model-checking results by combining formal verification and simulation. We are not trying to define a new Domain-Specific Language (DSL) that can be then translated into verifiable and simulable specifications, or explaining how a DSL can be translated into a verification model (like ConceVE). However, DEv-PROMELA is designed in order to add more details about time and events in an untimed verifiable model. This new model can be then formally verified or simulated for verying and validating structural properties on the one hand, and behavioural properties in the other hand. This is done by automatically translating the model into a simulation model in order to analyze its behaviour or into a verifiable model to check non-timed properties. In this way, new verification capabilities are added to a verification language, while the model is kept simple and focused on its core aspects.

Conclusion

We described in this paper some work to develop a new approach which really combines discrete-event simulation and formal verification for V&V purposes. The main goal is to add new verification capabilities to existing formal verification languages. The approach consists to extend a verifiable language (called the source formalism) by adding the semantics of the DEVS abstract simulator. Consequently, this ensures that for any model expressed in the extended formalism, it exists an abstraction which can be verified using formal methods. Moreover, it can also be simulated in order to verify timed and behavioural properties which can not be verify with formal methods. A result of this approach is DEv-PROMELA, which is an extension of PROMELA for the modeling and simulation of DES. This is done by introducing the DEVS operational semantics into PROMELA, without breaking the verification capabilities of PROMELA. A DEv-PROMELA model is then a verification model and a simulation model which can be verified by combining formal verification for structural properties and simulation-based verification for behavioral properties. It is interesting to note that a DEv-PROMELA model is a syntactic model. This means that a DEv-PROMELA model can be easily automatically translated and implemented in any DEVS simulator which supports Classic DEVS. As an illustration of this capabilites, we use the MS4 Me environment to perform some simulation-based verifications. DEv-PROMELA was successfully applied to verify and validate designs of video games.

We also applied it on a model a manufacture chain, and compared the result with classic modelchecking. The DEv-PROMELA model was able to reduce the statespace for the verification of timeinvariant properties, while simulation-based verification was able to detect deadlocks that verification models was not able to detect.

One of the major drawbacks of this approach is inherent to the simulation: simulation-based verifications strongly depends on the verified scenarios. Identifying scenarios is a challenge for designers [START_REF] Banks | Discrete-event system simulation[END_REF] and depends on the applications domains. Several simulations and coverage tests must be performed like in [START_REF] Li | Integrated design validation: Combining simulation and formal verification for digital integrated circuits[END_REF] to ensure that the main scenarios were tested. Finally, by integrating discrete-event simulation and formal verification in a same specification language, DEv-PROMELA reduces the risk of errors due to transformations and morphisms.

As future works, we can also explore a way to use simulation in order to speed-up model-checking. Indeed, simulation could allow designers to identify execution paths which have a real meaning in the real world. Then it could be useful in order to limit the statespace explosion problem.

Figure 1

 1 Figure1The Basic M&S entities[START_REF] Bernard | Theory of Modeling and Simulation[END_REF].

  x == 2 ) → x = 3;

  y == 2 ) → y = 4; y == 2 ) → x = 2; 15: :: ( x == 2 ) → y = 4; 16: od; 17: } 18: 19: ltl {[](z == 1); } several guards are satisfied, a random one is selected.

  the finite set of states; a state is characterized by the values of each local and shared variables, and channels (the all sets L i , G j and C k ); -T ⊂ Q × L × Q, the finite set of transitions labeled by a statement l ∈ L;

Figure 2

 2 Figure2The Goalkeeper design error in a soccer video game.

Algorithm 2 :

 2 A DEv-PROMELA model of Goalkeeper. 1: active proctype goalkeeper () { 2: gk state = GK IDLE; clt : 0.5 → emit : silent] 5: ( gk state == GK DIV E ) → 6: gk state = GK IDLE;

  clt : 0.5 → emit : silent] 8: ( shooted && gk state ! = GK CAT CH ) → 9: gk state = GK DIV E; 10: :: [clt : 0.5 → emit : silent] 11: ( gk state == GK IDLE ) → 12: :: [evt : M OV E] else → 13: sk position = sk position -14: speed * getElapsedT ime; 15: ... The verification is then done in two steps. Our tool DEv-PROMELA Studio automatically transforms the DEv-PROMELA specification into a PROMELA equivalent model by removing the event descriptors.

Figure 3

 3 Figure 3 The Crossroad Problem.

Figure 4

 4 Figure 4 The Manufacture Chain. Each square represent a step or a process/operation.

Figure 5

 5 Figure 5 Exemple of the operation 1180.

  Statements relative to state changes are assignments and message exchange instructions. Assignment statements involve local and global variables, whereas communication statements involve buffered channels. It is important to note that, if assignements are always considered as enabled statements (i.e. they can be always executed), the instructions relative to channels can be blocked if the associated buffered channel is empty or full. Controlflow statements are classical conditionnal and loop instructions. These ones allow selection of the next statement among different branches regarding a guard. Because PROMELA processes are non-deterministic, if Algorithm 1: A simple example of PROMELA program.

Table 1

 1 Results of crossroad checking.

			States Transitions Remarks
	DT-PROMELA	1251	2759
	Timed PROMELA	927	1603	Only linear relations between clocks
	DEv-PROMELA	422	834	Simulation allows using of arbitrary clocks
	Algorithm 3: PROMELA model of the operation 1180.
	1: active proctype op1180 () {
	2:	event!PRPMARKLAS;
	3:	event?code; // Log Event PRPMARKLAS
	4:	if
	5:	:: batch attr1001 == 0 → goto STEP8511;
	6:	:: else → skip;
	7:	fi;
	8:	event!PRMCHECWID;
	9:	event?code; // Log Event PRMCHECWID
	10: STEP8511: if
	11:	:: batch attr1615 ! = 0 → goto STEP9000;
	12:	:: else → skip;
	13:	fi;
	14:	event!PRMD0LAS01D;
	15:	event?code; // Log Event PRMD0LAS01D
	16:	event!MSLD0LAS01D;
	17:	event?code; // Log Event MSLD0LAS01D
	18: STEP9000: batch attr1615 = 0;
	19: ...
	20: }
	Algorithm 4: DEv-PROMELA model of the operation 1180.
	2:	[clt : 0.28 → emit : P RP M ARKLAS]
	3:	skip; // Log Event PRPMARKLAS
	4:	if
	5:	:: [evt : laser] batch attr1001 == 0 → goto STEP8511;
	6:	:: [evt : laser] else → skip;
	7:	fi;
	8:	[clt : 0.27 → emit : P RM CHECW ID];

1: active proctype op1180 () { 9:

Table 2

 2 Results of chain checking.

			States Transitions Time Memory Results
	PROMELA	315	558	0.2	128653	4 unreachable states, no deadlock
	RT-PROMELA	945	1697	0.5	256686	4 unreachable states, no deadlock
	DEv-PROMELA	128	353	0.09	100302	2 unreachable states, no deadlock found by model
							checking, deadlocks found in simulation
	Algorithm 5: RT-PROMELA model of the operation 1180.
	1: int batch attr1615;
	2: int batch attr1001;
	3: chan event = [1] of byte;
	4: byte code;
	5:
	6: active proctype op1180 () {
	7:	when {y ≤ 28 } reset { y } event!PRPMARKLAS;
	8:	event?code; // Log Event PRPMARKLAS
	9:	if
	10:	:: batch attr1001 == 0 → goto STEP8511;
	11:

:: else → skip;

12:

Acknowledgement

This work is part of the R&D project "MAGE", from French "Investing for the Future" national program.


Sylvine Durand

Baptiste Lheraud

Isabelle Giraud

Nicolas Bech

Frédéric Grandjean

Thierry Rigaud

Jean Peccoud

Richard Cordaux
email: richard.cordaux@univ-poitiers.fr

Heterogeneous distribution of sex ratio distorters in natural populations of the isopod Armadillidium vulgare

Keywords: Sex ratio distorter, endosymbiont, Wolbachia, f element, sex determination

come

Introduction

Sex ratio distorters (SRD) are selfish genetic elements located on sex chromosomes or transmitted by a single sex, which skew the proportion of males and females in progenies towards the sex that enhances their own vertical transmission [START_REF] Beukeboom | The evolution of sex determination[END_REF]. Major SRD types include sex chromosome meiotic drivers [START_REF] Jaenike | Sex chromosome meiotic drive[END_REF][START_REF] Helleu | Sex chromosome drive[END_REF], some B chromosomes [START_REF] Camacho | B chromosomes and sex in animals[END_REF] and selfish cytoplasmic genetic entities [START_REF] Chase | Cytoplasmic male sterility: a window to the world of plant mitochondrial-nuclear interactions[END_REF][START_REF] Cordaux | The impact of endosymbionts on the evolution of host sexdetermination mechanisms[END_REF][START_REF] Hurst | Reproductive parasitism: maternally inherited symbionts in a biparental world[END_REF]. Collectively, they are found in a wide range of animal and plant species and they have had a tremendous impact on the ecology and evolution of their host species [START_REF] Burt | Genes in conflict[END_REF][START_REF] Werren | Selfish genetic elements, genetic conflict, and evolutionary innovation[END_REF]. One of the most emblematic SRD is the bacterial endosymbiont Wolbachia [START_REF] Werren | Wolbachia: master manipulators of invertebrate biology[END_REF][START_REF] Kaur | Living in the endosymbiotic world of Wolbachia: A centennial review[END_REF]. Wolbachia is a cytoplasmic, maternally inherited alphaproteobacterium found in a wide range of arthropods and nematodes. In arthropods, Wolbachia often manipulates host reproduction in favor of infected females, thereby conferring itself a transmission advantage. This is achieved through various strategies, three of which causing sex ratio distortions towards females: male killing, thelytokous parthenogenesis and feminization of genetic males [START_REF] Cordaux | The impact of endosymbionts on the evolution of host sexdetermination mechanisms[END_REF][START_REF] Hurst | Reproductive parasitism: maternally inherited symbionts in a biparental world[END_REF][START_REF] Werren | Wolbachia: master manipulators of invertebrate biology[END_REF][START_REF] Kaur | Living in the endosymbiotic world of Wolbachia: A centennial review[END_REF].

In the terrestrial isopod Armadillidium vulgare, chromosomal sex determination follows female heterogamety (ZZ males and ZW females) [START_REF] Juchault | Croisement de néo-mâles experimentaux chez Armadillidium vulgare Latr. (Crustace, Isopode, Oniscoide). Mise en evidence d'une hétérogamétie femelle[END_REF][START_REF] Chebbi | The Genome of Armadillidium vulgare (Crustacea, Isopoda) Provides Insights into Sex Chromosome Evolution in the Context of Cytoplasmic Sex Determination[END_REF][START_REF] Cordaux | Characterization of a Sex-Determining Region and Its Genomic Context via Statistical Estimates of Haplotype Frequencies in Daughters and Sons Sequenced in Pools[END_REF]. However, many females produce progenies with female-biased sex ratios, due to the presence of two feminizing SRD: Wolbachia endosymbionts and a locus called the f element [START_REF] Cordaux | The impact of endosymbionts on the evolution of host sexdetermination mechanisms[END_REF][START_REF] Rigaud | The evolution of sex determination in isopods crustaceans[END_REF][START_REF] Cordaux | Evolutionary Significance of Wolbachia-to-Animal Horizontal Gene Transfer: Female Sex Determination and the f Element in the Isopod Armadillidium vulgare[END_REF]. Wolbachia symbionts cause ZZ genetic males to develop as phenotypic females [START_REF] Martin | Mise en évidence d'un micro-organisme intracytoplasmique symbiote de l'Oniscoide Armadillidium vulgare L. dont la présence accompagne l'intersexualité ou la féminisation totale des mâles génétiques de la lignée thélygène[END_REF]. Three Wolbachia strains have been described in A. vulgare, for which feminization induction has been demonstrated (wVulC and wVulM strains [START_REF] Rigaud | Feminizing endocytobiosis in the terrestrial crustacean Armadillidium vulgare Latr. (Isopoda): Recent acquisitions[END_REF][START_REF] Cordaux | Evidence for a new feminizing Wolbachia strain in the isopod Armadillidium vulgare: evolutionary implications[END_REF]) or is strongly suspected (wVulP strain [START_REF] Verne | Evidence for recombination between feminizing Wolbachia in the isopod genus Armadillidium[END_REF]). The f element is a nuclear insert of a large portion of a feminizing Wolbachia genome in the A. vulgare genome [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF]. The f element induces female development, as a W chromosome does, and it shows non-Mendelian inheritance, making it an SRD [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF][START_REF] Legrand | Nouvelles données sur le déterminisme génétique et épigénétique de la monogénie chez le crustacés isopodes terrestres Armadillidium vulgare Latr[END_REF]. These SRD may cause turnovers in sex determination mechanisms [START_REF] Cordaux | The impact of endosymbionts on the evolution of host sexdetermination mechanisms[END_REF][START_REF] Rigaud | The evolution of sex determination in isopods crustaceans[END_REF][START_REF] Juchault | Transfer of a parasitic sex factor to the nuclear genome of the host: A hypothesis on the evolution of sex-determining mechanisms in the terrestrial isopod Armadillidium vulgare Latr[END_REF] and they could explain why sex chromosome systems are so variable in terrestrial isopods [START_REF] Juchault | Evidence for female heterogamety in two terrestrial crustaceans and the problem of sex chromosome evolution in isopods[END_REF][START_REF] Becking | Diversity and evolution of sex determination systems in terrestrial isopods[END_REF][START_REF] Becking | Sex chromosomes control vertical transmission of feminizing Wolbachia symbionts in an isopod[END_REF][START_REF] Russell | Evolutionary transition to XY sex chromosomes associated with Y-linked duplication of a male hormone gene in a terrestrial isopod[END_REF].

Testing this hypothesis requires characterizing the evolutionary dynamics of SRD such as Wolbachia and the f element in natural populations. In A. vulgare, this characterization is quite limited because prior studies were mostly restricted to a narrow geographic area (western France), sometimes focusing solely on Wolbachia [START_REF] Verne | Evidence for recombination between feminizing Wolbachia in the isopod genus Armadillidium[END_REF][START_REF] Juchault | Contribution à l'étude qualitative et quantitative des facteurs contrôlant le sexe dans les populations du crustacé isopode terrestre Armadillidum vulgare Latreille. I. La population de Niort (Deux Sèvres)[END_REF][START_REF] Grandjean | Mitochondrial DNA polymorphism and feminizing sex factor dynamics in a natural population of Armadillidium vulgare (Crustacea, Isopoda)[END_REF][START_REF] Rigaud | Mitochondrial DNA polymorphism, sex ratio distorters and population genetics in the isopod Armadillidium vulgare[END_REF][START_REF] Verne | Effects of parasitic sex-ratio distorters on host genetic structure in the Armadillidium vulgare-Wolbachia association[END_REF]. The only exception is a 1993 study [START_REF] Juchault | EVOLUTION OF SEX DETERMINATION AND SEX-RATIO VARIABILITY IN WILD POPULATIONS OF ARMADILLIDIUM-VULGARE (LATR) (CRUSTACEA, ISOPODA) -A CASE-STUDY IN CONFLICT-RESOLUTION[END_REF], which collated and extended results from the early 1980's [START_REF] Juchault | Contribution à l'étude qualitative et quantitative des facteurs contrôlant le sexe dans les populations du Crustacé Isopode terrestre Armadillidium vulgare Latr. II -Populations hébergeant le facteur féminisant F (bactérie intracytoplasmique)[END_REF][START_REF] Juchault | Contribution à l'étude qualitative et quantitative des facteurs contrôlant le sexe dans les populations du Crustacé isopode terrestre Armadillidium vulgare Latreille. III. Populations n'hébergeant pas le facteur féminisant F (bacteroïde intracytoplasmique)[END_REF]. The main observations were that Wolbachia and the f element are present at variable frequencies in field populations, and the f element is more frequent than Wolbachia. However, earlier studies were limited by the lack of molecular tests for Wolbachia and/or the f element, preventing any direct assessment of SRD presence. Instead, the authors used a complex, indirect procedure combining a physiological test and crossings [START_REF] Juchault | EVOLUTION OF SEX DETERMINATION AND SEX-RATIO VARIABILITY IN WILD POPULATIONS OF ARMADILLIDIUM-VULGARE (LATR) (CRUSTACEA, ISOPODA) -A CASE-STUDY IN CONFLICT-RESOLUTION[END_REF]. In addition to being tedious and time-consuming (generation time is one year in this species), this procedure did not allow direct and undisputable assessment of SRD presence. Moreover, it could only be run on females and therefore provided no information on SRD presence in males. Finally, it could not reveal individuals potentially carrying both SRD.

Here, we took advantage of the availability of molecular markers to directly assess SRD presence in males and females from A. vulgare field populations from Europe and Japan. This approach allowed us to circumvent the limitations of previous studies, and to revisit the population dynamics of Wolbachia and the f element in this species and their association mitochondrial lineages.

Materials and Methods

647 A. vulgare individuals from 16 natural populations across Europe and Japan were collected by hand. Individuals were sexed and stored in alcohol or at -20°C prior to DNA extraction. Total genomic DNA was extracted from the head and legs of each individual, as described previously [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF]. We used four molecular markers to assess the presence of Wolbachia and the f element in DNA extracts: Jtel [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF], wsp [START_REF] Braig | Cloning and characterization of a gene encoding the major surface protein of the bacterial endosymbiont Wolbachia pipientis[END_REF], recR [START_REF] Badawi | Signs of Neutralization in a Redundant Gene Involved in Homologous Recombination in Wolbachia Endosymbionts[END_REF] and ftsZ [START_REF] Werren | Evolution and phylogeny of Wolbachia: reproductive parasites of arthropods[END_REF] (Table S1). While Jtel is specific to the f element, wsp and recR are specific to Wolbachia, and ftsZ is present in both the f element and Wolbachia [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF]. We assessed the presence or absence of these markers by PCR, as described previously [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF]. Different amplification patterns were expected for individuals with Wolbachia only (Jtel-, wsp+, recR+, ftsZ+), the f element only (Jtel+, wsp-, recR-, ftsZ+), both Wolbachia and the f element present (Jtel+, wsp+, recR+, ftsZ+) or both Wolbachia and the f element lacking (Jtel-, wsp-, recR-, ftsZ-). The few individuals exhibiting other amplification patterns were classified as "undetermined status". A quantitative-PCR assay was used to measure Wolbachia titer in some individuals (see supplementary Methods). To characterize Wolbachia strain diversity, wsp PCR products were purified and Sanger sequenced using both forward and reverse primers by GenoScreen (Lille, France). Forward and reverse reads were assembled using Geneious® v.7.1.9 to obtain one consensus sequence per individual. To evaluate mitochondrial diversity, we amplified by PCR a ~700 bp-long portion of the Cytochrome Oxidase I (COI) gene in all individuals [START_REF] Folmer | DNA primers for amplification of mitochondrial cytochrome c oxidase subunit I from diverse metazoan invertebrates[END_REF]. PCR products were purified and Sanger sequenced as described above. Haplotype network analysis was performed using the pegas package [START_REF] Paradis | pegas: an R package for population genetics with an integrated-modular approach[END_REF]. All statistical analyses were performed with R v.3.6.0 [START_REF]R: A language and environment for statistical computing[END_REF]. Figures were realized with ggplot2 [START_REF] Wickham | ggplot2: Create Elegant Data Visualisations Using the Grammar of Graphics[END_REF].

Results

We tested the presence of Wolbachia and the f element in 423 females and 224 males from 16 populations across Europe and Japan (Tables 1,S2). While most males lacked both SRD, 48% of females carried at least one of them. The remaining females presumably carry W chromosomes, although the existence of other feminizing elements cannot be formally excluded. As expected for feminizing elements, the SRD were mostly found in females, the f element being more frequent than Wolbachia overall. Both SRD were found in the same individuals in only 3 females from a single population (Chizé). Wolbachia-infected individuals carried one of the three previously known Wolbachia strains of A. vulgare: wVulC (n=62), wVulM (n=23) or wVulP (n=4).

Wolbachia and f element distribution in females was highly heterogenous among populations (Figure 1a). These SRD were found in 10 and 11 out of 16 populations, but they reached frequencies >10% in only 6 and 7 populations, respectively. The two SRD coexisted in 8 populations. A generalized linear model predicting the frequency of the f element as a binomial response by the proportion of individuals carrying Wolbachia (each statistical unit being a population) showed that the prevalence of the two SRD was significantly negatively correlated (9.8% of deviance explained, Chi-squared test, p < 7.9 × 10 -8 , 14 df) (Figure 1b). Hence, in Floirac, Poitiers, Saint Julien l'Ars and Pisa populations, Wolbachia was frequent (23-94% frequency in females) and the f element was rare (0-8%). By contrast, the f element was frequent (35-96%) and Wolbachia was rare (0-11%) in Prague, Beauvoir, Chizé, Coulombiers and La Crèche populations. In the other populations, both SRD were found at low to moderate frequency (0-19%), including 3 populations devoid of both SRD (Lastovo, Hyogo and Bucharest).

Males carrying Wolbachia or the f element were found in 2 and 4 out of 16 populations, respectively. In all cases, these males occurred in populations in which the corresponding SRD were the most prevalent ones in females: Beauvoir, Chizé, Coulombiers and La Crèche for the f element, and Floirac and Saint Julien l'Ars for Wolbachia. Overall, these males had much lower Wolbachia titer than females from their respective populations (Figure S1, Table S3).

The 642 individuals sequenced at the COI gene presented a total of 92 segregating sites defining 23 haplotypes (named I to XXIII; GenBank accession numbers in Table S4), with 1 to 7 haplotypes per population (Table S2, Figure 2). The most frequent and widespread haplotype (I) was found in 188 individuals from 10 populations. The second most frequent and widespread haplotype (V) was found in 106 individuals from 7 populations. We found 21 out of the 23 haplotypes among individuals lacking both Wolbachia and the f element (Table 2, Figure 2). Among individuals carrying the f element, 6 haplotypes were found, all but one (I, II, III, V and VI) being shared with individuals lacking both Wolbachia and the f element, and one (IV) being carried by a single individual in the entire dataset. Among Wolbachia-infected individuals, all those carrying wVulC were associated with either haplotype V or its close relatives (XI and XII). All individuals carrying wVulM were associated with haplotype II and those carrying wVulP with haplotype VII. Of the 5 haplotypes found in Wolbachiainfected individuals, 4 were shared with individuals lacking both Wolbachia and the f element (II, V, VII and XII), 2 of which were also shared with individuals carrying the f element (II and V), and one (XI) was present in a single individual in the entire dataset.

Discussion

Our results provide direct evidence that the f element is overall more frequent than Wolbachia in the sampled A. vulgare populations. We detected the f element in 11 A. vulgare natural populations from 4 European countries (Czech Republic, France, Germany and The Netherlands) and Japan. Together with its previous detection in Denmark [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF], our results indicate that the f element has spread to a wide geographical range. The relative frequencies of the f element and Wolbachia are highly variable among populations and, in general, when one SRD is frequent, the other SRD is rare. Overall, these results are consistent with earlier results from the 1990's [START_REF] Juchault | EVOLUTION OF SEX DETERMINATION AND SEX-RATIO VARIABILITY IN WILD POPULATIONS OF ARMADILLIDIUM-VULGARE (LATR) (CRUSTACEA, ISOPODA) -A CASE-STUDY IN CONFLICT-RESOLUTION[END_REF], although no molecular assay allowing direct testing was available at that time and SRD presence or absence was inferred indirectly.

As the Jtel marker is located across the site of integration of the f element in the A. vulgare chromosome [START_REF] Sb | Birth of a W sex chromosome by horizontal transfer of Wolbachia bacterial symbiont genome[END_REF], f element presence in various populations can be explained by a single event of integration of a Wolbachia genome in the A. vulgare genome. A less parsimonious scenario would require independent insertions at the same chromosomal site, which is highly unlikely. The former scenario contradicts an earlier hypothesis on the evolutionary dynamics of the f element, which suggested that the f element was unstably integrated in the A. vulgare genome, experiencing frequent loss from oocytes and recurrent gain from Wolbachia endosymbionts [START_REF] Legrand | Nouvelles données sur le déterminisme génétique et épigénétique de la monogénie chez le crustacés isopodes terrestres Armadillidium vulgare Latr[END_REF][START_REF] Juchault | Transfer of a parasitic sex factor to the nuclear genome of the host: A hypothesis on the evolution of sex-determining mechanisms in the terrestrial isopod Armadillidium vulgare Latr[END_REF][START_REF] Juchault | Sex determination and monogeny in terrestrial isopods Armadillidium vulgare (Latreille, 1804) and Armadillidium nasatum bundde-lund, 1885[END_REF][START_REF] Juchault | Evolution of sex-determining mechanisms in a wild population of Armadillidium vulgare Latr. (Crustacea, Isopod) : competition between two feminizing parasitic sex factors[END_REF][START_REF] Rigaud | The spread of parasitic sex factors in populations of Armadillidium vulgare Latr. (Crustacea, Oniscidae): effects on sex ratio[END_REF]. Under this scenario, multiple independent f-like elements would be expected to segregate at low frequencies in populations, they should be integrated in different genomic locations and they should all be able to induce feminization [START_REF] Cordaux | Evolutionary Significance of Wolbachia-to-Animal Horizontal Gene Transfer: Female Sex Determination and the f Element in the Isopod Armadillidium vulgare[END_REF]. While our results do not formally invalidate the possibility of additional f-like integrations in A. vulgare populations, which the Jtel marker would not detect, it does not appear to be the most parsimonious hypothesis. Examination of sex ratios from progenies of wild-caught females lacking both SRD may offer further insight into this issue.

Using molecular assays allowed us to circumvent two limitations of the previously used physiological test: the impossibility to detect Wolbachia and the f element in males, and the impossibility to detect individuals carrying both SRD. Regarding Wolbachia presence in males, the historic protocol was only applicable to females per design [START_REF] Grandjean | Mitochondrial DNA polymorphism and feminizing sex factor dynamics in a natural population of Armadillidium vulgare (Crustacea, Isopoda)[END_REF][START_REF] Rigaud | Mitochondrial DNA polymorphism, sex ratio distorters and population genetics in the isopod Armadillidium vulgare[END_REF][START_REF] Juchault | EVOLUTION OF SEX DETERMINATION AND SEX-RATIO VARIABILITY IN WILD POPULATIONS OF ARMADILLIDIUM-VULGARE (LATR) (CRUSTACEA, ISOPODA) -A CASE-STUDY IN CONFLICT-RESOLUTION[END_REF] and subsequent PCR screens for Wolbachia infection have mostly focused on testing females [START_REF] Verne | Evidence for recombination between feminizing Wolbachia in the isopod genus Armadillidium[END_REF][START_REF] Rigaud | Mitochondrial DNA polymorphism, sex ratio distorters and population genetics in the isopod Armadillidium vulgare[END_REF][START_REF] Verne | Effects of parasitic sex-ratio distorters on host genetic structure in the Armadillidium vulgare-Wolbachia association[END_REF]. In fact, males have seldom been tested and found to carry Wolbachia [START_REF] Dittmer | Host origin and tissue microhabitat shaping the microbiota of the terrestrial isopod Armadillidium vulgare[END_REF]. Here, we detected Wolbachia in 7 males from 2 populations (Floirac and Saint Julien l'Ars), carrying either wVulC or wVulM strains. The failure of feminization by Wolbachia most certainly reflects insufficient bacterial titer to induce feminization (Figure S1). These field observations hence support the view that titer is an important factor for successful feminization, as low titer is linked to incomplete feminization and intersexual phenotypes [START_REF] Juchault | Sex determination and monogeny in terrestrial isopods Armadillidium vulgare (Latreille, 1804) and Armadillidium nasatum bundde-lund, 1885[END_REF][START_REF] Legrand | Rôle des bactéries symbiotiques dans l'intersexualité, la monogénie et la spéciation chez les crustacés oniscoïdes[END_REF].

We also detected the presence of the f element in 11 males from 4 populations. Historically, the presence of the f element in males has been indirectly inferred from crossings and the resulting sexratios biases of progenies [START_REF] Legrand | Nouvelles données sur le déterminisme génétique et épigénétique de la monogénie chez le crustacés isopodes terrestres Armadillidium vulgare Latr[END_REF][START_REF] Juchault | Evolution of sex-determining mechanisms in a wild population of Armadillidium vulgare Latr. (Crustacea, Isopod) : competition between two feminizing parasitic sex factors[END_REF][START_REF] Rigaud | Conflict between feminizing sex ratio distorters and an autosomal masculinizing gene in the terrestrial isopod Armadillidium vulgare Latr[END_REF]. Our results constitute the first direct evidence for the presence of the f element in A. vulgare males. In all 4 populations in which f-carrying males were found, the f element was also frequent in females. Altogether, these observations suggest that the 11 males carrying the f element also carry the masculinizing dominant M allele [START_REF] Cordaux | Evolutionary Significance of Wolbachia-to-Animal Horizontal Gene Transfer: Female Sex Determination and the f Element in the Isopod Armadillidium vulgare[END_REF][START_REF] Juchault | Evolution of sex-determining mechanisms in a wild population of Armadillidium vulgare Latr. (Crustacea, Isopod) : competition between two feminizing parasitic sex factors[END_REF][START_REF] Rigaud | Conflict between feminizing sex ratio distorters and an autosomal masculinizing gene in the terrestrial isopod Armadillidium vulgare Latr[END_REF]. Indeed, the M allele is able to restore a male phenotype in individuals carrying the f element [START_REF] Cordaux | Evolutionary Significance of Wolbachia-to-Animal Horizontal Gene Transfer: Female Sex Determination and the f Element in the Isopod Armadillidium vulgare[END_REF][START_REF] Juchault | Evolution of sex-determining mechanisms in a wild population of Armadillidium vulgare Latr. (Crustacea, Isopod) : competition between two feminizing parasitic sex factors[END_REF][START_REF] Rigaud | Conflict between feminizing sex ratio distorters and an autosomal masculinizing gene in the terrestrial isopod Armadillidium vulgare Latr[END_REF]. Because of sex ratio selection, the M allele is thought to have been selected to restore males in response to femalebiased sex ratios caused by the f element [START_REF] Rigaud | Conflict between feminizing sex ratio distorters and an autosomal masculinizing gene in the terrestrial isopod Armadillidium vulgare Latr[END_REF]. Thus, the M allele is expected to rise in frequency when the f element is frequent in a population [START_REF] Rigaud | Conflict between feminizing sex ratio distorters and an autosomal masculinizing gene in the terrestrial isopod Armadillidium vulgare Latr[END_REF], which is consistent with our observations. Unfortunately, no molecular marker of the M allele is currently available, which prevents any direct assessment of its actual presence in these populations. Thus, we cannot exclude that males carrying the f element simply carry non-feminizing variants of this SRD.

Our results show that Wolbachia and the f element never co-occur at high frequency in any population. This apparent mutual exclusion can be explained considering that co-occurrence of multiple feminizing factors in a population should favor the most transmitted one [START_REF] Cordaux | Evolutionary Significance of Wolbachia-to-Animal Horizontal Gene Transfer: Female Sex Determination and the f Element in the Isopod Armadillidium vulgare[END_REF][START_REF] Taylor | Evolutionary consequences of cytoplasmic sex ratio distorters[END_REF]. Hence, Wolbachia is expected to lead to the loss of nuclear feminizing elements in A. vulgare populations. This situation does not result from an interference between chromosomes and Wolbachia within individuals, but from counter selection of nuclear feminizing alleles in a population that becomes increasingly biased towards females. Hence, the rise of Wolbachia would associate with the decline of the f element in a population. Why, under these circumstances, Wolbachia has not invaded all A. vulgare populations is still unclear and may reflect fitness effects or possible resistance genes.

As a result, only very few individuals were found to carry both Wolbachia and the f element. They represent only 3 females, all from the Chizé population (Figure 1a). These were likely born from mothers carrying Wolbachia and fathers carrying the f element, which are frequent at Chizé. The apparent absence of carriers of both SRD in other populations where these SRD are present could simply be explained by the paucity of males carrying the f element.

Mapping SRD distribution onto mitochondrial genealogy showed excellent congruence between Wolbachia strains and mitochondrial haplotypes (wVulC-V, wVulM-II and wVulP-VII). Such strong association has previously been noted in A. vulgare-Wolbachia interactions at a smaller geographic scale [START_REF] Rigaud | Mitochondrial DNA polymorphism, sex ratio distorters and population genetics in the isopod Armadillidium vulgare[END_REF][START_REF] Verne | Effects of parasitic sex-ratio distorters on host genetic structure in the Armadillidium vulgare-Wolbachia association[END_REF] and, more generally, in many arthropod-Wolbachia interactions [START_REF] Galtier | Mitochondrial DNA as a marker of molecular diversity: a reappraisal[END_REF]. This result corroborates the rarity of non-maternal transmission of Wolbachia in A. vulgare. By contrast, the f element was found in 6 different mitochondrial backgrounds (I-VI) scattered across the mitochondrial phylogeny, indicating no particular association between the f element and mitochondria. This result confirms and extends earlier data focused on western France and in which f element presence in females was indirectly inferred based on sex ratios of their progenies [START_REF] Rigaud | Mitochondrial DNA polymorphism, sex ratio distorters and population genetics in the isopod Armadillidium vulgare[END_REF]. This observation can be explained by the occasional paternal transmission of the f element, which breaks its association with mitochondrial background [START_REF] Cordaux | Evolutionary Significance of Wolbachia-to-Animal Horizontal Gene Transfer: Female Sex Determination and the f Element in the Isopod Armadillidium vulgare[END_REF][START_REF] Legrand | Nouvelles données sur le déterminisme génétique et épigénétique de la monogénie chez le crustacés isopodes terrestres Armadillidium vulgare Latr[END_REF][START_REF] Rigaud | Mitochondrial DNA polymorphism, sex ratio distorters and population genetics in the isopod Armadillidium vulgare[END_REF].

Figure legends Figure 1 .

 legends1 Figure legends

Figure 2 .

 2 Figure 2. Haplotype network of 23 mitochondrial variants (I-XXIII) from 16 Armadillidium vulgare populations. Each circle represents one haplotype and circle diameter is proportional to the number of individuals carrying the haplotype. Branch lengths connecting circles are proportional to divergence between haplotypes. Sex ratio distorter frequencies are color-coded for each haplotype.

Table 1 . Prevalence of Wolbachia and f element sex ratio distorters in 16 populations of Armadillidium vulgare. 245Table 2 . Distribution of mitochondrial haplotypes in 642 Armadillidium vulgare individuals from 16 populations.

 12 II, III, V, VI, VII, VIII, IX, X, XII, XIII, XIV, XV, XVI, XVII, XVIII, XIX, XX, XXI, XXII, XXIII

		Number of	Haplotype
	Sex ratio distorter status	individuals	number	Haplotype list
	No f element, no Wolbachia I, f element only 404 21 128 6 I, II, III, IV, V, VI
	Wolbachia (wVulC strain) only	62	3	V, XI, XII
	Wolbachia (wVulM strain) only	20	1	II
	Wolbachia (wVulP strain) only	4	1	VII
	Wolbachia (undetermined strain) only 5	2	II, VII
	Both wVulM and f element	3	1	II
	Undetermined status	16	4	I, V, VI, XIX

Acknowledgments

We thank Drs. Nicolas Cerveau, Rémi Elliautout, Misel Jelic, Shigenori Karazawa, Giuseppe Montesanto and Eveline Verhulst for providing samples.

Funding statement

This work was funded by Agence Nationale de la Recherche Grants ANR-15-CE32-0006 (CytoSexDet) to RC and TR and ANR-20-CE02-0004 (SymChroSex) to JP, and intramural funds from the CNRS and the University of Poitiers.

Data accessibility

All data are provided in the electronic supplementary material.

A) B)

Figure 1