Faqing Yang

Jean-Pierre Jacquot

Scaling up with Event-B: A Case Study

HAL is

Introduction

This paper relates our experience with the specification of a realistic algorithm for the control of autonomous vehicles. The problem to solve has interesting characteristics:

the development should lead to a certified product (a component for a car moving in the public space), the physical and mathematical model uses common mathematical notions such as trigonometric, kinematics, integrals, and so on, there is an existing empirical solution.

The problem is known as platooning: autonomous vehicles that move as virtual trains. All vehicles follow the virtual track defined by the first vehicle while keeping to a minimum the distance between them. The issue is then to guarantee that the control algorithm is safe, i.e., that vehicles can never collide.

We chose Event-B because the concepts of proof obligation and formal refinement are well fitted for the task of guaranteeing an implementation. However, several points needed to be assessed. Could a non-functional property such as non-collision be specified in Event-B? Is the support environment, particularly the provers, strong enough for such a problem? Can we model adequately a system which contains continuous functions, real numbers, or geometric relationships, in a framework which is based on discrete sets and integers?

A first specification was written on a simplified version of the problem. The model considered only a linear track (1D) and the control was only aimed at keeping some ideal distance while avoiding collisions. While simplistic, this model was important on three respects: it allowed us to identified the "hard" parts, it prototyped the properties of interest, and it provided us with a neat structure for the development.

The next specification considered the platooning problem from a realistic point of view. Vehicles are now moving on a plane, the leader of the platoon is not constrained to a predefined track, the properties of interest are now the non-collision and the distance form the virtual track drawn by the leading vehicle.

The changes between a model in 1D to a model in 2D do not seem that big. Instead of one value, the control law must now compute two values: linear acceleration and derivative of the curvature. Furthermore, the system is assumed to stay within the boundaries which guarantee that the lateral and longitudinal controls can be modeled and computed independently.

However, working on a plane introduces notions such as trigonometric functions, curvature, and so on. While this means a modest increase in complexity for a mathematically literate person, those new concepts introduce genuine difficulties for the specifier; e.g, how to model a sine function when co-domains are restricted to integers?

The paper discusses some scaling-up issues when going from a 1D model to a 2D model. We could solve some, most importantly the consistency proofs and the adaptation of the mathematical model. Other issues can be solved but at a high cost, proving global temporal properties is among them. Last, some are yet beyond our reach because the tools cannot deal with the complexity; animation falls in this case for instance.

The paper is structured as follows: Section 2 introduces the notation and semantics for Event-B; Section 3 describes the platoon problem and the model used; Sections 4, 5, 6, 7 and 8 discuss the different aspects of scaling up with Event-B: mathematics, specification structure, temporal properties, tools and process; finally, Section 9 concludes.

Event-B Language

Event-B [START_REF] Metayer | The Event-B Mathematical Language[END_REF][START_REF] Abrial | Modeling in Event-B: System and Software Engineering[END_REF] is an evolution of the classic B method [START_REF] Abrial | The B Book[END_REF]. Designed for modeling the environment where a piece of software developed with the B-method must execute, Event-B proved to be a good formalism for specifying and reasoning about systems such as concurrent systems, reactive systems, or complex algorithms. Event-B is a state based specification technique. It embodies a process: formal refinement.

Formal Model. A formal model consists of a state and events. A state is a set of variables constrained by invariants. Values associated to variables are either symbols, integers, or set-theoretic constructions upon those (powersets, relations, functions, etc.). Invariants are expressed as formulae in first-order predicate calculus. Events are guarded generalized substitutions. Guards are formulae on the state and substitutions apply simultaneously on a subset of state's variables.

The semantics of a model is given by a few rules. Substitutions use the weakest precondition calculus of Dijkstra [START_REF] Dijkstra | A Discipline of Programming[END_REF]; events must keep the invariant; when several guards are true, the choice of the event to fire is non-deterministic; there must exist a computable initial state. The intuitive behavior of a specification is easy to explain: first, the INITIALISATION event is fired, then a cycle begins where: all guards are evaluated, one event is picked among those with a "true" guard, and its substitutions are executed. The cycle ends when no guard is true, which means either that the system has reached a terminal state, or that the system is deadlocked. Infinite cycles are also possible, which could be the correct behavior or indicate a reachability problem for a terminal state.

The formal semantic rules are implemented as proof obligations. To verify a model, that is, to assess its consistency, we need to discharge all the proof obligations.

Refinement. Event-B allows one to express that a model is a refinement of another, more abstract model. Refinement consists in introducing new variables. An abstraction invariant relates the new variables to the abstract variables. Events from the abstract model can be kept untouched in the refinement, or can be rewritten using the new variables. New events can be introduced too. In practice, it is often useful to think in term of reification of variables and of decomposition of an event into several smaller ones.

The semantics of refinement is given by proof obligations. Proving a refinement correct amounts to prove that concrete events maintain the invariant of the abstract model, the abstraction invariant, and do not prevent abstract events to be triggered.

The syntactic structure of the language was designed so that the proof obligations can be easily generated and broken into small formulae. The Rodin platform [START_REF]RODIN: Rigorous Open Development Environment for Complex Systems[END_REF] provides the practical framework to carry out modeling in Event-B. It seamlessly integrates modeling and proving, and provides mechanisms for extension and configuration so that it can be tailored to different application domains or development methods.

3 The Platooning Problem

Platoons

Research on urban mobility systems based on fleets of small electric vehicles stresses the importance of a new moving mode: platooning. A platoon is defined as a convoy of autonomous vehicles which follow exactly the same path and which are spaced at very close distance one from the other.

In this work, we consider platoons formed by a leader vehicle and followers. Leaders and followers have different control laws. We specify only the follower control law. Its aim is to keep as close as possible to the preceding vehicle while following a virtual ideal track without colliding. We use a model of vehicle where the control can be decomposed into longitudinal (distance with preceding vehicle) and lateral laws. We assume operating conditions such that the two controls can be set independently [START_REF] Daviet | Longitudinal and Lateral Servoing of Vehicles in a Platoon[END_REF].

There are numerous strategies to form and maintain platoons, characterized by their degree of centralization and the volume of communication. We specify a minimal strategy: no central control and no communication between vehicles other than perception, i.e., a vehicle can sense a few information from the preceding vehicle (distance, speed, etc.). The virtual track is set by the leader. The control is local to each vehicle, based on current state and perceptions. This strategy may not be the most efficient but it is very robust. In particular, it can be used as a fall-back in case of failure in a system using more sophisticated algorithms. Hence the need to guarantee its correctness.

Within this problem setting, platoons can be considered as situated multi-agent systems (MAS) which evolve following the Influence/Reaction model [START_REF] Ferber | Influences and Reaction : a Model of Situated Multiagent Systems[END_REF][START_REF] Ferber | Multi-Agent Systems: An Introduction to Distributed Artificial Intelligence[END_REF]. Development of the specification follows a stepwise refinement process based on this model: (i) driving systems perceive, (ii) decisions are taken, and (iii) physical vehicles move.

Research Goal and System Hypotheses

We aim at modeling formally a pragmatic strategy known as Daviet-Parent algorithm [START_REF] Daviet | Longitudinal and Lateral Servoing of Vehicles in a Platoon[END_REF] in order to prove that implementations enjoy certain properties [START_REF] Lanoix | Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles[END_REF] such as: (i) the model is sound bound-wise, (ii) no collision occurs between the vehicles, (iii) no unhooking occurs, and (iv) no oscillation occurs.

Presently, we focus on two essential safety properties: no collision within a platoon occurs 1 and the soundness is maintained.

Our model is based on the following system hypotheses: we consider a set of N(≥ 2) vehicles forming a linear platoon, motion of vehicles is limited by fixed bounds on velocity, acceleration, curvature and derivative of curvature, we consider forward-only motions on a non self-intersecting track, we suppose that the frequency of the control algorithm is the same for all vehicles, so they can be modeled as synchronized, sensors are perfect and their accuracy is such that the velocity of the previous vehicle can be precisely known, actuators of the engine are perfect.

The hypotheses are strong but not that far from reality considering (1) we are not modeling fault, fault-tolerance, or such matters, (2) near perfect abstract sensors or actuators can be built from merging results of several concrete ones.

State of Vehicles

In the 1D model, vehicles move on a linear track, equivalent to a rail. The state of the i th vehicle at time t is the pair (xpos i (t), speed i (t)), where xpos i represents position on the track and speed i represents the velocity. Control consists in setting of an acceleration to modulate speed. The behavior law is represented by (1) extracted from [START_REF] Simonin | Generic Expression in B of the Influence/Reaction Model: Specifying and Verifying Situated Multi-Agent Systems[END_REF], where MaxSpeed is the maximum velocity, accel i is the acceleration, and ∆t is the time increment:

                           n_speed = speed i (t) + accel i (t).∆t xpos i (t + ∆t) =            xpos i (t) + MaxSpeed.∆t if n_speed > MaxSpeed xpos i (t) -speed i (t) 2 2.accel i (t) if n_speed < 0 xpos i (t) + speed i (t).∆t + accel i (t).∆t 2 2 otherwise speed i (t + ∆t) =    MaxSpeed if n_speed > MaxSpeed 0 if n_speed < 0 n_speed otherwise . (1)
The acceleration accel i is chosen according to the current state of the i th vehicle and the values sensed on the preceding vehicle.

In the 2D model, vehicles move on a plane. The vehicle state η must model its position, represented by cartesian coordinates (x, y), and its attitude, represented by the orientation θ of vehicle's axis with respect to x-axis. The behavior law now contains a velocity v and a trajectory's curvature κ which are controlled by application of a linear acceleration a and a derivative of the curvature χ. When a control (a, χ) is applied to a state (x 0 , y 0 , θ 0 , v 0 , κ 0 ) at time t for a period ∆t, the new state at time t + ∆t becomes:

           x = x 0 + cos θ 0 F C (∆t, v 0 , κ 0 , a, χ) -sin θ 0 F S (∆t, v 0 , κ 0 , a, χ) y = y 0 + cos θ 0 F S (∆t, v 0 , κ 0 , a, χ) -sin θ 0 F C (∆t, v 0 , κ 0 , a, χ) θ = θ 0 + v 0 κ 0 ∆t + (aκ 0 + v 0 χ) ∆t 2 2 + aχ ∆t 3 3 v = v 0 + a∆t κ = κ 0 + χ∆t (2)
where

F C (∆t, v 0 , κ 0 , a, χ) = ∆t 0 (v 0 + at) cos(v 0 κ 0 t + (aκ 0 + v 0 χ)t 2 /2 + aχt 3 /3)dt and F S (∆t, v 0 , κ 0 , a, χ) = ∆t 0 (v 0 + at) sin(v 0 κ 0 t + (aκ 0 + v 0 χ)t 2 /2 + aχt 3 /3)dt .
At this mathematical level, the increase in complexity is noticeable but not dramatic: most of it boils down to the expansion of standard geometric formulae.

4 Scaling up with Event-B: Mathematics

1D Model Adaptation

The formulae in the 1D model are basic arithmetic expressions; they contain no special mathematical functions. The values of xpos i , speed i and accel i can easily be modeled as integer numbers. It suffices to choose a system of units small enough to reach the accuracy needed in practice. Hence, they can be expressed straight away in Event-B.

2D Model Adaptation

By contrast, a simple look at the 2D model shows that we need to transform the model so it can be expressed in Event-B. The most obvious "problems" are the sine and cosine functions (meaningless on Integers) and the integral in F C and F S expressions.

The Discretization Issue. The heart of the difficulty lies in the discretization of continuous kinematic values such as position, speed or acceleration. The question is then: Why not use continuous values? We are not ready to answer positively for two reasons.

First reason is practical. Current provers within the B world consider only integer numbers. Even with these "simple" numbers, proofs are often complex and intricate. It is not clear that provers doing a good job with real numbers will be available soon.

Second reason is deeper. Software systems are inherently discrete. Because of numerous latencies in the autonomous car (sensing data, computing controls, driving actuators), the control system will operate at a rather slow frequency. So, the actual system will run as if time is discrete.

The B formal method aims at producing code which is proven to maintain functional invariants. So, we need to introduce the discretization at some point. Our position is that we must introduce this fundamental feature early in the models: as soon as we need "continuous" values in the specification. Of course, we must then develop techniques and strategies to take care of this feature.

Although reasonably simple from a mathematician point of view, the 2D model cannot be translated directly in Event-B. We need to "refine" it. We used three heuristics.

(1) Free Physical Units. In Event-B, the easiest representation of continuous kinematic values such as position, velocity, acceleration is integer numbers. By keeping the physical units unspecified but homogeneous (e.g., the unit of velocity is equal to unit of distance divided by unit of time.), we can adapt the representation to the desired accuracy of the computations. Distances can be millimeters as well as meters, and times can be milliseconds as well as seconds.

(2) Approximate Mathematical Functions. The restriction to Integers of the ranges of sine or cosine is a three value set: not very interesting. To solve this problem, we introduce a special dimensionless constant µ and we consider µ cos θ and µ sin θ instead of cos θ and sin θ. We do the same with F C and F S and consider µF C and µF S . By choosing a µ with a big value, expressions can be reasonably coded with integers.

Event-B provers know about standard rules of arithmetic but ignore trigonometric or general calculus rules. In order to use the provers, we use Taylor series and identities to transform expressions into arithmetic approximations.

Last, the vehicle state η = (x, y, θ, v, κ) is represented by a 6-tuple (x, y, γ θ , σ θ , v, κ). The values of x, y, v and κ are integers; the units must be taken small enough to obtain a good accuracy. The values of γ θ and σ θ are also integers which respectively represent µ cos θ and µ sin θ. We define a carrier set POINT to denote the set of all possible vehicle states. The approximate, but accurate, model of 2D platooning is then:

               x = x 0 + (γ θ 0 FC (∆t, v 0 , κ 0 , a, χ) -σ θ 0 FS (∆t, v 0 , κ 0 , a, χ))/µ 2 y = y 0 + (γ θ 0 FS (∆t, v 0 , κ 0 , a, χ) + σ θ 0 FC (∆t, v 0 , κ 0 , a, χ))/µ 2 γ θ = (µ C γ θ 0 -µ S σ θ 0 )/µ σ θ = (µ C σ θ 0 -µ S γ θ 0 )/µ v = v 0 + a∆t κ = κ 0 + χ∆t (3)
where

µ C = µ -β 2 /(2µ), µ S = β -β 3 /(6µ 2 ) with β = v 0 κ 0 ∆t + (aκ 0 + v 0 χ)∆t 2 /2 + aχ∆t 3 /3, FC (∆t, v 0 ,
κ 0 , a, χ) and FS (∆t, v 0 , κ 0 , a, χ) expanded as Taylor series.

Event-B translation is straightforward but yields overly long expressions.

( equality is not true anymore (hint: ÷ denotes the integer quotient). So any proof which relies on the equality cannot be discharged anymore.

In the initial 1D platooning model, we found two reviewed goals that were instances of the above example. The "obvious" formula below, straight translation of the 1D mathematical model, introduces non provable proof obligations. We proved the model by avoiding the problem with the equivalent expression: An important question when we started the 2D modeling was: can we keep the same development structure as for 1D modeling? We had two reasons. First, a great deal of effort had been put into it so it is intelligible, consistent with the general MAS model, then easy to validate. Second, we can expect proofs structures (and even whole proofs) too to be similar if developments are similar.

We have been able to keep the exact same structure of the development. The same refinements with the same rationales are present in both specifications. In fact, we used the development of 1D specification as a "road-map" for development of the new model.

The structure of the specification [START_REF] Lanoix | Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles[END_REF] consists of an abstract machine Platoon and four refinements. Each development introduces a clearly identified concept. Platoon sets the "vocabulary" and the safety property of interest. Platoon_1 splits the platoon's movement into each vehicles' movements. Platoon_2 implements the physical reaction laws. Platoon_3 introduces the decision step. Platoon_4 introduces the perception step and implements the decision laws.

Decomposition of Events

During the refinement, the number of events increased much more steeply. A simple pattern explains this explosion.

Both specifications implement the reaction laws in machine Platoon_2 and the decision laws in machine Platoon_4. We need to decompose the abstract events move1 and move in machine Platoon_1, and the abstract events decide1 and decide in machine Platoon_3 into more concrete ones. Let us consider the decomposition of event move.

The mathematical model (1) in 1D indicates that three cases must be considered when computing a new state. This is due to the fact that speed is bounded. In Event-B, conditional definitions are expressed by the use of guards. This means that the move event must be decomposed into three events, one for each situation (speed reaching lower bound, reaching upper bound, or within bounds.)

All events where speed is a parameter are decomposed following the analysis exemplified in Table 1. In the 2D model, we have to consider two bounded parameters: speed and curvature.

n_speed i = speed i + accel i .∆t n_κ i = κ i + χ i .∆t . ( 4
)
The analysis must then take into account the combination of three cases for n_speed i and three cases for n_κ i . So, events are refined into nine following the pattern of Table 2.

Table 2. Decomposition of move event in the 2D model

n_speed i \ n_κ i < -MAX_κ ∈ -MAX_κ..MAX_κ > MAX_κ < 0 move_vmin_κmin move_vmin_κ move_vmin_κmax ∈ 0..MAX_SPEED move_v_κmin move_v_κ move_v_κmax > MAX_SPEED move_vmax_κmin move_vmax_κ move_vmax_κmax

Statistics of the Specifications

The multiplication of events depicted above happened a few times. It should be noted that other refinement strategies for the abstract event move could have been chosen. For instance, we could have kept the refined event unique, but at the expense of very complex guards. Our trade-off lengthens the specification text and increases the number of proof obligations but each proof is much simpler. Table 3 shows the increase in complexity when passing from the 1D initial model, to the 1D revised model using the technique presented in Sect. 4.2 and augmented with deadlock-freeness, to the 2D model.

Introducing a safety property such as deadlock-freeness has little impact on complexity. While the number of variables roughly doubled when going 2D, all other measures varied by a four-fold increase. Interestingly, the ratio between manually and automatically discharged proof obligations increases just a little: most of the new proof obligations are simple ones. The most important increase is the number of theorems. They are used to ease the proofs by introducing only once standard mathematical properties. This is a consequence of the introduction of more complex arithmetic expressions in the 2D model. 6 Scaling up with Event-B: Temporal Properties

Temporal properties can be classified into two categories. Safety properties specify that nothing bad will happen. Liveness properties specify that something good will eventually happen [START_REF] Lamport | Proving the Correctness of Multiprocess Programs[END_REF]. Our model must guarantee a safety property: deadlock-freeness. This safety property was introduced after a long period of perplexity where we were baffled by observing collisions in our programmed simulations of the exact same model that was verified, i.e., where we had proven that firing any event kept a strictly positive distance between vehicles as invariant [START_REF] Lanoix | Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles[END_REF]. The mystery was lifted when we realized that if a moving vehicle cannot react, i.e., its control system is deadlocked, then it will likely collide with something.

Deadlock-freeness is not well integrated into the Event-B framework. As for many other temporal properties, we can use "tricks". For deadlock-freeness, we build the disjunction of the guards of all events other than INITIALISATION and we prove it is a theorem. So, we can be sure that one event at least can always be fired.

The trick works well on small models but does not scale up. In the 1D specification, the deadlock-freeness theorem in machine Platoon_2 is a formula with around 42 lines (7 events times 6 lines per guard). It would be around 390 lines long in the last refinement of the 2D specification (39 events times 10 lines per guard). Two problems arise then. One concerns the management of a proof of a disjunction of 39 cases. Rodin proof explorer is well thought out and we are quite confident that, with time and patience, we could discharge the proof. The second concerns the construction of the formula. Right now, we must rely on a manual cut and paste procedure. Needless to say, the probability of introducing a non obviously detectable error is too high for the result to be trusted. Clearly, we need a tool to build automatically this formula.

Scaling up with Event-B: Tools

Formal methods depend heavily on automated support. They require long, intricate, and generally tedious chains of reasoning to discharge or establish properties, even trivial ones. This is the nature of formal proof systems. Effective tools are not a "nice addition" to a formal method, but a key factor for its deployment. Event-B is supported by Rodin, a framework which integrates gracefully tools to edit, verify and validate models.

Edition and Verification

The increase in size shown in Table 3 did not pose any problems to Rodin editors, either the native structural editor or pluggable text-editors such as Camille [START_REF] Bendisposto | Developing Camille, a Text Editor for Rodin[END_REF]. Likewise, visualization tools such as the LaTeX generator or the pretty-printer were up to the task.

Provers were also able to deal with the increase in complexity. In fact, the general strategy of breaking a verification proof into several smaller proof obligations as used by B spreads the increase in complexity on much more proof obligations, but each one remains reasonably simple. Some proofs were more complex because the model uses more complex formulae, not because it is bigger.

Animation Plug-in for Validation

Animation is a technique to execute specifications. Thus, we can play, experiment and observe the behavior of models. Several tools support the technique [START_REF] Bendisposto | La validation de modèles Event-B avec le plug-in ProB pour RODIN[END_REF][START_REF] Leuschel | Animation and Model Checking of CSP and B using Prolog Technology[END_REF][START_REF] Van | Goal-Oriented Requirements Animation[END_REF][START_REF] Schmid | A Survey of Simulation Tools for Requirements Engineering[END_REF][START_REF] Siddiqi | Towards quality requirements via animated formal specifications[END_REF]. The principle of animating an Event-B specification is a simple three-step process:

1. the user gives values to the constants and carrier sets in the contexts, 2. the INITIALISATION event is fired to set the system in its initial state, 3. the animator enters a loop:

(a) compute the guard of all events, enable those for which the guard is true. When events are parameterized, pick one value, if any, which makes the guard true, (b) the specifier fires one of the enabled event; the substitutions are computed, (c) check if the invariants still hold [optional].

The computation of the invariant is superfluous when the animated specification has been fully proven. However, it is a very valuable feature when animation is used on unproven specifications, in particular to check potential candidate for invariant formulae.

It may sound strange to use anecdotal observations in a context where mathematical proofs are pivotal to the method. However, we firmly believe that such semi-formal activities are useful, and even sometimes necessary, for three reasons.

The first reason relates to the notion of validation. Proofs show that a particular text is logically consistent and that the last model in a sequence of refinements is a correct concretization of the initial model. However, proofs do not tell if a model is an adequate description of the desired behavior of the system. Animation exhibits behavior.

The second reason concerns temporal properties. Not all properties can be expressed in Event-B. Animation can then be used to "test" the specification for certain properties.

We can set up scenarios and look if the system goes only through safe states. Like tests, animation does not prove correctness but shows errors.

The last reason is that animation is a good, practical, tool to get deep insights on complex specifications. Actually, animation was mainly invented for this reason [START_REF] Balzer | Operational specification as the basis for rapid prototyping[END_REF].

We used intensively animation to understand the collision problem in the 1D platooning specification. In particular, animation helped us to understand which values lead to deadlocks. From those, we could abstract to general configurations, and then relate to parts of the deadlock-freeness theorem.

We also found out, in another work [START_REF] Mashkoor | B événementiel pour la modélisation du domaine: application au transport[END_REF], that animation could be a reasonably cheap way to get a correct refinement of an abstract fact into a complex behavior. Animation helped to define the guards and the explicit coding of causal order required by Event-B.

Breaking Animators

The positive experience with 1D induced us to use animation early in the 2D model development. Unfortunately, animators failed us even on the first refinement.

We tried with two different animators, Brama2 and ProB [START_REF] Leuschel | ProB: An Automated Analysis Toolset for the B Method[END_REF]. In both cases, the notion of POINT (3) was the first visible obstruction. We needed to code it, either crudely as integers with Brama or more abstractedly as symbols with ProB. Either way, a list should be provided by hand. This is not realistic and even meaningful.

One way to get rid of POINTs is to refine them as their coordinates. Each coordinate is an integer function which could be individually managed but six of them create too complex a space. Brama seems to enumerate values, ProB uses more sophisticated constraint solving techniques; both strategies fail on the 6-dimensions space.

This can be explained by two important features of Event-B: non-determinism and definition of values by their properties. Animators are then more oriented toward "picking" values rather than "computing" values. This orientation is fine most of the time, but it should not be exclusive. Sometimes, even in abstract specifications, we know some expressions are deterministic computations: kinematic functions are a good example. In those cases, we would appreciate to be able to tell this to the animator.

In the transformations we developed to make specifications "animatable" [START_REF] Mashkoor | Transformation Heuristics for Formal Requirements Validation by Animation[END_REF], we have some ad-hoc heuristics which force a computation. Their major drawback is to make the text of the guards and the substitutions much more complex. While in principle they are applicable, we have not yet tried them in the 2D specification. We lack the automated editors required by the number of expressions to transform.

Scaling up with Event-B: Process

Like for any complex artifact, we need a precise and definite process to build good formal specifications. A good formal specification should have the following properties: (a) it is logically consistent, (b) it has proven functional properties, (c) it meets nonfunctional properties, and (d) it is a reasonable model of the problem.

Formal refinement is the keystone around which the B-method is designed. Its embodiment into the language and the support tools allows one to develop pieces of software where an implementation is proven against its specification. Refinements break down the verification process into discharging many, but small, proof obligations. So issues (a) and (b) are well taken care of. Event-B uses the same strategy. Here, models are complexified while retaining the same functional properties.

To deal with the issues (c) and (d), i.e., the validation of the specification, we have defined an extended refinement process depicted in Fig. 1.

The idea is to associate validation activities to formal refinement steps. A development step is then composed of four activities:

1. refinement of the physical/mathematical model. The mathematical expressions are refined so that they can be translated into Event-B and lead to provable properties.

Discretization is studied at this stage. 2. formal refinement of the Event-B specification with all proof obligations discharged. 3. animation of the specification. The specification is transformed in order to be animatable [START_REF] Mashkoor | Transformation Heuristics for Formal Requirements Validation by Animation[END_REF], scenarios are elaborated, and behavior is observed with the animator. 4. analysis and refinement of temporal properties. This activity leads to the introduction of variants and theorems for temporal properties and their proof.

The order of the activities is important. A mis-adapted physical model may lead to non provable, although correct, formulae. There is no point to validate an unproven specification as it may be inconsistent. Animation can help get better insights on the temporal constraints which need to be formalized.

The process was successfully tested with the 1D model. Actually, it was through replaying the construction of the 1D model with the full process that we were able to identify the flaws in the initial model and to produce a revised, correct, version. As can be inferred from the above discussion on tools, we could not fully validate the 2D specification due to the lack of automated tool support. However, the process helped us the ask the pertinent questions when validating through "walkthrough" of the specification. Furthermore, it gave us ideas on improvements of the environment.

Conclusion and Future Works

Our experience with a real-world model is both reassuring and worrying. This is consistent with our findings on using Event-B for the modeling of transportation domain [START_REF] Mashkoor | Domain Engineering with Event-B: Some Lessons We Learned[END_REF]. On the very positive side: we could model a reasonably complex algorithm and prove its correctness. Daviet-Parent algorithmis a good representative of a class of problems of great practical importance: problems for which we have empirical solutions, prototype implementation, and a strong need to certify it before we can use it in practice.

Event-B is a good candidate for formal modeling and development of real systems. First, the language has sufficient power to express complex mathematical models and algorithms. Second, the formalism embodies a sound, effective, and easy to use refinement based process. Last, the tool support for edition and verification is up to the task. Of course, stronger provers or syntactic sugar-coating to help navigate long texts would be welcome improvements but are not mandatory to make the method usable.

)

  Check and Rewrite Mathematical Formulae for Provability. Many properties of formulae on real numbers can be safely assumed when we restrict their use to integer numbers, but not all. Consider the true equality with real numbers: a * (b/c) = (a * b)/c. Its equivalent with natural numbers is a * (b ÷ c) = (a * b) ÷ c. Unfortunately, this

  xpos0+MAX_SPEED-(((MAX_SPEED-speed0) * (MAX_SPEED-speed0))/(2 * accel0))

  xpos0 + ((MAX_SPEED-speed0) * (MAX_SPEED-speed0))/(2 * accel0) + speed0 * ((MAX_SPEED-speed0)/accel0) + MAX_SPEED * (1-(MAX_SPEED-speed0)/accel0) 5 Scaling up with Event-B: Specification Structure

Fig. 1 .

 1 Fig. 1. A step of development process

Table 1 .

 1 Decomposition of move event in the 1D model

	n_speed i	< 0	∈ 0..MAX_SPEED	> MAX_SPEED
	move	move_reduce	move_normal	move_max

Table 3 .

 3 Statistics of the specifications

		1D initial model 1D revised model 2D model
	Sets	0	0	1
	Constants	15	15	50
	Axioms	27	27	86
	Variables (last refinement)	10	10	16
	Invariants	16	17	29
	Events (last refinement)	15	15	39
	Guards (last refinement)	81	81	354
	Theorems	1	4	46
	Variants	3	3	3
	Automatic POs	187	196	743
	Manual POs	29	36	177
	Reviewed POs	4	1	0
	Undischarged POs	0	0	0
	Total POs	220	233	920

Collisions between platoons or between a vehicle and an obstacle should of course be considered in a real system. First kind should be taken care by the control law of leaders, second kind is dealt with by lower level emergency systems. Both are outside the scope of this work.

http://www.brama.fr

Acknowledgments We are indebted to our colleagues from MAIA and TRIO groups at LORIA with special thanks to A. Scheuer for his development of the 2D model.

Work partially supported by ANR under project ANR-06-SETI-017 TACOS (http://tacos.loria.fr), and by Pôle de Compétitivité Alsace/Franche-Comté under CRISTAL project (http://www.projet-cristal.net).

A second reason to be optimistic was our ability to deal with a physical and mathematical model which incorporates complex functions and continuous time. This has required some sweat and efforts, but was never a blocking factor. We think that there are a few "conditioning techniques" that can be used at the mathematical level to put continuous model in a form suitable to Event-B. We have identified some of them.

Whether Event-B should support continuous functions or real numbers is an interesting question. The answer may not be clear-cut. In our system, real numbers would have eased the writing and maybe some consistency proofs. However, they would not help much improving an implementation because actual vehicles will operate on a discrete time. The control software of actual prototype vehicles operates around 20 Hz. That makes for quite a discrete time.

The worrying issue lies with the checking of temporal properties, either formally through proofs, or pragmatically through animation.

On the formal side, the current situation is not adequate. Only "coarse" properties can be expressed and even then, awkwardly. This is clearly an area where research is needed. A way to overcome this limitation is to associate B or Event-B with another formalism which supports temporal modelling. CSP||B proposed in [START_REF] Schneider | Communicating B Machines[END_REF][START_REF] Treharne | Combining Control Executives and Software Specifications[END_REF] is a candidate. Experiments [START_REF] Colin | Using CSP B Components: Application to a Platoon of Vehicles[END_REF][START_REF] Nguyen | A Tool for Checking CSP||B Specifications[END_REF] conducted on the specification of the platoon problem indicate a good potential. However, two big issues are still opened: the automation of the proof of consistency between CSP and B parts, and the refinement divergence between CSP and B. Whether CSP||B will scale up soon to realistic models is not yet clear.

On the pragmatic side, we need better animators. Such tools have a very important property: they act on the specification itself. We can be confident that observing animations is observing the model's behavior. It is not clear that the failures to use animators that we have identified can be overcome soon. We are currently working on the idea of translating the specification into an executable language like C or MATLAB. Such translators could be used as a "fall-back" when standard animation fails. They will not exhibit the real model's behavior but a reasonably close version.


Vincent Chalvet

Artur Zarzycki

Yassine Haddab

Member, IEEE Philippe Lutz

Digital Microrobotics Based on Bistable Modules : Design of a non-redundant digital micropositioning robot

High precision manipulation becomes a recurrent need in micro or nanoscale. Microrobots based on active material were designed to perform micromanipulation tasks in various environments such as microrobotic stations or electronic microscopes (SEM, TEM). These active materials are used to generate proportional actuation, but show some drawbacks we want to avoid (non linearity, integration of sensors, . . . ). In this paper we propose a new type of microrobot, called digital microrobot. It is based on the use of bistable modules (Fig. 1), and generates a discrete workspace. This microrobot can be used in open-loop mode and gets rid of bulky and expensive instruments and sensor integration. Moreover, no external energy is required to maintain the microrobot in a given position. The study presented in this paper is dedicated to the design of the robotic structure in order to generate a desired workspace.

I. INTRODUCTION

With the fast development of microtechnologies during the last decades, several microrobots have been developed to interact with the MEMS (Micro Electro Mechanical Systems), and other micro-objects. Increasing accuracy and repeatability of these positioning systems was therefore formulated in the domain of microrobotics, in order to handle various tasks in the microworld. In particular for the manipulation of the micro-objects (whether artificial ones or biological ones), for the positioning and the characterization of these objects, or even for the micro-assembly of MEMS. These studies focus on two main points : design of grippers (hand effectors) to handle micro-objects, and design of the carrying microrobots (carrier) for the positioning of the gripper. Although studies of micro-grippers design have expanded widely, the studies concerning carriers was limited. Micro-grippers are becoming very powerful. They include several kinds of sensors ([1] [START_REF] Kim | Nanonewton force-controlled manipulation of biological cells using a monolithic MEMS microgripper with two-axis force feedback[END_REF]) in order to manipulate objects with more safety, or to improve the releasing process ( [START_REF] Chen | Overcoming adhesion forces: active release of micro objects in micromanipulation[END_REF]). Current carriers created to manipulate very small objects, are often designed as the miniaturization of robots used in the mesoscale. This is why they face the same problems as traditional actuators such as friction, wear, backlash or lubrication. Several studies have nevertheless been done for the development of carriers.

Microrobotic community have adopted the active materials in order to actuate the micropositioning systems. These materials show much better capabilities in the microworld than the traditional actuators massively used in mesoscale robotics and manipulation tasks. Active materials actually present very high resolutions and are therefore mostly used Authors are with FEMTO-ST Institute, UMR CNRS 6174 -UFC / ENSMM / UTBM, Automatic and MicroMechatronic Systems Department, 14, rue Alain Savary, 25000 BESANC ¸ON, France. E-mail : {vincent.chalvet;artur.zarzycki;yassine.haddab;philippe.lutz}@femto-st.fr for actuation and sensing. However, these active materials present some drawbacks which may be difficult to handle during the control process of the system. The behavior of such materials is very complex, presenting non linearity and sometimes non stationarity. These drawbacks make the modeling and thus the control of such actuators very difficult. Moreover, the sensors needed for the control are generally difficult to integrate, bulky and expensive instruments for signal processing and real-time operating.

A. Binary Actuation

We propose a new concept of microrobot in order to overcome all these problems. This robot is based on discretelyactuated modules. An analogy can be made between continuous vs. binary manipulators and analog vs. digital circuits. In electronics, digital devices replaced many of their analog counterparts because of higher reliability and lower cost. Similar reasons motivates the conception of digital robots.

Discrete actuators have already been developed for a long time with the stepper motors. The control of these actuators became easier, but it also generated drawbacks already encountered with traditional actuators such as friction. That is why the use of control feedback is necessary. In order to generate a discrete workspace, we will use binary actuators that can be used in open-loop.

In the mesoscale, several binary-actuated robots have already been developed and showed very good performances compared to the commonly used continuous range of motion robots and positioners. The most known one is the variable geometry truss (VGT) manipulator which is a macroscopically serial manipulator composed of binary actuators. It was highly studied by Chirikjian since 1994 with his binary paradigm for robotic manipulators in [START_REF] Chirikjian | A Binary Paradigm for Robotic Manipulators[END_REF]. This planar binary VGT manipulator consists of several cascaded modules. Each of them is composed of three binary actuators, resulting in eight discrete states (2 3 ). By adding modules on top of each other, the end effector of the manipulator can reach a very high number of discrete positions, revealing a highly-redundant workspace. An other well-known binary manipulator uses the same concept of three binary actuators by modules. It is the Binary Robotic Articulated Intelligent Device (BRAID) [START_REF] Sujan | Lightweight Hyperredundant Binary Elements for Planetary Exploration Robots[END_REF]. This is also a VGT manipulator like the previous one, but it can create a three dimensional workspace, and is aimed to be used in aerospace robotics.

In the microscale, several binary actuators have also been developed. They were mainly used as digital-to-analog converters ([8][9]), and showed very good accuracy and stability. They can be used as small linear micropositioners. For example, by including them inside MEMS, we become able to position several of the MEMS components such as micromirrors. Other binary micro-actuators were also used as electric relays in MEMS ( [START_REF] Qiu | A High-Current Electrothermal Bistable MEMS Relay[END_REF]).

B. Bistable Module

To obtain a digital microrobot, our first work was to design the elementary module which can constitute the whole digital microrobot. This module is not a simple binary module, but a bistable module. Most of binary modules have two stable positions, but not two robust ones. Only one of the two positions generated is robust thanks to the use of stoppers.

Unlike these modules, bistable modules have two stable, robust and repeatable states. They furthermore do not need power supply while staying in one of the two positions used. The energy supply is only needed for switching states. This property of bistability induces very low power consumption, and enables the open-loop control of the system. The bistable module developed in [START_REF] Chen | Digital Microrobotics Based on Bistable Modules : Design of Compliant Bistable Structures[END_REF] was furthermore improved compared to other bistable micro-actuators such as the one in [START_REF] Qiu | A High-Current Electrothermal Bistable MEMS Relay[END_REF], in order to improve its stability and strength.

Let us see how this bistable module works. It is a monolithic structures, of 2 × 9 mm 2 in dimensions, and composed of three different elements (see Fig. 1) :

• one bistable structure • two stop blocks • two pairs of thermal actuators The thermal actuators push forth and back the bistable structure whose displacement is limited by the stop blocks. These stop blocks furthermore induce a blocking force, guaranteeing the robustness of the two positions generated.

II. GLOBAL DESIGN OF THE ROBOTIC STRUCTURE

A. Fabrication Constraints

The objective is to create a monolithic microfabricated microrobot based on the use of bistable modules described previously. The bistable modules from which we will start building the microrobot have a very small thickness compared to its other dimensions. It is a 9 mm width and 2 mm height module with a maximum thickness of 500 µm. The microrobot will show a very thin architecture, resulting in a fragile structure. Even if this small thickness can be seen as a drawback, it is also one of the positive points of this architecture. Small thickness actually enables the robot to work in confined environments like microrobotic stations or Transmission Electronic Microscopes (TEM). In order to control the fragility of the structure, the stress generated inside the structure has to be check. It should not exceed the breakpoint (limit of the stress) of the material used. This stress has to be checked for the normal use of the robot (activation of modules) as well as for the manual handling of the structure (for instance while microfabricating it). The stress threshold we consider here is 1 GP a for silicon.

Some constraints are directly linked to the bistable modules' properties. The first one concerns the dimensions of the module which are quite large compared to the generated displacement. The robotic structure has to be sufficiently large to include the modules, but can furthermore generate very small displacements. The second one is the force to which the module can resist. This bistable module was actually designed with the objective to be used in a robust robotic structure. Each module can undergo a force of 1.54 mN before showing significant values of unwanted displacement. With the aim of maintaining the good behavior of the microrobot, the force applied onto the bistable modules should not exceed that blockage force.

The last constraints concern the kind of workspace we want the microrobot generates. The generated workspace, presents 2 n positions (n is the number of modules used in the microrobot). As this robot is designed to work in the microscale, the workspace will have a submicrometer resolution. The first robotic architecture we are going to build will generate a two dimensional displacement, that is why we consider a square workspace without any redundancy. Redundancy is indeed a prevalent property of digital robots. It is the cause of many difficulties for the trajectory planning and forward or inverse kinematics calculation.

B. Chosen Structure

These bistable modules can not be assembled on a serial way. Two main reasons lead us to this conclusion. The first one is the weight that each module induces on the other ones. Indeed while increasing the number of modules, the weight that every module will support increases as well and creates an opposition force to the displacement of the bistable structure. The second reason is the most binding one, it involves the connector wires of the modules. As these wires are quite big compared to the size of the modules' components, they can block several modules of the serial structure. These two reasons introduce forces that are in opposition to the force created by the thermal actuators of the module, and may prevent these modules from switching. They are very restrictive and will in the best case deteriorate the good behaviour of the robotic structure, but could probably block the displacement of the entire robot. We abandoned the concept of a serial structure for the robot, and focused on a parallel design for the robotic architecture. The parallel structure is actually very good because it provides a strong robotic structure that could handle heavy components. It is very well fixed to the base of the robot, facilitating the powering of all the bistable modules and does not generates any problems with the connector cables. We conceived a structure that fits all the constraints previously mentioned, and can furthermore use only modules of the same displacement, making the fabrication process much easier. All the bistable modules used generate a displacement of 10 µm. The proposed architecture was created in order to generate a two dimensional workspace. This first digital microrobot is composed of six bistable modules occupying an area of 4 × 3 cm 2 . A CAD model of the mechanical structure of this robot is represented on Fig. 2. All the bistable modules of this structure are generating the same displacement of 10 µm. The workspace generated (Fig. 3) is a square of 4 µm length. It contains 64 discrete positions (2 6 ), each of them are stable and robust. This workspace shows no redundancy, all these positions are distinct. They are furthermore equidistant in the two dimensions of the referential R 1 , with a separation of 505 nm. The referential R 1 is the referential of the workspace (see Fig. 3), it is different from the referential of the structure R 0 (see Fig. 2) by a rotation of π 4 . This structure consist in six bistable modules, but we can easily extend it to a higher number of modules (all of them always generating the same displacement between their two states). By doing so, we don't change the size of the workspace generated, but only increase its resolution. From a theoretic point of view (considering perfect revolute joints), each time we add one module to the structure, we improve the resolution by two in one dimension (one side of the square). The dimension in which the resolution is improved depends on the side of the structure on which the module is added. This means that if we have a structure with 10 bistable modules (5 on each side of the structure), the workspace generated will be a square of 4 µm length, that contains 1024 distinct points, all equidistant with a separation of 126.25 nm. Introducing a resolution four times better in the two dimensions than with only six bistable modules. All these results are valid for the case in which all the rotoid articulations are perfect.

The resolution reachable by this robot depends on the number of modules we add to it. The better resolution we can reach is limited by the size of the wafer on which the robot will be fabricated (the size of the wafer limits the number of modules we can add). Because of discrete and highly redundant workspace, calculation of the forward and inverse kinematics is generally difficult for digital robots. While several studies have been made in this domain in [START_REF] Ebert-Uphoff | Inverse Kinematics of Discretely Actuated Hyper-Redundant Manipulators Using Workspace Densities[END_REF] and [START_REF] Lees | An Efficient Method for Computing the Forward Kinematics of Binary Manipulators[END_REF], they only consider the case of macroscopically serial manipulators presenting a hyper-redundant workspace. But, in the case we are presenting here, we have chosen a robotic architecture for which the kinematics calculation is simplified.

A. Forward Kinematics

The forward kinematics of this structure can be reduced to a simple form. For this calculation we consider the robot as a rigid structure with perfect rotoid articulations. As the size of the structure is very huge compared to the small displacements generated by the bistable modules (a ratio of 1000), the rotations considered are very small. All the trigonometric functions can then be linearized.

We define the position of the end effector by its coordinates x and y in the referential R 0 of the structure (see Fig. 4). Equation 1represents the forward geometric model of the microrobot.

x y = K • 1 1 2 1 4 -1 -1 2 -1 4
1 1 2 1 4 1 1 2 1 4 •         bl 1 bl 2 bl 3 br 1 br 2 br 3         (1)
The constant K in (1) depends on the geometric parameters of the structure, namely the length and width of the beams and the displacement of the bistable modules. The bl i ∈ {0; 1} defines the state of the module i on the left side of the structure, and the br i ∈ {0; 1} is for the modules of the right side.

From a generic point of view, if we have N 1 modules on the left side (named bl 1 to bl N1 ), and N 2 modules on the right side of the structure (named br 1 to br N2 ), the forward kinematics can be written as in [START_REF] Kim | Nanonewton force-controlled manipulation of biological cells using a monolithic MEMS microgripper with two-axis force feedback[END_REF].

x y = K • δl 1 • • • δlN 1 2 N 1 -1 -δr 1 • • • -δrN 2 2 N 2 -1 δl 1 • • • δlN 1 2 N 1 -1 δr 1 • • • δrN 2 2 N 2 -1 •           bl 1 . . . bl N1 br 1 . . . br N2           (2)
Where δl i is the displacement generated by the bistable module number i on the left side of the structure, and δr i is the displacement generated by the bistable module number i on the right side of the structure. The reader may notice that the constant K is different from the previous constant K. Indeed, the displacement generated by each module (δl i and δr i which were the same for every module in the previous case) was included in the constant K.

The forward kinematics developed here is reduced to a matrix multiplication. It is a generic formulation of the forward kinematics that can easily be adapted to any architecture of the same type. One important thing to notice in this matrice is that the displacement generated on the end effector by one module is half displacement generated by the previous module (on the same side of the structure). Thanks to this particularity, two different combination of modules cannot reach the same position. This induces a non-redundant equidistant workspace.

B. Inverse Kinematics

For digital robots, the inverse kinematic model calculation is quite difficult because we first have to know the exact location of every reachable positions, and find the position the closest to the desired one. The number of reachable positions is 2 n , where n is the number of actuators. This number n can easily exceed twenty, generating a huge list of positions. The difficulty of the calculation of the inverse kinematic model increases exponentially with the number of actuators. The redundancy property of the workspace make it even harder. But for the case we are dealing with now, the inverse kinematic model is quite easy to establish. Thanks to the particular configuration of this workspace, i.e. nonredundancy, square and uniform distribution.

For the inverse kinematics solution, we have to consider an other referential than the basis referential (R 0 ). We will work on the referential of the workspace (R 1 ). The difference between the referential of the workspace and the referential of the robot is only a rotation of π 4 . We define the desired position of the end effector X d by its components x d and y d in the referential of the workspace. We then need to know the resolution of the workspace. Two resolutions have to be known, the one on the x 1 axis (δ x ) and the one on the y 1 axis (δ y ).

The calculation of the inverse kinematic is composed of three steps for each side of the structure (this means six steps in total) :

1) Divide the desired position by the appropriate resolution ( x d δx or y d δy ) 2) Define the nearest integer 3) Convert it to its binary form Each bit of the binary number obtained represents the state of the bistable module of one side of the structure (the left side for x d and the right side for y d ). The modules are ordered from top to bottom. The most significant bit represents the state of the top module, and the least significant bit represents the state of the bottom module. This inverse kinematics representation is only valid for the particular workspace obtained here. If we change some geometric parameters of the structure, for example changing the ratio between all the beams of the structure, this will generate a new form of the workspace. And we will have to establish a different representation.

The limitation of this representation can be observed when increasing the number of modules used. When the resolution of the workspace becomes close to 10 nm, the inverse kinematics becomes less accurate because of non linearities not taken into account.

IV. FEA SIMULATION

This digital microrobot is entirely microfabricated and build in a monolithic structure. The use of flexure hinges instead of traditional rotoid articulations prevent us from backlash and other drawbacks frequently encountered with these traditional articulations. These flexure hinges have to be characterized in order to provide good behaviors, as well as some other parameters of the robotic structure. For this, we use the results generated by the simulations made with the FEA software Ansys. All these results provide informations The bistable module was already designed in a previous study in which its dimensions were defined. We only have to take the robotic structure into account. It is composed of two different elements which are combined together several times. These elements are the pseudo-rigid beams and the flexure hinges. The properties we will focus on to choose the size of these different elements are the mechanical stress generated inside the structure by its deformation, and the force applied by the structure onto the bistable modules. While undergoing the displacement of the bistable modules, the robotic structure will deform and tend to return to its rest position as all flexible structure would do. A restoring force is then applied by the structure onto the bistable modules. This force should not exceed a certain threshold which is the blocking force of the stop blocks (1.54 mN ), otherwise the robot will not be robust anymore. The stress registered inside the structure should also not exceed a certain threshold which is the silicon's rupture stress. We consider here that the limit is 1 GP a.

A. Hinges' Dimensions

We will first study the case on which the structure does not undergo any disturbances. First of all we have to choose the shape of the flexure hinges we are going to use.

Three main sort of flexure hinges can be used : circular hinges, beam hinges and ellipse profile hinges. As circular hinges' deformation is located in a very small area, which can be considered as a fixed point in some cases, we will measure very high stress. On the contrary, beam hinges' deformation is distributed along all the length of the beam, generating very low stress. Finally ellipse profile hinges can be considered as a mix of the previous two kind of hinges. It provides low stress with a more located deformation area than the beam hinges. We choose here to use circular flexure hinges in order to mimic the behavior of a traditional rotoid articulation. This kind of flexure hinges will undergo high stress, but as the displacements of all the elements of the structure are very small (several microns), the stress will be acceptable. These circular flexure hinges will furthermore provide very accurate rotations with an approximately fixed instant center of rotation. A circular flexure hinge is generally defined by two dimensions : its radius R and its neck thick-ness t. The ration t/R is often considered because it defines the behavior of the hinge. Studies were made in [START_REF] Yong | Review of circular flexure hinge design equations and derivation of empirical formulations[END_REF] to define the appropriate equation to use for different wide ranges or t/R ratio. In our case, we made finite element simulation of the whole structure (without the bistable modules) to define the appropriate dimensions of the different parts of the robotic structure. We noticed that the behavior of the robot becomes acceptable with a ratio t/R ≤ 0.5. So it seems to be a good idea to reduce the neck thickness of the hinges.

As we are going to microfabricate this robot in a clean room, it is better not to choose too small structures because errors of 1 or 2 µm can appear during the etching process and rupture risk is permanent while manipulating the structure during microfabrication. We then choose a neck thickness for hinges of 15 µm.

The curves representing the force applied on every module and representing the stress inside the structure for different values of the hinges' radius can be considered as a negative exponential curve that starts being constant with a radius of 60 µm. This radius is sufficiently high for performing small stress and forces, and sufficiently small for providing the behavior of a rotoid articulation, with the generation of a fixed instant center of rotation.

B. Beams' width

For this part, we consider a perturbation force applied on the end effector of the structure. We will indeed choose a structure that permits a robust workspace, which means that all the positions of the workspace should be robust to an external force. The bistable modules were actually designed in order to create robust microrobot, being able to handle forces of 1.54 mN . The forces generally encountered in the domain of micromanipulation are between 1 mN and 10 mN .

We still use the FEA software to define the properties of the structure. The forces applied on every modules and the stress inside the structure were measured for all the positions reachable by the robot while it undergoes an external force from 0 to 10 mN . The consequence of this force is a small displacement of the whole workspace. The displacement of the workspace depends linearly on the the force applied on the end effector of the robot. For the design of the robot we are focusing on, i.e. a beam width of 300 µm and hinges of 15 µm neck and 60 µm radius, a force of 5 mN induces a workspace displacement of 0.5 µm. But this displacement can easily be reduced by increasing the beam's width. For instance this displacement becomes almost ten times smaller with a beam's width of 700 µm.

But the most constraining characteristic is the force applied on every bistable modules. This force should never exceed the limit of 1.54 mN . If we consider a structure with beams of 300 µm width, the structure can undergo an external force of 6.5 mN before reaching this blocking force on one of the six bistable modules, while with beams of 700 µm the external force can not exceed 5.5 mN . As the first prototype of the digital microrobot will undergo testing of the force it can bear, we choose to use the structure that can handle the strongest external force, i.e. with beam width of 300 µm. Knowing the force applied on the structure, we can also imagine a control strategy which takes the displacement of the whole workspace into account.

The complete structure will then be composed of beams of 300 µm width and circular flexure hinges of 15 µm neck thickness and 60 µm radius. This structure may not be the most efficient one, but it is the best to create a first prototype that will endure several tests.

C. Validation of the Forward Kinematics

The simulations made with the FEA software can also be used for a first validation of the forward geometric model we have established before. We compare the workspace generated by the simulation with the one calculated by the geometric model. The results are shown in TABLE I, in which we focused on the differences between a structure containing beams of 300 µm and a structure with 700 µm width beams. The gap between the workspace generated by the simulation and the one generated by the calculation depends on the position considered. The average of the gap is 43.6 nm in the case 300 µm beam's width, and 24.0 nm for a structures with beams of 700 µm width. This offset difference is due to the deformation of the beams which is not taken into account by the geometric model. As the 700 µm width beam will show less deformation, it is predictable that the model fits better the simulation. If we try to introduce this offset's average inside the model's equations, then the difference between the simulation and the calculation is only composed of a very small fluctuation. This fluctuation is ±3.8 nm in the first case, and ±2.2 nm for the second, which is negligible compared to the resolution of the workspace. But as we will increase the number of modules in the structure, the resolution of the workspace will decrease and the gap between the simulated positions and the calculated positions will not be negligible anymore.

The geometric model we have established before is then compatible with the simulation results. This modeling is simple (matrix multiplication), and it fits very well the behavior of the structure.

V. CONCLUSIONS AND FUTURE WORKS

In this paper we have proposed a new concept of carrying microrobot. This domain of robotic is sparsely studied, but is becoming more and more required. This digital microrobot is based on the use of bistable modules, developed in a previous study ([11]). The robotic structure has been designed to obtain a square workspace, with a high resolution. The resolution of the architecture proposed here (with 6 bistable modules) is 500 µm, but we can easily reduce it twice, four times, or even more. Each position of the discrete workspace is moreover stable and robust without the need of any feedback. This new digital microrobot offers several advantages that overcome the problems of traditional microrobots (wear, backlash, non linearity, . . . ). We have moreover developed forward and inverse kinematic models which are easy to manipulate and fit very well the results of the FEA analysis.

We are now microfabricating in clean room the first prototype of this microrobot, and will compare the simulation results with the real system. After that a motion planning strategy will be developed for this particular non-redundant workspace.

Fig. 1 .

 1 Fig. 1. Bistable Module

Fig. 2 .

 2 Fig. 2. CAD model of the digital microrobot with six bistable modules

Fig. 3 .

 3 Fig. 3. Workspace generated by the robotic structure with 6 modules

Fig. 4 .

 4 Fig. 4. kinematic model of the robotic structure

Fig. 5 .

 5 Fig. 5. Representation of the inverse kinematic calculation process

Fig. 6 .

 6 Fig. 6. Elements of the structure studied with the results of the FEA software Ansys

VI. ACKNOWLEDGMENTS

The authors gratefully acknowledge the contribution of Direction Generale de l'Armement (DGA).