Laurent Laval

Gilles Richard

Laval Laurent

Richard Gilles

Use of Open Source in Integrated Modular Avionics for A380 Program

Keywords: SNMP, Open source, development process

come   L'archive ouverte pluridisciplinaire

Introduction

This paper presents the use of the open source approach on the SNMP software project developed for the Integrated Modular Avionics (IMA) for A380 Program.

The SNMP (Simple Network Management Protocol) is used to monitor the future A380 network called AFDX. This software function is widely present in standard Ethernet network, and runs on operating systems like Windows or Unix.

Open source of the SNMP function has been used as a basis for the development in order to reduce costs and to secure the development (in terms of delay and maturity). This paper presents the context of the project, then the experiment during the development of this project by using an Open Source.

Project overview

IMA Concept

Traditional aircraft functions runs on a number of dedicated hardware units. Considering that most of those hardware units perform basically the same functions (input acquisitions, processing and computation, and output generation), a natural optimisation of resources has been realised to share the development efforts by identifying common parts, standardising interfaces and encapsulating services…, in other words, to adopt a modular approach. Then, the next step was to share the hardware and software resources by integrating several functions on the same execution platform, with the appropriate segregation (spatial and temporal) between them. This modular approach is known as Integrated Modular Avionics (IMA).

A full IMA system includes a number of computing modules communicating over a shared network. The standard defined for classical Ethernet doesn't meet all the requirements of the avionics world. A set of additional services has been defined in order to provide a safe, deterministic and reliable network called AFDX (Avionics Full DupleX switched ethernet). The AFDX network uses as far as possible standards protocols. For AFDX maintenance purpose, i.e., failure detection reported by AFDX elements, the network management is made using the SNMP protocol. The SNMP is an application-level protocol part of the UDP/IP protocol suite.

Network management is designed to be as simple as possible. It is based on two elements:

• Network manager is responsible for running management application that monitors and controls the network subsystems. • Network subsystem agents can be processing modules like workstations, intelligent hubs, routers and bridge/switches that host SNMP agents. These SNMP agents are responsible for performing the functions that are requested by the network manager (monitoring, report on failure, configuration…). SNMP is the means by which the management station and the network subsystems communicate. SNMP is a simple protocol that allows a network administrator to inspect or alter variables on a network element from a remote management station.

The SNMP was designed in the late 1980s to facilitate the exchange of management information between networked devices. The first version of SNMP (SNMPv1) went through the standards-process quickly and became an Internet Standard in 1990. SNMP is supported by almost all network devices and is widespread used today. SNMP is the most popular protocol used to manage networked devices.

SNMP function

The SNMP part developed by Thales for the Integrated Modular Avionics (IMA) for A380 Program corresponds to an SNMP agent included on processing modules. It shares this task with the Network BITE (Built In Test Equipment) Function (NBF), which collects and centralises information on the network status and failures and performs error diagnosis and localisation.

Basically, the SNMP agent implements the SNMP protocol version 1 (Ref. [START_REF] Case | A Simple Network Management Protocol[END_REF]) and the MIB (Management Information Base). The SNMP agent interprets the SNMP messages, controls the MIB containing the information about the elements to be managed and send the response to the network manager. The MIB implemented is not the standard MIB generally used on ethernet network, but a specific MIB related to AFDX network.

The MIB is a structured database, a tree, that contains the information about the elements to be managed. Every resource to be managed is represented by an object in the MIB. The leaf objects of the tree are the actual managed objects, each of them represents some status object, counter, or related information that is to be managed. These objects allow the detection/localisation of a network failure and the analysis of the network (performance analysis, etc.) for maintenance and tests means purpose. A network management function may monitor the resource at that system by reading the values of objects in the MIB and may control the resources at that system by modifying those values.

Three general-purpose operations may be performed on objects with SNMP: ♦ get, to retrieve a set of objects values from an SNMP agent; ♦ set, to update a set of objects values in an SNMP agent and ♦ trap, when an SNMP agent sends an unsolicited objects values to a management application.

Prototyping Phase

In order to make measurement of critical resources (memory, cpu…) on an IMA platform, it has been planned to make an SNMP agent prototype. An open source has been used to develop this prototype with a minimal cost. The open source implementation should be simple and should have a modular design for allowing adaptations to our needs and operational requirements. The open source software found should be also reliable.

Open Source Software selection for prototype

The selection of the open source is subjective and does not try to cover all important packages available.

We choose an open source published in a book (Ref [START_REF] Comer | Internetworking with TCP/IP Volume 2[END_REF]) which was compliant to all these criteria that are dominant in the decision process concerning whether the open-source software can be reused.

Prototype results

Results produced by this prototype were very positive:

• An SNMP agent function that works correctly • An open source code simply and easily to understand that allows us to fit it to our needs with few adjustements. • Measurements on memory and timing constraints were found in line with our resources and margins. • The use of SNMP prototype allows us to have quickly a source with few remaining bugs.

• An open source code very simple and a sufficient documentation that did not need support.

As the use of the open source in the prototype was very positive, this version was a good solution to take the concepts used in the development and we decided to reuse this prototype in our development to secure technical aspects.

As software development from scratch is very expensive, we have to find solutions or opportunities to reduce this cost by reusing previous developed software (PDS); the use of open source can help us to reduce costs. However, the development of the SNMP software shall comply with the constraints of a development for the production of an embedded software for airborne systems.

4.

Constraints to use open source in aircraft embedded software development

Constraints on Aircraft embedded software

The production of software for airborne systems and equipment used on aircraft or engines, that performs its intended function with a level of confidence in safety, shall follow the DO-178 B guidelines (Ref. [START_REF] Rtca | Software Considerations in Airborne systems and Equipment certification[END_REF]) in order to contribute to the aircraft certification.

In order to be certified, the software production shall follows the software life cycle processes defined below: o Software development (specification, design, coding, integration). o The integral processes that ensure the correctness, control, and confidence of the software life cycle (software verification, software configuration management, software quality assurance, certification liaison). o Software planning For each process, the DO-178B describes:

• objectives for software life cycle processes • descriptions of activities and design considerations for achieving those objectives • descriptions of the evidence that indicate that the objectives have been satisfied.

In the IMA project, the development of the SNMP project shall apply the DO178B level C considerations. Of course the original open source did not respect all the constraints of the software life cycle.

Open Source Software definition and legal aspects

The term "Open Source software" is both an informal term that refers to software where the source code is available, and a precise definition established by the Open Source Initiative that implies some legal constraints like free redistribution, availability of a source code, and free modifications to adapt to our specific needs. For more details on this definition, refer to the Open Source Definition (http://www.opensource.org) For these legal constraints, it is necessary to verify by lawyers that the open source chosen can be used or not in a commercial product.

DEVELOPMENT PROCESS

The use of open source can help us to reduce cost in some phases of the software life cycle.

The relative estimated effort in each phase for a full development of this type of software is detailed as follows : 21 -22 -23 January 2004By using open source, we estimated at first to have a gain in design phase and coding phase.

Specification phase

Standards specification of the SNMP are the RFC documents. To improve the specification in order to produce faster a comprehensive first issue, we used:

• Internet documentation like FAQs that gives a lot of information • Analysis of a concrete example of protocol implementation Furthermore, specific measurements on SNMP usage domain in IMA project made with our prototype allowed us to solve quickly assumptions taken into account on SNMP response time requirements.

Design Phase

During this phase, it is interesting to understand the details of implementation in order to produce more robust code if we know how the protocol operates. The open source implementation shows data structures, source code and sometimes explains the underlying principles. This helps to answer many questions and explain many subtleties that allows product improvement. The documentation provided explained and showed how a judicious choice of data representation can make the protocol easier to implement and conversely how a poor choice of representation can make the implementation tedious and difficult.

Nevertheless, the design documentation provided with the open source was not adequate to be compliant with the DO178B considerations. So, we make a reverse engineering from SNMP protocol parts of source code. The design of the SNMP agent shall also take into account some specificity like AFDX MIB implementation, interfaces with Operating system and network drivers and others technical considerations linked to IMA environment.

The detailed implementation of the open source make easier to write software design documentation because we have access to some of the assumptions that went into the software. In the SNMP project, the Open Source allows to reduce the design phase duration and to get the good solutions to optimise design and performances.

PHASE INITIAL TECHNICAL EFFORT EXPECTED TECHNICAL EFFORT WITH USE OF OPEN SOURCE

Coding phase

The entire open source cannot be directly used. Importing lines of code or algorithm cannot be done due to the specific constraints for the production of software for airborne systems.

The open source chosen is a very compact source code, runs on Unix environment, uses dynamic allocation and recursive functions that are prohibited in our coding rules.

Due to the development on an embedded environment, specificities should also be taken into account like: o Embedded software restriction for The memory management (dynamic allocation prohibited, memory size limitation, …), the performance (code optimisation, specific embedded OS,…) o Drastic coding rules to have a better quality, maintenance, and a source code easily to test. o Interfaces with a specific operating system o Specific customer requirements

The original code has been rewritten in our project to respect these specificities. Nevertheless the data structures and concepts used for this open source implementation have been conserved and some parts of the new version are very similar from original code. Some parts as encoding/decoding SNMP protocol have been used as example to make easier the coding of the new version. For example, the number of lines of codes of the embedded source of the SNMP decoding/encoding parts, was about twice greater in order to respect the coding rules and the extra code needed for robustness.

The version of open software used, even if the code has been rewritten, allows us to reduce the number of bugs found during debug. In modified source code the number of introduced bugs was very low and the investigation/correction of them was very simple thanks to the open source code implementation.

Test phase

The test phase includes software tests and system tests.

In our quotation, we have planned to buy for tests purpose a SNMP manager COTS to validate the SNMP agent, but it was not possible to find a manager that can be adapted to all of our needs (manager that runs on several platforms (Unix, windows, Linux), control of SNMP messages exchanges, manager that can be launched by line command for executing tests in batch mode…). So because of all these constraints, we preferred to develop our own SNMP manager. For software tests, we have used some parts of Open Source mixed to proprietary components and tests tools components to build a specific tool that was qualified for generation of SNMP exchange (request/response). For system tests, we produced a specific SNMP manager by using also some parts of Open Source.

The use of open source in our project for test purpose allows us to develop easily a flexible test environment for software tests and system tests. The implementation of the open source code parts can be used directly because these tools run on host environment and are not constraints by certification.

Estimation of the gain provided by the use of open source

In the figure presented below, we estimate the gain of the use of open source in our project in each phase.

CONCLUSION

The open source has been used in all the parts of the development process from specification phase to test phase. All parts of the original open source code have been rewritten due to the constraints of our implementation, but few bugs have been introduced during this task. Open source is also interesting to produce flexible test environment. In each phase, the open source made the development easier.

The open source software has been ideally suited for reuse in our project context and could be used more generally in the development of protocol standards; it avoids to start a development from scratch.

Open source process selection is very important on obtained results.

Our experiment shows that :

• The initial development delay was not significantly reduced • The cost was reduced by 20 % versus a classical development • The product is robust Now we expect :

• A low number of remaining bugs • A low cost of maintenance

Figure 2 - 1 :

 21 Figure 2-1: IMA communication infrastructure (simplified)

Figure 2 - 2 :

 22 Figure 2-2: AFDX maintenance structure -general view

  As the SNMP version 1 is a standard defined in 1990, an important number of open source software implementation are available today. The choice of the open source must be done following specific criteria that seems to us important for our development constraints. The retained criteria was:o A documentation available (completeness and consistency).

o Simplicity, readability and maintainability of code implementation. o An operational open source version widely used.

Comprehensive and qualitative documentation was a key driver for the adoption of an open source in our project. A good documentation would help us to produce software specification and software design documentation during the retro-engineering phase.

-22 -23 January 2004


F Brochard-Wyart

P G De Gennes

O Sandre

Transient pores in stretched vesicles : role of leak-out

Keywords: . : 87.22.Bt (Membrane and subcellular physics and structure), 87.45.-k (Biomechanics, biorheology, and biological fluid dynamics)

We have visualized macroscopic transient pores in mechanically stretched giant vesicles. They can be observed only if the vesicles are prepared in a viscous solution to slow down the leak-out of the internal liquid. We study here theoretically the full dynamics of growth (driven by surface tension) and closure (driven by line tension) of these large pores.

We write two coupled equations of the time evolution of the radii r(t) of the hole and R(t) of the vesicle, which both act on the release of the membrane tension. We find four periods in the life of a transient pore : (I) exponential growth of the young pore; (II) stop of the growth at a maximum radius r m ; (III) slow closure limited by the leak-out; (IV) fast closure below a critical radius, when leak-out becomes negligible. Ultimately the membrane is completely resealed.

I. Introduction

Forcing the passage of molecules, or genes, through a cellular membrane is a central problem of drug delivery. Model experiments based on vesicles represent a first step in this direction. A variety of physical techniques have been proposed to increase the permeability of lipid bilayers : a) raising the osmotic pressure inside a vesicle induces a surface tension σ, and the permeability (of dyes, or of spin labels) is significantly increased [1] b) if a bilayer becomes stuck on a porous surface (e.g. with a cationic bilayer and a negative surface) it tends to invade the pores; this again creates a tension σ and an extra permeability [START_REF] Guedeau-Boudeville | Proc. Natl. Ac. Sc[END_REF] c) instead of a porous medium it is possible to use a patched solid surface, some regions being attractive, and some being neutral or repulsive : a vesicle stuck on this surface becomes more permeable, or even breaks [START_REF] Bernard | [END_REF] d) electroporation is a classical technique [4,5] : with voltage drops of the order of 1

Volt across the bilayer, some large pores can be induced.

In a recent series of experiments [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] some of us have studied giant vesicles where the tension σ could be established by two different ways :

(i) adhesion on an attractive surface, which generates flattened vesicles (ii) irradiation of a vesicle (doped with suitable fluorescent dyes). For some (mysterious) reason, the equilibrium area per polar head under illumination is slightly reduced, and a tension σ appears (within minutes). An effect of the same kind was reported for unlabeled vesicles submitted to laser tweezers [START_REF] Bar-Ziv | [END_REF]. This optically induced tension is very convenient, because it allows to work in a simple (spherical) geometry.

Another important trick introduced in ref. [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] amounts to replace water by a more viscous mixture of water and glycerol (typical viscosity η 0 =30cPoises). This allows to observe the formation, growth, and ultimate closure of large pores (radius r ≈ a few microns).

The role of glycerol is explained in ref. [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] : a large pore allows for a certain leak-out of the inner compartment which has been known for some time [5,8]. Leak-out reduces the tension σ, and leads to pore closure. But with glycerol this leak-out becomes very slow, and we can watch large pores persisting over long times (seconds). Some of the salient features of growth and closure in the slow leak-out limit have been modelized in ref. [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF].

Our aim in the present paper is to make the theoretical discussion more general, in two directions : a) we discuss fast leak-out as well as slow leak-out b) it is assumed in ref. [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] that the growth and the late stages of closure were dominated by the internal viscosity η 2 of the lipid layer. This was correct for the experiments at hand, but in some other cases, all steps may be governed by the solvent viscosity η 0 . This limit is discussed here in an appendix.

In section II we construct the dynamical equations describing the pore size r(t) and the overall radius R(t) of the vesicle -allowing for fast or slow leak-out. We display some numerical result on r(t) for a few typical cases. In section III we concentrate on the slow leakout regime : here, it is possible to derive explicit formulas describing the four major time intervals involved : growth (I), bloom (II), leak-out (III) and ultimate closure (IV). Some of the physical questions which appear are discussed in section IV.

II. Transient pores

1) Counting the areas

The geometry is shown on Fig. 1. We constantly assume that the pore area (πr 2 ) is much smaller than the overall area of the envelope sphere (4πR 2 ). We call R i the radius of the original vesicle under initial tension (σ 0 ) and R 0 the radius in zero tension (σ=0).

The lipid area A L differs from 2 0 4 R π because tension stretches our system :

      + = E R A L σ π 1 4 2 0 (1)
where E is a two dimensional modulus. In the regime of interest here (weak tensions) E is not related to the Van der Waals interactions in the lipid. It is in fact controlled by the unfolding of "wrinkles" (fluctuations) of the surface [9].

kT K R K E b b 2 0 48π = (2)
where K b is the Helfrich bending constant [10] and kT is the thermal energy. The overall distribution of areas is ruled by :

2 2 0 2 2 1 4 4 r E R r A R L π σ π π π +       + = + = (3)
It is sometimes convenient to define a critical pore radius r c which corresponds to the complete relaxation of the tension (σ=0) in situations of zero leakage (R=R i ). Thus

E R r c 0 2 0 2 4 σ = (4)
2) Rate equations a) changes of the pore radius r(t) are driven by two forces :

(i) the tension σ (favoring expansion) (ii) the line energy ℑ of the pore (favoring closure)

When the internal viscosity of the bilayer is dominant [11], this leads to

r r r d ℑ - = σ η  2 2 ( 5
)
where d is the lipid thickness. In most macroscopic physical systems, r / ℑ is a negligible correction. But here it is important, because the tensions σ are unusually small in vesicles.

b) Leak-out provides a way of changing the overall solvent volume, as explained in ref. [5,[START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF]8]. The leak-out flux is

2 const. r V Q L =
where V L is the leak-out velocity. The shear stresses involved in this outward flow are of order η 0 V L /r where η 0 is the solvent viscosity. They are balanced by the Laplace pressure

p=2σ/R. The result is R R r R Q  2 3 0 4 3 2 π η σ - = = (6)
On the whole, we now have three equations [START_REF] Bernard | [END_REF]5,[START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] for three unknowns (r, R, σ).

3) Non dimensional form

In the following, we consider small variations of the vesicle radius

( ) δ + = 1 0 R R and
( )

0 0 1 δ + = R R i
at t=0, with δ,δ 0 <<1. Then the critical pore radius introduced in Eq. ( 4) is given by

2 0 0 2 8 R r c δ = .
The two radii can be expressed in reduced units : . This latter represents the drop of the vesicle radius due to leak-out : ∆ varies from 0 to 1 as R decreases from R i to R 0 . The reduced time is

τ t t ~= with d 2 0 2 1 η σ τ = (7)
Introducing the reduced surface tension

0 σ σ σ = ~, Eq. (3) rewrites ∆ σ - - = 2 1 r ~ (8)
The differential equations (5,[START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] are normalized as

       = ℑ - = L r r t d d r t d r d 3 σ ∆ σ ) (6' ) (5'
The system (5', 6') contains only two adjustable parameters The radius

c L L r r r =
is the upper pore size determined by leak-out first introduced in ref. [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF]. The two extreme cases are (i) instantaneous release for r L =0 : pore never opens (ii) gelified content for ∞ →

L r ~

: there is no leak-out at all, and ( ) 0

= t ∆
all the time. Then Eq.

(5') reduces to ( )

2 1 r r t d r d - =
and can be solved analytically, as in [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF] :

t r r ln r r ln i i = - - - 2 2 1 1 2 1 (11)

4) Numerical simulations

In the following we take as a conjectural value 15 0. r ~i = for the initial radius, which comes from the fits of Eq. (11) with experimental data on vesicles that burst irreversibly [START_REF] Sandre | Proc. Natl. Ac. Sc[END_REF].

We vary L r ~ in a broad range (10 -2 to 10 4 ) as a model of the thickening of the ambient liquid.

Simulations are performed using the simple Newton algorithm with a variable time step t ∆ and an iteration number N ranging from 4000 to 160000 for the largest L r ~. We show here typical results : which corresponds to a nearly symmetrical peak with maximum area. This means that there is a solvent viscosity that maximizes the delivery of the vesicle content : this effect could be useful for drug delivery by artificial vesicles and endocytosis processes involved in cells.

ii) Slow leak-out ( 1

>> L r ~)
In that case, the slow closure (III) takes much more time than the three other stages of the long-lived pores. The closure velocity V 3 (defined as the slope of the curves on Fig. 3(a

iii) Influence of the line tension

The first role of the line energy ℑ ~ is to limit the pore nucleation.

If i r > ℑ (or i r 0 σ > ℑ
), the force acting on the pore edge is always negative, and it shrinks immediately.

The other effects are studied by varying ℑ ~ among three values : 0.05, 0.10 and 0.14(<0.15).

We chose 5 = L r ~, an intermediate value between fast and slow leak-out, which fits rather well our experimental results (that will be presented in a forthcoming paper). It is clear on the curves of Fig. 4 . This fast regime (IV) will be discussed in the next section. iv) Scaling laws (Fig. 5)

In order to compare the simulations to analytical formulas derived in section III, we analyze here the variation of some characteristic features of the curves with the two control parameters L r ~ and ℑ ~ :

III. The slow leak-out limit

We can solve the adimensional equations (5') and (6') in the limit of slow release 1 >> L r ~. This condition simplifies the analytical resolution because the characteristic time of leak-out

τ τ L L r ≅
is much larger than the rise time τ. Therefore the initial growth of the pore is decoupled from the slow release of the encapsulated liquid. We analyze in this limit the four regimes of the life of a transient pore defined on the experimental curve (Fig. 1).

Regime (I) : Growth

At time t=0, a pore nucleates at a radius r i . This nucleation may be induced by a surface defect (dust particle, chemical heterogeneity, …) or by thermal activation. The pore grows for ℑ > r ~i

. At short times, we have the following approximations :

   = = 1 0 σ ∆ ~ or with dimensional units    = = 0 σ σ i R R (13)
Eq. (5') then reduces to r t d r d = , i.e. :

t ĩe r r ~≅ τ / t i e r r ≅ (14)
In the limit 1 >> L r ~, the solution over the whole regime I verifies ∆=0, and the pore radius is given by Eq. (11) . We can estimate ∆ m by using a scaling solution of Eq. (6') :

L m L m m m r r r r ~ℑ = ≅ 2 3 σ ∆ L m m i r r R R 0 2 2 2 4 σ ℑ ≅ - (16)
In the limit 1

>> L r ~, m r
~ becomes close to one, and ∆ m <<1. Eq. ( 15) leads to :

( ) 2 1 m m r r ~- ≅ ℑ (17) i.e. 2 1 ℑ - ≅ r ~m 0 2σ ℑ - ≅ c m r r ( 18
)
The parameter

0 σ / ℑ
has a simple meaning : it is the nucleation radius of a pore (in conditions of ideal nucleation) as derived from a pore energy

ℑ -r r π σ π 2 0 2
. Indeed, this radius is small (<1µm).

The numerical simulations show that the maximum pore radius fits well Eq. ( 17 The curvature

ℑ - = - = - = r r r r r r ~L m L m m m m m 3 4 σ ∆    tends to zero like 1 - L r ~ when ∞ → L r ~.
Regime (III) : Quasistatic leak-out (r 23 >r>r 34 )

As r(t) starts to decrease, σ(r,R) grows : a release of the inner liquid is then necessary in order to maintain an almost zero surface tension. More precisely, the pore closes if the driving force is negative, i.e. :

ℑ < r ~σ ℑ < σ r ( 19
)
We shall see that the inequality ( 19) is very nearly an equality : in regime (III) the driving force of Eq. ( 5) is nearly zero

r / ℑ ≅ σ or 1 << ℑ - σ σ r / ( 20
)
We may say the regime (III) is quasistatic. A detailed argument for this follows :

We calculate the derivative of Eq. (5') :

( ) ( ) ∆ ∆      + - - - = r r r r r r ~2 1 2 (21)
In this regime, the closure velocity is very slow, and we can assume

ℑ ≅ r ~σ to evaluate ℑ ≅ r r ~L2 ∆  . Eq. (21) becomes : 0 2 3 2 ≅ ℑ -         - ℑ ≅ r r r r r r ~L    (22)
We set 0 = r   because the scale time variation for leak-out is L r ~ times larger

( 1 1 << ≅ L r r r   ) : the closure is at almost constant velocity. If 3 r 2 ~<< ℑ
(or r>r 34 , which defines the limit of regime (III), where the pore is not too small so that leak-out has a significant effect), the first term between parentheses in Eq. ( 22) is negligible. This leads to :

0 2 ≅ ℑ + r r r ~L  (23)
Introducing r 23 and t 23 as the cross-over values between regimes (II) and (III), the solution is : When the size of the hole becomes too small, leak-out is nearly suppressed. The radius r 34 at cross-over between regimes (III) and (IV) has already been introduced, and verifies :

ℑ ≅ r ~3 34 2 0 2 3 34 2 σ c r r ℑ ≅ (26)
The vesicle has almost reached a constant radius ∞ R and Eqs. (5', 6') becomes :

( )      ≅ ℑ - - - = ∞ 0 1 2 ∆ ∆   r r r ~ (28) (27)
Assuming that ℑ ≅ r ~σ is still valid at the cross-over enables to estimate the surface tension at the end :

3 2 2 34 2 34 34 89 1 3 1 / . r r r ~ℑ ≅ ≅ + ℑ ≅ - = ∞ ∞ ∆ σ (29)
This relation (also verified on the numerical simulations) shows that the vesicle recovers a non-negligible surface tension at the end of the pore closure. For example above 40% of the initial tension is maintained for 10 0. ~= ℑ . This could explain why series of successive pores are observed in the experiments.

The fast closure of the pore is governed by Eq. ( 27), which rewrites :

( ) 3 34 2 2 34 2 3 r r r r r ~-- =  (30)
We do not propose an analytical solution that would be valid for the whole duration of regime (IV). Instead, we just look at the final stage, when the equation is linear :

      - ≅ 34 2 34 3 2 3 r r r r  (31)
This is a good approximation after a time t 4 that is defined arbitrarily such as ( )

3 34 4 r t r ~= (32)
Then the integration leads to :

( ) 2 3 2 3 1 4 2 34 34 ln t t r r r ln - - =         - (33)
which can be linearized as ( )

4 34 3 2 2 t t r ln r ~-ℑ - ≅ (34)
Therefore it appears that the final closure of the pore is at constant velocity :

d V 2 4 2η ℑ ≅ (35)
This linear regime is valid over a range that is not negligible, since ( ) before dying abruptly (regime IV). In the limit of slow leak-out ( 1 >> L r ~), the dynamical equation for r(t) can be derived by a simple scaling argument. Line tension closes the pore with a net power that equilibrates the entropy production per unit time :

3 2 0 r r V S T r L       = = ℑ - η   ( 36
)
The viscous losses are due to flows of solution through the pore. The leak-out velocity has already been estimated as

R r V L 0 η σ =
. The closure is quasi-stationary and we can use

approximation (20) to get R V L 0 η ℑ ≅ . Thus Eq. (36) rewrites r R r 2 0 2 η ℑ = ℑ - (37)
This simple expression contains the salient features of regime (III) : the logarithm of the pore radius decreases linearly in time, with a slope in agreement with Eq. ( 24). Of course the exact prefactor cannot be obtained by this scaling argument.

2) Looking back at Fig. 1, our theoretical picture allows us to derive with a good accuracy two important parameters of the membrane: the surface viscosity η s =η 2 d and the line energy of a pore. Indeed the ratio between the velocities in the two linear regimes (III) and (IV) contains η s as the only unknown :

s m r R V V η η π 0 2 0 3 4 4 3 = (38)
The values R 0 =14.5µm, r m = 4.5µm, ).

The thickness of a phospholipid bilayer being d≈3.5nm, we predict the bulk viscosity of 1,2dioleoyl-sn-glycero-3-phosphocholine (DOPC) : . The usual measurements of line energies ℑ are extremely delicate [4,5,8,12], and ℑ is expected to be sensitive to certain lipid impurities.

We have studied one extreme case, based on the well-known effect of cholesterol to stiffen the bilayers. Our preliminary results show that the line energy is three times larger for a membrane containing DOPC and 30mol% cholesterol.

3) The presence of glycerol may modify the membrane characteristics and the twodimensional mobility of lipids. Vesicles of DOPC containing a hydrophobic fluorophore were studied by time-resolved fluorescence spectroscopy [13]. The rotational motion of the molecular probe was slowed down at high glycerol content (in a 91:9 w/w mixture of glycerol and water, the rotation time becomes three times larger than in water). This result tells us that a slight viscous thickening of the lipid is observed, but no dramatic effects are reported. This is crucial because the maximum size of transient pores in the fast leak-out limit is

2 0 0 R r s L η η ≅ .
If we assume no dependence of η s on the glycerol content, the size of transient pores in pure water are expected to be thirty times smaller : 100-200nm. These pores open and close before reaching a visible size in optical microscopy. But their presence explains certain anomalous permeabilities observed for stretched adhesive vesicles [14]. They have also been observed in the membrane of human erythrocytes [START_REF] Chang | Guide to Electroporation and Electrofusion[END_REF]. The authors used a very clever setup to freeze the cells with a controlled time delay after electroporation, and observe them later by electron microscopy. Despite statistical scatter among the cells, they reached a good insight of the pore dynamics. They divided it into three stages : (i) within 3ms, pores expand rapidly up to 20-40nm in diameter (ii) between 20ms and 220ms they saturate at a maximum diameter of 100-160nm (iii) after 1s to 5s almost all the pores have shrank. This scenario looks similar to ours except that the scales of times and pore sizes are about thirty times smaller.

4) We assumed that, at all times, σ is uniform all over the vesicle. This means that no rim surrounds the hole. This is the signature of plug flows extending over large distances, which have been observed in the bursting of polymer "bare" films (i.e. with no surfactants, [11]). An experimental evidence of this assumption is that no bright circle around the pore is visible in fluorescence microscopy. This simplification may be lost when the membrane viscosity is no more dominant. Our experiments on liquid/liquid dewetting have shown that indeed a rim appears when dissipation in the bulk liquid overcomes dissipation in the film [16].

Note added in proof: While this paper was in review, we became aware that Eq. ( 15) in H. Isambert, Phys. Rev. Lett. 80 (1998) 3404-3407 is an equivalent form of our Eq. ( 11) for the pore radius vs. time in the case of negligible leak-out.

Appendix : transient pores in low viscosity membranes

We now study the opposite limit, when the viscous dissipation in the membrane is small compared to the dissipation of the backflows induced by the pore opening in the surrounding liquid. The extension of Eq. ( 5), incorporating a mixed dissipation both in the membrane and in the solvent may be written as

ℑ - = + σ η η r r d r r   2 0 2 (A1)
The first term is the contribution of the viscous dissipation in the solvent. It can be justified by the following scaling argument. The entropy production per unit time is

3 2 0 r r r S T       ≅   η
, where r 3 is the volume of the flows occurring through the pore. The transfer of surface and line energies into viscous losses leads to Eq. (A1). Notice that for the backflows in the solvent, we have only a scaling form and we do not know the exact numerical coefficient. This is not true for the second term, because dissipation due to radial plug flows in the membrane was calculated exactly.

We study here the case where solvent dissipation is dominant. This implies where

        - - - - = 2 0 2 2 2 2 2 0 1 R R R R r r i i c σ σ
The other rate equation (describing leak-out) is not modified Pores will open at constant velocity g r  (I) up to a large size r m (II). Then they close slowly during step (III) which is identical to the previous case, with a closure velocity

2 0 0 3 3 2 R r V m πη ℑ ≅ .
The cross-over radius 34 r between slow and fast closure is unchanged. But the fast regime (IV) is entirely different. Eq. (A1) shows that ( )

t t r - ℑ ≅ ∞ 0 2 η
, i.e. the slope as 0 → r becomes infinite. The line tension can still be deduced, from the curvature of r(t) near r=0.

Numerical simulations of Eq. (A5) are shown in Fig. 6 for several values of ' r L (=5, 10, 50).

Glossary

  see "aborted" pores with a dynamics in three stages only : growth (I), maximum (II) and fast closure (IV). The slow closure regime (III) appears clearly for 1 ≥ L r ~, as seen on Fig. 2(a). It becomes broader when L r ~ increases further. An intriguing result is that the final drop of the vesicle radius ∞ ∆ (or equivalently the surface tension at end ∞ σ ~) is not a monotonous function of . 2(b), 2(c). A look to the curves of the outward flow on Fig. 2(d) helps to understand this. The peak value of Q decreases monotonously with L r ~, but the peak shape is not symmetrical : the left tail is lacking at The release of the vesicle content and the relaxation of surface tension being proportional to the integral of Q, they are both maximum at

  )) decreases when L r ~ increases, for a given value of ℑ ~. But the radius 34 r ~ at the crossover between slow (III) and fast (IV) closures does not vary ( ). The final value of ∆ (and hence of the vesicle radius) is also constant, as seen on Fig. 3(b) : in the slow leak-out case, raising the solvent viscosity increases the pore lifetime, but it does not change the efficiency of the content release. However, one should keep in mind that Eq. (5) stands for a viscous dissipation dominated by the flows of lipid. For a very viscous content ( is developed in the Appendix.

  that, at higher line tension : (a) the pore reaches a smaller maximum radius m r ~ and closes faster; (b) the decrease of the vesicle radius (and so the released volume) is smaller; (c) there is less relaxation of the surface tension at end; (d) the peak of the outward flow occurs at a later time. This last observation means that, for 10 < L r ~, the line energy ℑ ~ plays a role even in the growth regime (I) : it slows down the pore opening which cannot be described simply by Eq. (11). The two closure regimes (III) and (IV) depends also directly on ℑ ~. The plot of the closure velocity (i.e. the negative values of r  ) vs. pore radius (e) shows two parts : -a plateau between m r ~ and 34 r ~ corresponding to regime (III) at almost constant velocity denoted V 3 -an acceleration of the closure, with a final velocity ℑ = ∞ r 

  (a) the maximum pore radius m r ~ vs. L r ~ m r ~ starts to increase with L r ~, then it saturates at a level that depends on ℑ ~ only. (b) the slow closure velocity vs. L r ~ Although the pore radius ) t ( r ~ appears linear in time during regime (III), a better linear regression is obtained when we plot ) t ( r ln vs. t ~. The slope is then plotted as a function of L r ~ for the three values of ℑ ~. We find a scaling law that is valid from 10 = smaller L r ~, this law overestimates the slope, which tends to a value that depends on ℑ ~ onlyregime (III) is undistinguished from the final closure at velocity ℑ = ∞ r  (the difference between ℑ ~ and the saturation levels on Fig. 5(b) comes from the semi- logarithmic plot). (c) the surface tension at the end ∞ σ ~ vs. ℑ the following section, we derive analytical developments of the solutions ) t ( r ~ for the "slow leak-out limit" 1 >> L r ~. Interestingly, we have shown here numerically that, in practical, the condition 10 > L r ~ is sufficient to ensure the validity of the scaling laws.

  ) : Maximum radiusThe hole grows up to m r ~, and starts to decrease. At its maximum size,

  than 1% uncertainty : Fig.5(a). The linearized form (18) becomes a good approximation for small values of ℑ ~.

  very closed to the scaling law deduced from Fig. 5(b). A linearized form of Eq. (24) is ) : Fast closure (r<r 34 )

  thickening of the solution increases the size of transient pores. The cross-over between "fast" and "slow" leak-out is ruled by d blooming of pores (regime II) occurs for a radius L m r r ≅ : pores abort before reaching the equilibrium size r c , because enough surface tension is relaxed by the fast release of the vesicle content. If 1 > L r ~, a full blooming of pores is allowed : slowing down leak-out leads to mature pores, now at almost their equilibrium radius. After blooming, pores close slowly (regime III),

,

  t=0)=R i describes the full life of transient pores in that limit. At short times the pores grow at constant velocity where σ 0 is the stress before hole opening. We can define a characteristic time of Because the same viscosity is involved in the pore expansion and in solvent release, η 0 does not show up in the controlled parameter. In addition the pore can reseal only if r c <R 0 (otherwise the vesicle bursts irreversibly). Therefore in practice 1 > ' r L, which means that when dissipation in backflows dominates, the pores are always in the slow leak-out regime.

Fig. 1 :Fig. 2 :Fig. 3 :Fig. 4 :

 1234 Figures and captions

Fig. 5 :Fig. 6 :

 56 Fig. 5 : Scaling lawsthe leak-out parameter L r ~ is varied over a broad range, and three values of the line tension ℑ ~ are studied : 0.05 (closed circles), 0.1 (open circles) and 0.14 (closed triangles); (a) maximum pore radius m r ~ vs. L r ~; (b) closure velocity during regime (III) (slope of semilogarithmic plot ) t ( r ln vs. t ~) vs. L r ~.


Hamza Sahli
email: hamza.sahli@inria.fr

Thomas Ledoux
email: thomas.ledoux@inria.fr

Éric Rutten
email: eric.rutten@inria.fr

Modeling Self-Adaptive Fog Systems Using Bigraphs

Keywords: Fog systems, Self-adaptation, Formal methods, Modeling, Bigraphical reactive systems

Fog systems are a recent trend of distributed computing having vastly ubiquitous architectures and distinct requirements making their design difficult and complex. Fog computing is based on an idea that consists of leveraging both resource-scarce computing nodes around the Edge to perform latency and delay sensitive tasks and Cloud servers for the more intensive computation. A convenient way to address the challenge of designing Fog systems is through the use of formal methods, which provide the needed precision and high-level assurance for their specification through formal verification. In this paper, we present a novel formal model defining spatial and structural aspects of Fog-based systems using Bigraphical Reactive Systems, a fully graphical process algebraic formalism. The model is extended with reaction rules to represent the dynamic behavior of Fog systems in terms of self-adaptation. The notion of bigraph patterns is used in conjunction with boolean and temporal operators to encode spatio-temporal properties inherent to Fog systems and applications. The feasibility of the modelling approach is demonstrated via a motivating case study and various self-adaptation scenarios.

Introduction

Fog computing [START_REF] Mouradian | A comprehensive survey on fog computing: State-of-the-art and research challenges[END_REF][START_REF] Yousefpour | All one needs to know about fog computing and related edge computing paradigms: A complete survey[END_REF] is an emerging paradigm that aims to decentralize Cloud systems with distributed micro data-centers in the core network and even more resource-scarce devices at the Edge of the network. The main idea behind the Fog is to leverage resources around the Edge to perform latency and delay sensitive tasks closer to end-users and thus avoid network bottlenecks. Cloud servers are exploited only for the more intensive and latency insensitive functions. By introducing location-based awareness, the Fog paradigm grants enhanced performance and more assurance about computation and data placement.

A typical Fog system architecture is considered as a set of heterogeneous computing nodes scattered across separate layers. The bottom one is the Edge or the Fog layer organized as multiple clusters acting as small to medium sized data-centers close to data producers. Each of these clusters is composed of several computing devices of different kinds, referred to usually as Fog/Edge nodes. The latter can range from networking devices equipped with low computing capacities (e.g. routers) to more powerful computing entities (e.g. Raspberry Pi). Fog nodes are ubiquitous by nature, sometimes mobile and mostly possess limited processing power, storage and energy abilities. The top layer of a Fog system is the Cloud layer which contains much powerful servers performing computationintensive tasks. Deployed on resource-scarce computing nodes, a Fog application should be designed as a set of loosely coupled and fine-grained components. To this end, the concept of micro-services provides a new architectural style where Fog-based applications can be quickly deployed and smoothly scaled. In such highly dynamic and large-scale Fog systems, aspects such as locality of nodes and their characteristics, cluster formations and neighboring relation, services distribution, as well as Fog systems temporal evolution are key concerns making the task of designing Fog systems challenging. The main questions we address is how to design a Fog system accurately and the proper means to express faithfully properties providing assurances about respecting system and application constraints/requirements while continuously evolving over time. Formal methods offer the appropriate answers to tackle these open issues. They present mathematical concepts which provide the needed rigour and high-level assurance for qualitative specification of Fog systems infrastructures and applications, in addition to their dynamic behaviors and spatio-temporal properties.

In this paper, we propose a preliminary modelling approach for self-adaptive Fog systems based on a formalism introduced by R. Milner [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF]. Bigraphical reactive systems (BRS for short) is adopted as a formal foundation for its ability to represent the hierarchical locations of Fog-based systems entities and applications, as well as their characteristics and the complex interactions between the various elements. The notion of bigraphical reaction rules is used to capture the temporal evolution of Fog systems in terms of self-adaption in a natural way. Besides, bigraph patterns can be combined with standard boolean operators or more expressive temporal logic operators to define spatio-temporal properties related to such systems behavior and Fog applications requirements, serving as a basis to perform formal analysis. Moreover, BRS is characterized by a humanoriented graphical aspect supporting equivalent representation to algebraic ones. This feature provides an intuitive representation of Fog-based systems making them more convenient to comprehend by DevOps engineers. All these distinctive features among others omitted here (e.g. the concept of regions very close to distributed layers) make BRS formalism a fitting candidate to formalize Fog. Although other formalisms may present more or less suitability in some modelling areas to some extent, we advocate that BRS is a more fitting as it covers ideally most modelling requirements of Fog systems and allows to express and reason about their behavioral properties via formal verification.

Bigraphical reactive systems were applied on a wide range of distributed and ubiquitous system such as multi-agent systems [START_REF] Mansutti | Multi-agent systems design and prototyping with bigraphical reactive systems[END_REF], wireless networks [START_REF] Calder | Real-time verification of wireless home networks using bigraphs with sharing[END_REF], IoT in-frastructures [START_REF] Sevegnani | Modelling and verification of large-scale sensor network infrastructures[END_REF], Cloud-based elastic system [START_REF] Sahli | A brs-based approach to model and verify cloud systems elasticity[END_REF]10]. Among existing bigraphical approaches, the most related ones in principal to ours are [START_REF] Sevegnani | Modelling and verification of large-scale sensor network infrastructures[END_REF] where a BRSbased framework for modelling large-scale sensor network infrastructures and verification of temporal logic properties specifying application requirements is proposed. Authors in [START_REF] Tsigkanos | Modeling and verification of evolving cyberphysical spaces[END_REF] presented a similar bigraphical approach for the modelling of evolving Cyber-Physical Spaces and reasoning about spatio-temporal properties. To the best of our knowledge, the approach we propose here is the first to adopt bigraphical reactive systems for modelling structural and behavioural aspects of Fog systems and formalizing relevant constraints and properties. As a matter of fact, we believe our model is the first of its kind to apply a formal method in order to address these kinds of aspects inherent to Fog systems.

The remainder of this paper is organized as follows. Section 2 summarizes the main elements of BRS. In Section 3, we propose a formalization of Fog systems, then we address the representation of structural aspect using sorted bigraphs and finally we extend the model to include dynamic behaviour in terms of self-adaptation. Section 4 is dedicated to presenting a motivating case study, several adaptation scenarios and properties demonstrating the feasibility of our approach. Finally, Section 5 concludes and discusses our perspectives.

Bigraphical Reactive Systems

Bigraphical Reactive Systems (BRS) is a universal meta-modeling formalism originally defined by R. Milner in [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF] to provide a fully graphical formal model that emphasizes the orthogonal notions of locality and connectivity. The formalism comes as well with a mathematical algebraic language capable of describing the structural and behavioral aspects of ubiquitous and interacting systems that evolve in both time and space. A BRS BG(Σ, R) consists of a category of bigraphs defined over a sorting discipline Σ to represent the state of a given system and a set of parametric reaction rules R defining the dynamic evolution of the system by modeling the temporal self-adaption of the set of bigraphs [START_REF] Milner | The Space and Motion of Communicating Agents[END_REF]. A bigraph consists of a combination of a place graph, i.e. entities in terms of spatial distribution and nesting, and a link graph specifying the interconnections between these entities. Graphical and Algebraic Forms. Bigraphs can be described in two ways, in a diagrammatic depiction or with an equivalent algebraic representation. Figure 1 depicts the anatomy of a simple bigraph. Graphically, a bigraph as an ordinary graph is composed of several nodes linked by edges. Nodes encode the modeled system entities which can be real or virtual, while edges or links represent the various interactions and relationships between the entities. Nodes are always nested within regions, i.e. roots, depicted by dashed rectangles; they may also be nested within each other. This defines a parenting relationship between them in terms of nodes containment, or in other words the place graph of the bigraph. As a rule, nodes in the theory of BRS are permitted to take any kind of shape or color in some cases. A node can be dotted with zero, one or many ports used to link it with other nodes by means of edges, forming a link graph of a bigraph. A control is associated with each node consisting of a node type identifier. Controls denote the arity of nodes i.e. ports number, which of these nodes are atomic i.e. empty nodes, and which of the non-atomic nodes are active, i.e. subject to reactions, or passive. Sites modeled by grey squares are considered as an abstraction indicating the presence of other nodes which represents hidden parts of the model. The inner/outer names of a bigraph are links or potential links to other bigraphs. By convention, inner/outer names are drawn above or below the bigraph (e.g. x0 and y0 in Figure 1).

In addition to their rich graphical representation, a term algebraic language resembling traditional process calculi is defined to encode bigraphs. The language primary elements and operations for composing elementary bigraphs are listed in Table 1. For instance, the parallel product U ||V term may be used to compose bigraphs by juxtaposing their roots and merging their common names. The merge product term U |V allows juxtaposing two bigraphs and merging their regions into a single one. As an additional example is the nesting operation U.V which denotes a bigraphical term placed inside another one. The barren (empty) region Bigraph Definition. A bigraph is formally defined by G = (V, E, ctrl, G P , G L ) : I → J, where V and E are respectively finite sets of nodes and edges. ctrl : V → K is mapping function associating a control to each node in the bigraph G. K referred to as the bigraph signature is its set of controls. G P = (V, ctrl, prnt) : m → n is the place graph of G. m and n are respectively the number of sites and regions, prnt : m V → V n is a mapping function that identifies the parent of each node. G L = (V, E, ctrl, link) : X → Y represents the link graph of the bigraph G, where link : X P → E Y i is a link map, X and Y are respectively inner and outer names. P is a set of ports of the bigraph G. I = m, X and J = n, Y are respectively inner and outer interfaces of the bigraph encoding the potentiality of G to interact its external environments. Sorting Discipline. A bigraph can be further associated with a sorting discipline allowing to classify the different bigraphical terms specified in the bigraph such as nodes, links and sites. This sorting logic helps as well as defining the necessary constraints on the designed bigraphs. A sorting discipline Σ is a triple Σ = {Θ, K, Φ}, where Θ is a non empty set of sorts. K is the bigraph signature, and Φ is a set of formation rules associated with a bigraph. The latter consists of a set of structural constraints a bigraph has to satisfy. Note that disjunctive sorts are written as xy which means a node can either be of sort x or y. Bigraphical Reaction Rules. Dynamic behavior in terms of system evolution is defined in BRS via rewrite rules, called bigraphical reaction rules. A reaction rule R(p) = (R, R ) consists of a pair of bigraphs referred to as redex and reactum and can be written by R → R . The redex on the left-hand side represents the parts of a bigraph to be altered, while the reactum on right-hand side specifies how those parts are altered. The transition is triggered on a bigraph G when R has an occurrence or a match in G. The result of the rule application is a new bigraph G obtained by inserting R in G to replace R .

Bigraphical Model of Fog Systems

In this section, we formally define bigraphs used to specify a Fog system in our model. We describe the way sorted bigraphs are used to capture the semantics of such systems. The model is extended via parametric reaction rules explaining the evolution of a Fog system over time and modeling self-adaptation.

Formalizing Fog Systems

A Fog-based system is modeled in our approach by a bigraph F S composed of the parallel product of two elementary bigraphs representing the Fog and Cloud layers. The parallel product term usage characterizes our model by a genericness and extendability, making it easily scalable and modifiable. This bigraphical term offers the possibility to include additional bigraphs representing the external environment as other Cloud or Fog service providers and thus an ability to represent different systems architectures (e.g. federation of Fogs).

The proposed formalization is achieved by associating a precise semantics in the theory of BRS to each Fog architectural element. A Fog system and its two Cloud and Fog layers are formalized via bigraphs. The different Cloud instances and Fog nodes are expressed with bigraphical nodes and the various kinds of interactions are modeled by edges. Sites represent parts of a Fog system that we wish to hide or abstract away. The proposed formalization helps in exemplifying the different parts of a Fog-based system, as well as exposing the conceptual entities involved in such systems' typical architecture 4 . Definition 1. Let F L be a bigraph modeling the Fog layer of a Fog system and CL be a bigraph modeling its Cloud layer, a Fog system bigraph F S is composed by applying the parallel product term on F L and CL (see Equation 1).

F S def = CL F L (1)
Definition 2. A Fog system bigraph is defined formally in our approach by

F S = (V F S , E F S , ctrl F S , F S P , F S L ) : I F S → J F S (2)
-V F S = V F L V CL
is a finite set of nodes of a Fog system F S obtained from the disjoint union of the sets of nodes of the Fog F L and Cloud layers CL.

-E F S = E F L E CL
is a finite set of edges given by the disjoint union of sets of edges of the Fog F L and Cloud CL layers.

-ctrl F S = ctrl F L ctrl CL : V F S → K F S is a control mapping function assign- ing to each node v ∈ V F S of the bigraph F S representing a Fog system, a control k ∈ K F S defining its type. A signature K F S = K F L K CL is
I F S = I F L ||I CL = m F S , X F S , m F S = m F L +m CL and X F S = X F L ∪X CL
is the inner interface of the bigraph F S. m F S is the number of sites and X F S is a set of inner names of F S.

-J F S = J F L ||J CL = n F S , Y F S , n F S = n F L + n CL and Y F S = Y F L ∪ Y CL , is
the outer interface of F S, where n F S and Y F S are respectively the number of regions and the set of outer names of F S.

Modeling Fog Systems with Sorted Bigraphs

We now outline how the structural and conceptual aspects of a given Fog system are encoded through sorted bigraphs. Accordingly, we define a sorting discipline for the class of bigraphs used to describe a Fog system architecture in our model.

A sorting discipline provides the proper semantics to represent faithfully a Fog architecture. Besides, it imposes the necessary structural constraints via formation rules to preserve architectural integrity and ensure bigraphs are designed in a meaningful way. The sorting discipline for the bigraph F S is defined by

Σ F S = {Θ F S , K F S , Φ F S }, where Θ F S = Θ F L Θ CL , K F S = K F L K CL and Φ F S = Φ F L Φ CL
= {SE, SE L , SE U , SE F }, v = {V M, V M L , V M U } and t = {CN, CN L , CN U } represent
respectively different states of a server, virtual machine and container. A service or micro-service is modeled with nodes of sort m = {s}. The various entities computing capacities such as memory, CPU, battery, and storage as well as services requirements in terms of computing resources are encoded respectively by nodes of sort a = {M v , C v , B v , S v } and q = {M r v , C r v , B r v , S r v } where v is parameter recording the value of each kind of node.

Nodes of sort a are always placed in a node having a sort c = {C}. Such nesting condition and other kinds constraints are formalized in the set of formation rules Φ F S with conditions Φ i , 1 ≤ i ≤ 11, listed in Table 3. These formation rules are defined to ensure only bigraphs with meaningful structure can be constructed and thus maintain architectural integrity even after self-adaptations. More precisely, conditions Φ 1 -Φ 2 are constraints on nodes activity. For instance, Φ 2 states that all nodes having a sort lnsvtmc are active, which means they are subject to reactions. Formation rules Φ 3 -Φ 9 are conditions on nodes placing. An example of this kind of nesting rule has been given above. Finally, conditions Φ 10 -Φ 11 are linking formation rules. As an example, rule Φ 11 imposes on a node having an m-sort to be connected to nodes of its own sort or to io-names, encoding the bigraph F S ability to interact with the external environment. An example of a graphical form of a bigraph F S encoding a Fog-based system is given in Figure 2. Note that for the sake of simplicity, controls of sorts p, a and r are purposely omitted in the graphical form. The bigraph F S is obtained by composing F L and CL bigraphs representing Fog and Cloud layers using the parallel product operation. In Figure 2 the Fog and Cloud layers are modeled respectively by regions 0 and 1, depicted with dashed rectangles. Region 0 contains several clusters modeled by nodes having controls L1 -L4. A cluster node may be linked to an arbitrary number of other cluster nodes through connection points represented by nodes of control P . These connection points are used to express the neighboring relationship between Fog clusters, such that when two clusters are directly linked to each other, they are considered as direct or one-hop neighbors. For instance, clusters L1 and L2 are considered in our model as direct neighbors, while clusters L2 and L4 are considered as two-hop neighbors. The grey shapes in Figure 2 are sites, used as abstraction for hidden away entities.

Figure 3 is another simple example of a Fog layer bigraph F L modeled with region 0, which shows in depth the structure of a Fog cluster in our model. Sites are used here to abstract away the elements of the bigraphical model that we do not reason about. A Fog cluster L hosts a set a N nodes modelling Fog computing nodes. In the example, nodes of control N 1, N 2 L and N 3 U encode respectively stable, loaded and underused Fog nodes. Each node may host a set of application containers modelled with nodes having control CN . The latter may host themselves nodes of control S, modelling application services. The computing capacity of Fog nodes and containers is encoded with a node of control C, grouping nodes representing their respective memory, CPU, battery level, etc. For instance, the computing capacity of Fog node N 1 represented by a node C within N 1 can be represented by the following algebraic notation: C = C.(M 512 |C 1.1 |B 10 )|d) to express the computing capability of N 1. Finally, service requirements in terms of processing power are encoded in a similar way by nodes taking the shape of small circles within the node of S control. In our example, the service S requirements are expressed algebraically by: S = S fi .(M r 32 |C r 0.1 |B r 0.2 ).

Modeling Fog Systems Self-Adaptation

A bigraphical reactive system consists of a class of bigraphs modelling conceptual aspects of a system and a set of reaction rules encoding their dynamic behavior. The behavioral model consists of a set of parametric reaction rules giving the Fog system model the ability to self-adapt. Each reaction rule correspond to a reconfiguration action triggering a change that rewrites parts of the bigraph F S following the occurrence of a respective self-adaption event of the Fog system. In the following, we present a set of reaction rules modeling self-adaptation actions carried out in a Fog-based system while preserving the defined sorting discipline Σ F S . Due to the space limitation, here we do not give all the reaction rules in our behavioral model, instead, we present some relevant examples. The exhaustive behavioral model includes additional reaction rules such as virtual machine/container migration and replication, node mobility (relocation), turning on/off a node, service deployment, battery draining, tagging an underused or loaded container or virtual machine, etc. Examples of reaction rules defined in the algebraic terms language dedicated to BRS are summarized in Table 4. The first example is a reaction rule which models the establishment of a neighboring relationship between two clusters. On the left-hand side of the rule (redex), the two nodes L and L modelling two Fog clusters are independent of each other and not linked together, meaning that currently, they do not recognize one another as neighbors. On the right-hand side (reactum), two connection points modeled with nodes of control P are created within each cluster node and a communication link l is established between them to represent the new neighboring relationship (see Figure 4.a). Another example of reaction rule for resizing the memory allocated to a loaded or underused computing instance such a loaded container represented by control CN L is presented in Figure 4.b. The rule is employed to modify the memory parameter of the memory node M within a capacity node C from value x to x . We consider the memory increased if parameters x < x and decreased if x > x. Finally, the last example is a reaction rule graphical representation for tagging a node after it fails (see Figure 4.c). The reaction rule principle consists of replacing the node control N on rule's redex by another control N F on the reactum.

Motivating Case Study

A Fog System Architecture

Assume a Fog-based system distributed over a part of a college campus, specifically, a department and a dormitory. The Fog layer contains a number of small size Fog nodes such as cameras, routers and boxes, as well as larger nodes such as Raspberry Pis and small servers. The infrastructure includes, in addition, a more powerful server in the Cloud layer. Consider two smart city Fog applications, designed as a set of micro-services distributed across multiple Fog cluster on different nodes. The first application is a smart surveillance application [START_REF] Nagothu | A microservice-enabled architecture for smart surveillance using blockchain technology[END_REF], proposing a near site Edge/Fog-based solution for video analysis. Micro-service architecture is adopted to decouple the complicated video analysis tasks such as facial features extraction, car recognition and real-time behavior analysis. Five services are dedicated to such tasks, divided into low-level tasks deployed in the smaller nodes of the Edge infrastructure and computing intensive or high-level tasks outsourced to the bigger Fog nodes or to the Cloud. The smart surveillance application is composed of five micro-service, low-level ones: (S1) Feature extraction, (S2) Audio analysis, (S3) Licence plate recognition. High-level services include (S4) Gesture and facial recognition and (S5) Suspicious behavior analysis. The second application in our example is a smart bell application [START_REF] Xia | Combining hardware nodes and software components ordering-based heuristics for optimizing the placement of distributed iot applications in the fog[END_REF], which notifies the college dormitory inhabitants when they receive visitor(s). The micro-services composing the application are classified similarly into low-level and high-level services. The low-level services are (S1) Feature extraction, (S6) Bell ringing decision, and the high-level services are (S4) Gesture and facial recognition, (S7) Visitor habits analysis. Note that some micro-services in the two applications are identical.

The presented Fog-based infrastructure deploying the two Fog applications can be encoded in our model by the formulae below. Due to the space limitation, we give only an abbreviated algebraic form of the example bigraph F S where we abstract away some nodes using sites. The bigraph model encodes essentially three clusters L 1 , L 2 and L 3 containing 12 nodes (N 1 -N 12 ) used to host mostly low-level services S 1 , S 2 , S 3 , S 6 and a high-level service S 4 at the Fog layer (F L). A neighboring relationships exists between clusters L 1 , L 2 and L 2 , L 3 . A Cloud server SE within a CL-bigraph is hosting two of the high-level services S 5 , S 7 . Note that a micro-service can have several instances representing its workers (e.g. S 1 , S 1-1 , etc.) deployed in containers CN 1 -CN 21 and virtual machine V M 1 , V M 2 . In the algebraic representation we occasionally omit some workers and links between services for presentation reasons.

Self-Adaptation Strategies

Concentration of students and various persons such as visitors present at a college campus differ around the year. For instance, during the first and second semesters, more people are expected to be on the campus, while at the holidays very few are there. The estimate of students may as well fluctuate between the semesters since a portion of students usually does an internship outside of the college in the second semester. Besides, the number of people outside of dormitory varies around the day: more people are outdoors in the morning and more are indoors as the day goes by. Considering these different situations, it is obvious that the two Fog applications will have fluctuated workload very often. As computing nodes at the Fog are mostly resources-scarce, occasionally energy-constrained and unreliable, a Fog-based system must possess an ability to self-adapt at run-time in order to better optimize resources consumption, according to the context variation and depending on the workload and nodes availability. Here, we demonstrate the use of our defined bigraphical reaction rules to model self-adaptation strategies, which can be used in such systems in order to get around resources deficiency distinguishing computing nodes at the Fog. These reaction rules can be used to describe all possible evolution scenarios and reachable configurations of a Fog system in terms of self-adaptation in two orthogonal ways to rewrite an F S bigraph: iterative application of each reaction rule at a time and as a sequence of reaction modeling self-adaptation strategies. Assume two self-adaptation strategies controlling the Fog system and applications of our case study. The first strategy operates at the application level to scale out/in the two Fog applications horizontally. It scales out by creating additional workers for their respective micro-services when the demand average peaks and scales in by destroying workers when it drops. Two action plans modeling this adaptation strategy as sequences of parametric reaction rule that updates the bigraph model from a state S n to S n+1 are encoded by formulae (a) and (b). The first action plan AP a contains the reaction for creating additional workers for micro-services S1, S2, S3, S4 and S6, which we consider as the most subject to be affected by the workload augmentation. The action plan AP b contains rules for consolidation the unneeded workers of the aforementioned micro-services when they are unneeded. We use R * to indicate an arbitrary number of applications of a reaction (zero or more).

notation indicates a transition between reaction rules. A rule parameter i is used to model the index of the respective service e.g. add-worker(i), such that in our example 1 ≤ i ≤ 7. The second adaptation strategy concerns vertical resizing of containers hosting instances of the different micro-services. Based on resources consumption level of the hosted instances, the strategy adjusts the size of a given container by allocating to it additional computing resources. In our example, we assume a scenario where the size of a given containers (parameter i is used to determine the concern containers) needs to be adjusted to better accommodate the requirements of their hosted workers in terms of computing power. The reaction rules sequence modelling such strategy which resizes certain containers up or down is given by action plans AP c and AP d of formulae (c) and (d) respectively. The AP c reaction rules sequence allocates additional memory, CPU and storage space to the loaded containers, while AP d scales down the underused ones.

APc def = loaded -container(i) * resize -memory(x, x , i) * resize -cpu(x, x , i) * resize -storage(x, x , i) * (c) APd def = underused -container(i) * resize -memory(x, x , i) * resize -cpu(x, x , i) * resize -storage(x, x , i) * (d)
In a Fog/Edge infrastructure, node failure is a very common phenomenon that may be caused by environmental conditions. In the example of our case study, nodes deployed in open air exposed to rough weather or nodes equipped with intermittent energy sources (e.g. solar panels) such as cameras are typically subject to failure [START_REF] Fang | Issues of using wireless sensor network to monitor urban air quality[END_REF]. In nodes failure scenario, a strategy may be defined to self-adapt a Fog system by replacing the failed nodes with backup nodes or newly installed ones. Node failure event may be modelled with the reaction rules sequence of formulae (e), nodes that get tagged failed in any given cluster would be replaced with backup nodes (if possible) to ensure the two Fog applications continue to be available, especially the safety-critical application of smart surveillance.

APd def = failed -node(i) * add -node(i) * (e)

Constraints and Properties

Now we present how we can employ the notion of bigraphical patterns introduced in [START_REF] Benford | On lions, impala, and bigraphs: Modelling interactions in physical/virtual spaces[END_REF], to express constraints and properties characterizing Fog application requirements and relevant behaviors of self-adaptive Fog systems.

Application constraints. First, we present the formalization of Fog applications specific constraints in terms of state properties. The latter are expressed as predicated via logical formulae obtained by combining bigraph patterns with the basic boolean operators. The different predicates may define constraints on resource requirements, interactions between applications, micro-services placement, etc. These state properties are expected to be satisfied after every Fog system (re)configuration such that if a bigraphical pattern has a match in a given bigraph F S modelling a Fog system, it is considered true. Next, we give two examples of such constraints. Battery constraint. A Fog application may have a requirement specifying that the battery level of nodes on which its micro-services are deployed is not supposed to fall below a minimum threshold. For instance, critical service S4 of both applications in our example, may required a minimum number of hosting nodes to be always available in order to operate correctly. A strategy such as AP e can serve to satisfy this requirement continuously. This constraint is expressed by the predicate Ψ 1 . The constraint is satisfied if the battery level modeled by a control B i v of each node is always above a minimum threshold. N app ⊆ V F S is a set of nodes hosting certain application services.

Ψ1(v, min, i) def = ¬Bi v , such that v < min and i ∈ Napp Application Placement. To ensure secure placement of different application, a Fog system may have a constraint dictating the placement of certain microservices belonging to different applications in different nodes, servers or virtual machines. For instance, a predicate is given below, formalizing a mutual exclusion between micro-services S5 and S7 of the smart surveillance and smart bell applications and their workers to ensure they do not co-existed on the same VM. Behavioral Properties. To express temporal properties over the run-time behavior of Fog systems, it is possible to combine bigraph patterns not just with simple boolean operators, but with more expressive temporal logics such as Linear Temporal Logic (LTL in short) [START_REF] Huth | Logic in Computer Science: Modelling and Reasoning About Systems[END_REF]. Here we formalize relevant behavioral properties of self-adaptive Fog system by integrating bigraph patterns defined over our model as atomic propositions with temporal operators of LTL. For a given atomic proposition φ, we write •φ, φ, ♦φ, φ 1 ∪ φ 2 to denote respectively the temporal operators "next", "always", "eventually" and "until". A temporal property should be true for all possible future evolutions of a Fog system model after the application of bigraphical reaction rules. We present two examples of such temporal properties expressed as LTL formulae. Node replacement. A habitual scenario in a Fog or Edge infrastructure is node failure due to environmental conditions or energy constraints. Thus, to ensure the Fog system stays operational, a failed node should be replaced by a backup or newly installed node. The property specifies the fact that if a node tagged with control N F in our model exists, it will be replaced or repaired. The property can be used to evaluated a node replacing strategy such as AP e . Resource optimization. Because of nodes resource scarcity, a Fog system needs to control resource consumption and better optimize their utilization. For instance, an underused VM should be either used more, consolidated or scaled down in order to better utilize computing capabilities of the hosting server. Such property can validate the efficiency of a horizontal consolidation strategy such as AP b . It is encoded with the LTL formulae below. Informally, it states that it should be always the case if an underused VM exists in the Fog system, i.e. a node tagged with control V M U in our model, eventually it will be in a stable state, consolidated or resized.

Conclusion and Perspectives

Modeling a Fog system spatial distribution and temporal evolution in terms of self-adaption requires an adequate formal foundation that captures such aspects and allows automated computation and analysis of properties. In this paper, we have demonstrated how BRS can present a suitable formalism to structurally and behaviorally model Fog-based systems. Our primary motivation is to concentrate on proposing an extendable formal model capable of representing faithfully self-adaptive Fog systems and related properties. Beyond this scope, formal verification of the presented Fog systems spatio-temporal properties is an important perspective of ours, which we intend to address with the appropriate attention. Our aim is to employ the proposed model as a basis for reasoning about various properties including the ones given above using high-level automated formal analysis techniques. The proposed reaction rules can be applied to generate a sequence of bigraphical models representing past and current states of the Fog system. After every each adaptation, the resulting models can be checked whether certain properties are maintained or violated in the current configuration.

We are considering two kinds of formal analysis approaches: (i) real-time verification of state properties expressed via bigraph patterns such as Fog applications requirements and constraints, (ii) offline model-checking of temporal properties over the behavior of a Fog system. The idea is to construct a framework allowing not only to evaluate self-adaptation strategies by detecting prop-erties violation rate in each strategy but also to identify conflicting ones and report details. In the real-time verification approach, it is possible to use a real Fog system (or a simulator) generating self-adaption events that trigger the application of reaction rule sequences. When applied, the latter would rewrite the current bigraphical model to yield a new state that reflects the actual configuration of the system. State properties can be checked after each self-adaption over the most recent model to verify their satisfaction or violation. The offline verification approach can be employed at the early stages of a Fog system design or at the application deployment time. The objective is to obtain formal assurance about the system through model-checking of temporal properties to verify the absence of unwarranted system behaviors. The model-checking technique is based on a temporal logic which allows reasoning over different computation paths to explore all possible states of the system. This feature provides better coverage but is more computationally expensive, which makes it more suitable for the offline approach rather than for the real-time one (i.e. high analysis overhead).

Fig. 1 .

 1 Fig. 1. Anatomy of a bigraph.

  the set of controls defined for F S. -F S P = F L P ||CL P is the place graph of F S obtained by the parallel product of place graphs of the Fog layer F L and Cloud layer CL. -F S L = F L L ||CL L link graph of F S consisting of the parallel product of the link graphs of F L and CL. -

  . The controls of the set K F S we use to represent a Fog-based system listed in Table 2 are organized into different sorts of the set Φ F S . In greater details, sorts l = {L} and p = {P } contains controls used to model node clusters L and the connection points between them, representing their neighboring relationship. The controls of sort n = {N, N L , N U , N U } encode a Fog node in its different possible states. Following the same principle, sorts s

Table 3 .Fig. 2 .

 32 Fig. 2. A simple example of a bigraph F S.

Fig. 3 .

 3 Fig. 3. Example of bigraphical representation for a Fog cluster.

def=

  Li.(d)|Lj.(d)|id → Li.(Pl|d)|Lj.(Pl|d)|id addnode(i) def = L.(d)|N.(d)|id → L.(Ni.(d)|d)|id replicatevm(i) def = VMi.(d)|id → VMi.(d)|VMj.(d)|id consolidatevm(j) def = VMi.(d)|VMj.(d)|id → VMi.(d)|id resizememory(x, x , i) def = CNLi.(C.(M x |d)|d)|id → CNLi.(C.(M x |d)|d)|id resizecpu(x, x , i) def = CNLi.(C.(C x |d)|d)|id → CNLi.(C.(C x |d)|d)|id failednode(i) def = Ni.(d)|id → NFi.(d)|id

Fig. 4 .

 4 Fig. 4. Reaction rules for (a) Establishing neighboring relationship (b) Resizing memory (c) Tagging a failed node.

FSdef=

  /l1/l2/f1/f2/f3/f4 FL||CL FL def = (L 1 .(Pl1|d)|L 2 .(Pl1|Pl2|d)|L 3 .(Pl2|d) L 1 def = (N 1 .(CN 1 .(S 2 .(d)|d)|CN 2 .(S 2-1 .(d)|d)|d)|N 2 .(CN 3 .(S 2-2 .(d)|d)|CN 4 .(S 2-3 .(d)|d)| CN 5 .(S 3 .(d)|d)|d)|N 3 .(CN 6 .(S 3-1 .(d)|d)|CN 7 .(S 3-2 .(d)|d)|d)|N 4 .(CN 8 .(S 3-3 .(d)|d)|d)|d) L 2 def = (N 5 .(CN 9 .(S 1 .(d)|d)|CN 10 .(S 1-1 .(d)|d)|CN 11 .(S 1-2 .(d)|d)|d)|N 6 .(CN 12 .(S 1-3 .(d)|d)|CN 13 . (S 1-4 .(d)|d)|d)|N 7 .(CN 14 .(S 4 .(d)|d)|CN 15 .(S 4-1 .(d)|d)|d)|d) L 3 def = (N 8 .(CN 16 .(S 1-5 .(d)|d)|d)|N 9 .(CN 17 .(S 1-6 .(d)|d)|d)|N 10 .(CN 18 .(S 1-7 .(d)|d)|CN 19 .(S 6 . (d)|d)|d)|N 11 .(CN 20 .(S 6-1 .(d)|d)|d)|N 12 .(CN 21 .(S 6-2 .(d)|d)|d)|d) CL = SE1.(VM1.(S 5 f2 .(d)|S 5-1 f2 .(d)|S 5-2 f2 .(d)|d)|VM2.(S 7 f4 .(d)|S 7-1 f4 .(d)|d)|d)

=

  addworker(1) * addworker(2) * addworker(3) * addworker(4) * addworker(6) * (a) APb def = releaseworker(1) * releaseworker(2) * releaseworker(3) * releaseworker(4) * releaseworker(6) * (b)

5 )

 5 ∧ ¬VMx.(S i 7 )) ∨ (¬VMx.(S i 5 ) ∧ VMx.(S i7))

  .(NyF|d) → ♦(Lx.(Ny|d)))

  Ψ4(x, y, v, v , w, w ) def = (SEx.(VMyU.(M v |C w |d)|d) → ♦((SEx.(VMy.(d)))∨ (SEx.(VMy.(M v |C w |d)|d)) ∨ (SEx.(d))

Table 1 .

 1 Terms language for bigraphs.

	Term	Signification
	U ||V	Parallel product
	U |V	Merge product
	U.V	Nesting (U contains V)
	Kx	Node of type (control) K having a name or link x
	id	Identity or elementary bigraph
	di	Site numbered i
	1

Table 2 .

 2 Controls and sorts used in a bigraph FS.

	Meaning	Control	Arity Sort	Bigraph	Notation
	Cluster	L	0	l	F L	Large box
	Connection points	P	1	p	F L	Small square
	Stable node	N	0	n	F L	Rounded box
	Loaded node	NL	0	n	F L	Rounded box
	Underused node	NU	0	n	F L	Rounded box
	Failed node	NF	0	n	F L	Rounded box
	Stable server	SE	0	s	CL	Rounded box
	Loaded server	SEL	0	s	CL	Rounded box
	Underused server	SEU	0	s	CL	Rounded box
	Failed server	SEF	0	s	CL	Rounded box
	VM stable	V M	0	v	F L,CL	Rounded box
	VM loaded	V ML	0	v	F L,CL	Rounded box
	VM underused	V MU	0	v	F L,CL	Rounded box
	Stable container	CN	0	t	F L, CL	Rounded box
	Loaded container	CNL	0	t	F L, CL	Rounded box
	Underused container	CNU	0	t	F L, CL	Rounded box
	Service or micro-service	S	2	m	F L, CL	Circle
	Entity capacity	C	0	c	F L, CL	Medium Box
	Capacity values	M v , C v ,...	0	a	F L, CL	Small circle
	Requirement values	Mr v , Cr v ,...	0	r	F L, CL	Small circle

Table 4 .

 4 Reaction rule examples for the bigraph F S

	Reaction rule	Algebraic form
	neighbor -link(i, j)

In order to keep the definition succinct, we omit the complete formal definitions of Fog and Cloud bigraphs, as they can be redundant.