Sébastien Valette
email: sebastien.valette@creatis.insa-lyon.fr

Yun-Sang Kim
email: kim@creatis.insa-lyon.fr

Rémy Prost
email: remy.prost@creatis.insa-lyon.fr

THE INVERSE PROBLEM OF WAVELET SCHEME CONSTRUCTION FOR IRREGULARLY SUBDIVIDED 3D TRIANGULAR MESHES

We investigate a recent mesh subdivision scheme, allowing multiresolution analysis of irregular triangular meshes by the wavelet transforms. We consider the wavelet scheme construction in terms of an inverse problem. Some experimental results on different meshes prove the efficiency of this approach in multiresolution schemes. In addition we show the effectiveness of the proposed algorithm for lossless compression.

INTRODUCTION

Multiresolution analysis of 3D objects is receiving a lot of attention nowadays, due to the practical interest of 3D modelling in a wider and wider range of applications and in particular in artificial vision. Multiresolution analysis of these objects gives some useful features : several levels of details can be built for these objects, accelerating the rendering when there is no need for sharp details, and allowing progressive transmission. Another feature is that multiresolution analysis can be an efficient way for data compression. A survey of the existing methods used to simplify meshes which is the first step for processing multiresolution analysis, like vertex decimation [START_REF] Soucy | Multiresolution surface modeling based on hierarchical triangulation[END_REF], edge contraction [START_REF] Hoppe | Progressive meshes[END_REF] and wavelet based analysis [START_REF] Lounsbery | Multiresolution Analysis for Surfaces of Arbitrary Topological Type[END_REF], was reported in [START_REF] Heckbert | Survey of polygonal surface simplification algorithms[END_REF]. We put our attention on the third method, because wavelets are well-suited for multiresolution analysis. In section 2, we will shortly explain multiresolution analysis of meshes [START_REF] Hoppe | Progressive meshes[END_REF], and show its drawbacks in practical implementation, which we extend for irregular triangular meshes. Based on a recent work [START_REF] Valette | A multiresolution wavelet scheme for irregularly subdivided 3D triangular mesh[END_REF] we consider the inverse problem of the wavelet scheme construction in section 3. In section 4, we show why our proposal is suitable for compression. Section 5 gives the results obtained with this new scheme.

LOUNSBERY'S WAVELETS BASED MULTIRESOLUTION SCHEME

In wavelets decomposition, a mesh (for example a tetrahedron, see figure 1 for each resolution level j .

Reconstruction is done with two synthesis filters j P and

j Q . Let us call j C the 3 × j v
matrix giving the coordinates of each vertex of the mesh at the resolution level j . Then we have :

1 1 . + + = j j j C A C (1) 1 1 . + + = j j j C B D
(2)

j j j j j D Q C P C . . 1 + = + (3) j D represents the wavelet coefficients of the mesh, necessary to reconstruct 1 + j C from j C .
From a theoretical point of view, each column of the j P matrix (respectively the j Q matrix) represents a scaling function (respectively a wavelet function). These functions are defined on a 3D space fixed by the mesh topology. We apply the lifting scheme [START_REF] Sweldens | The Lifting Scheme : A Custom-Design Construction of Biorthogonal Wavelets[END_REF] which consists in constructing wavelet functions, starting from the hat function, orthogonal to the scaling functions which are hat functions too, but with a twice wider support. Without the lifting scheme, Lounsbery's multiresolution analysis would simply consist in subsampling the mesh (these wavelets are known as "lazy" wavelets), but with the lifting, the mesh at resolution level j is ensured to be the best approximation in the mean square sense for the mesh at level j+1. The main material for the lifting is the inner product between two functions defined by Lounsbery as:

∑ ∫ ∆ ∈ ∈           >= < ) ( ). ( ). ( ) ( , M s j ds s g s f area K g f τ τ τ (4) ) (M ∆
is the set of triangles τ of the mesh and j K is a constant for a given resolution level j . (

j j K - = 4
). Note that in this inner product it is assumed that the triangular faces of the mesh have the same area. The consequence of this assumption is that a mesh at resolution level j will effectively be the best approximation of the mesh at level 1 + j only if this constraint is fulfilled.

Proc. QCAV2001, Le Creusot, France, 21-23 May 2001, vol. 2, pp. 452, 457 Wavelets give a powerful tool for multiresolution analysis of surfaces. However, in the simplification process, the major drawback is that faces are always merged four to one to have a simpler mesh. If the mesh does not respect this connectivity constraint, one has to process a resampling of the mesh, known as remeshing, which results in a mesh having more faces than the original, as explained in details in [START_REF] Eck | Multiresolution Analysis of Arbitrary Meshes[END_REF] and [START_REF] Khodakovsky | Progressive Geometry compression[END_REF]. The aim of this work is to solve this problem by improving the subdivision process, as described in the next section.

A PROPOSAL FOR IRREGULAR MULTIRESOLUTION ANALYSIS

A. Avoiding the remeshing step

The aim of this paper is to provide a new method allowing to process multiresolution analysis directly on irregular meshes, avoiding the remeshing step, as shown in figure 2. This would result in two major improvements in multiresolution analysis on meshes:

-No extra computation is needed (for the remeshing)

-The reconstruction of the mesh can lead to a mesh identical to the original mesh. This allows a lossy to lossless encoding scheme for meshes.

Applying the multiresolution scheme on irregular meshes requires the modification of the two main steps: -The subdivision step, which gives the relation between the different level meshes (connectivity)

-The analysis-synthesis step, where the vertices coordinates of the lower resolution mesh and the wavelet coefficients are computed (geometry) These two modifications are described in details in the two next sections.

B. Modeling irregular subdivision scheme is an inverse problem

In the regular multiresolution scheme, the connectivity of all different level meshes depends on the lowest level mesh connectivity. Then the highest resolution level mesh connectivity has to be highly regular. Unfortunately, classically built meshes (e.g. meshes built with the marching cubes algorithm [START_REF] Lorensen | Marching Cubes: A High Resolution 3D Surface Construction Algorithm[END_REF]), are not regular and can not be directly used.

As a result, the subdivision scheme has to be changed, in order to allow every mesh to be processed. Based on [START_REF] Valette | A multiresolution wavelet scheme for irregularly subdivided 3D triangular mesh[END_REF] we propose an enhanced subdivision process, where the subdivision differs from a face to another one.

In our scheme, each face of a mesh can be subdivided in four, three or two faces, or remain unchanged. Figure 3 depicts the possible cases of subdivision for one face.

The direct problem

Taking a mesh j M having j n faces and j v vertices, we call j S a subdivision scheme applied on it, represented by the a row vector j s containing j n elements (integers between 1 and 11), and describes the subdivision case for each face:

      = j n j p p p s ....

M

is then the result of the subdivision process:

1 + → j S j M M j (5)
We define the efficiency ratio j r as:

j j j n n r 1 + = (6)
Note that:

4 1 ≤ ≤ j r ( 7
)
There are i n 11 possible subdivision schemes, but not all of them lead to a manifold mesh, as shown in figure 4 : The subdivision of the two faces in figure 4-a) results in a manifold mesh, but the in figure 4

S

satisfying:

J J J M M S = - - ) ( 1 1 (8)
This is a blind inverse problem. We can say that for any manifold mesh J M , there always exist one mesh 1 -J M and one subdivision scheme 1 -J S satisfying this constraint. One evident solution is the identity subdivision scheme [ ]

1 ... 1 1 = ident s
, which leaves the entire mesh unchanged:

J J ident M M S = ) ( But ident S
is not an interesting solution, resulting in The algorithm stops when no more faces have to be merged. In order to prevent the algorithm from being unable to merge some faces with respect to the manifold constraint, a modification of the mesh is allowed. It consists in an edge swapping between two neighbour faces, as shown in figure 7. Of course this modification has to be stored, to recover the original mesh after subdivision and guarantee the reversibility of the simplification process. We notice that this modification will introduce a supplementary quality loss during multiresolution analysis, but the difference between the original mesh and the altered mesh is small and experimental results show that this local error is negligible compared to the approximation error. Finally, the algorithm is very efficient for simplifying a large set of meshes.

C. Filter-bank construction

The last thing to do is to compute the approximation of the high resolution mesh with the simplified one that is to calculate the analysis filters j A and j B . This can be done with Lounsbery's scheme. A difference has to be noticed, due to the change of the subdivision process. The inner product [START_REF] Valette | A multiresolution wavelet scheme for irregularly subdivided 3D triangular mesh[END_REF] has to be reformulated and becomes:

∑ ∫ ∆ ∈ ∈           >= < ) ( ). ( ). ( ) ( ) ( , M s j ds s g s f area K g f τ τ τ τ (9)
K j (τ) is no longer a constant and changes with each face of the mesh. For example, a face in a low resolution mesh that will split in 3 faces will have K j (τ)=3 and the three resulting faces will have K j+1 (τ)=1, taking into account the differences between the triangle areas : the first face cited above will approximately be three times larger than the three last.

COMPRESSION

A. Compression efficiency

The proposed method has powerful features for compressing meshes, for two reasons:

• The wavelet decomposition, used to compute the vertices coordinates, transforms coordinates into wavelet coefficients which histogram is concentrated around the zero value, making them well suited for entropy coding. • Starting from the lowest resolution level, there is no need to store or transmit the faces descriptions to reconstruct higher levels, only the subdivisions have to be, which lets the amount of information needed to reconstruct the connectivity of the mesh close to 2 bits per face. In the experimental results section, the lowest resolution mesh is not compressed.

B. Lossless compression of the vertices coordinates

Here we consider vertices with integer coordinates in order to perform lossless compression. In addition, a number of rounding operations have to be introduced in the multiresolution analysis-synthesis scheme. For a brief demonstration, one shall come back to the construction of the matrix filters Q as the "lazy" filterbank. These filters do not perform any approximation, since during the analysis (where some vertices are removed, as the mesh is simplified) the coordinates of the remaining vertices stay unchanged. An integer-to-integer intermediate analysis-synthesis scheme can be defined as: where  . and  . are respectively the floor and ceiling operators, and ensure perfect reconstruction, as described in [START_REF] Jung | Lossless Subband Coding System Based on Rounding Transform[END_REF].

G1 G2 G3 G6 G5 G4 a) b) c) d) Proc. QCAV2001,
The approximation-effective filter-bank directly derives from the "lazy" filter-bank modified by the lifting scheme:

P Q Q α ( 16
)
where j α is a ) ( 1

j j j v v v - × +
matrix chosen to ensure the best possible approximation. By replacing j A by its definition [START_REF] Taubin | Geometric compression Through Topological Surgery[END_REF], equation ( 1) becomes :

j j j ermediate j D C C . 1 int + + = α (17)
An integer-to-integer analysis scheme can now be defined as explained in [START_REF] Calderbank | Wavelet Transforms that Map Integers to Integers[END_REF]:

  1 1 . + + = j j lazy j C B D (18)   j j j j lazy j D C A C . . 1 1 1 + + + + = α (19)
The corresponding inverse is :

  ( )   j j lazy j j j j j D Q D C P C . . . 1 1 + - = + + α (20)
Equations ( 18), ( 19) and (20) now give the integer-tointeger version of the multiresolution wavelet scheme defined in (2), ( 3) and ( 4). This scheme can be used for lossless compression as shown in the next section.

RESULTS

We show in this section the results obtained with the proposed algorithm on two different meshes:

-One mesh (Figure 8), which is a part of the internal structure of a human bone, which has a complex and thin shape. It was build with a method described in [START_REF] Lotjonen | A triangulation method of an arbitrary point set for biomagnetic problem[END_REF]. The algorithm constructed 24 resolution levels with this mesh. The lossless compression ratio obtained is R=6.0 .

-One mesh (figure 9), which has been build with the marching cube algorithm [START_REF] Lorensen | Marching Cubes: A High Resolution 3D Surface Construction Algorithm[END_REF], and which connectivity is highly irregular. 25 resolution levels were built.

The lossless compression ratio is here R=7.92 .

The algorithm was able to simplify both meshes to the simplest existing mesh : the tetrahedron (4 faces and 4 vertices).

Notice:

-Though the first mesh has much less faces than the second one (1084 vs 9478), the algorithm built 24 levels of resolutions for the first one and only 25 for the second one, because of the shape complexity of the bone structure mesh. This can also explain the difference in lossless compression efficiency.

-During the firsts resolution levels (from 0 to about 10) not much faces are created during the successive subdivision steps. As a result, i r is very low for these levels, resulting in a poor compression ratio for the firsts levels. One way to have a better compression ratio would be to first encode a mesh with middle complexity (e.g. at level 15 for the two considered meshes) with a method such as proposed in [START_REF] Taubin | Geometric compression Through Topological Surgery[END_REF], as the proposed algorithm is not very efficient with these very simple meshes (i.e. from level 0 to level 15). We proposed the enhancement of the new scheme [START_REF] Valette | A multiresolution wavelet scheme for irregularly subdivided 3D triangular mesh[END_REF] allowing to process multiresolution analysis on arbitrary meshes. In sharp contrast with [START_REF] Lounsbery | Multiresolution Analysis for Surfaces of Arbitrary Topological Type[END_REF] and [START_REF] Eck | Multiresolution Analysis of Arbitrary Meshes[END_REF] where a resampling of the original mesh is necessary, our scheme processes directly on the original mesh. The irregular multiresolution scheme is an inverse problem. The proposed method has many potential applications such as mesh compression, progressive transmission and fast rendering of 3D images.

  .a) is quaternary subdivided (figure 1.b) and deformed (figure 1.c), to make it fit the surface to be approximated. Subdividing the mesh consists in splitting each triangular face into four faces. These steps can be processed depending on the required resolution levels. a) b) c) Figure 1: the subdivision scheme Multiresolution analysis is computed with two analysis filters j A and j B

Figure 4 :

 4 Figure 4: The manifold constraint

1 - J r equal to 1 .

 11 In a coding efficiency purpose, one shall find a subdivision leading to a number of faces possible.

Figure 5 Figure 3 :Figure 5 :

 535 Figure 5 shows an example, where 15 faces are reduced to 6, resulting from merging 4 :1 faces for G2, 3 :1 faces for G3 and G6, 2 :1 faces for G1 and G4 and keeping one face unchanged for G5. For this subdivision scheme, 5 . 2 6 15 1 = = -J r .

Figure 6 :

 6 Figure 6: expansion of the simplified face set

Figure 7 :

 7 Figure 7: an edge swap between two faces

First

Figure 8 :

 8 Figure 8 : results on a complex shape mesh

  Le Creusot, France, 21-23 May 2001, vol. 2, pp. 452, 457

	C	int j	ermediate	=	1 + lazy j A	1 . + j C	(10)
									D	j	=	 B	1 1 . + + j lazy j C		(11)
			C	j	1 +	=	 P lazy j	j . int C	ermediate	+	Q	j lazy	D .	j		(12)

This work is in the scope of the scientific topics of the GdR-PRC ISIS research group of the French National Center for Scientific research.


Matteo Bordin

Cyrille Comar

Ed Falis

Franco Gasperoni

Yannick Moy
email: moy@adacore.com

Elie Richa
email: richa@adacore.com

Jérôme Hugues
email: jerome.hugues@isae.fr

System to Software Integrity: A Case Study

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

It is widely acknowledged that the main source of cost for developing high-integrity software systems is their verification. A significant portion of this verification cost is spent assessing that software complies with its requirements.

Over the years several different methods have been developed to address this issue, in particular: testing, peer reviews, formal verification and automatic code generation. It is more and more frequent that these verification strategies are mixed within the same system, so as to adopt the most appropriate one for each component. This increases the complexity of the integration phase because it has to cope with multiple formalisms, development and verification methods.

Our goal is to propose a pragmatic process to integrate components developed using different methods into a single system and demonstrate that properties already verified for each component in isolation are preserved in their composition. This process leverages AADL as a pivotal modeling language for system specification and relies on specific verifications between the latter and the components developed using heterogeneous modeling and programming languages, namely Simulink for computation intensive parts and Ada/SPARK 2014 for other components.

Our paper proceeds as follows. First we provide a high-level overview of our approach and enumerate the current methods for addressing the property preservation problem. Then we illustrate practically our approach using the Nose Gear Challenge problem, a simplified yet complete example of a high-integrity real-time system. We then conclude by comparing our approach to the state of the art.

Overview of our approach

The core problem we address in this paper is the assessment of property preservation when integrating heterogeneous components. Regardless of the safety standard of reference, the term "property" indicates a specific refinement level of requirements: properties may be system requirements, software requirements, high-level requirements (HLR), low-level requirements (LLR) and so forth.

Complex systems are built using a mixture of a top-down and bottom-up approach. In a top-down approach, the system is decomposed into atomic components which are then developed in isolation and integrated. In a bottom-up approach, existing components are adapted to be reused and integrated in a complete system.

When adopting a top-down approach, properties can be violated when the implementation does not correctly implement its specification. For example, a Simulink model may not guarantee the computational precision required by system specifications. To avoid this problem, we propose to represent the system architecture and all its constraints in the form of AADL models entities, completed with annex language such as REAL or BLESS . The system is decomposed into atomic components and each component is developed using the 2 most appropriate technology, for example Simulink or SPARK 2014. At this point it is fundamental to translate downwards the system constraints in the implementation language. For example, REAL constraints can be translated into Simulink assertion blocks or into SPARK 2014 contracts. This property translation process guarantees that all system properties are allocated and verified on the atomic components. The property translation continues until a property is verified: for example, a constraint can be verified by simulation in Simulink, and if such verification is not deemed sufficient, the property can be translated to SPARK 2014 and formally verified on the SPARK code.

When adopting a bottom-up approach, properties may be violated when sibling components do not respect their mutual interface contracts. For example, a control algorithm requiring a 20Hz execution rate may be integrated in a real-time architecture unable to guarantee such a property. To avoid this problem, we propose to formalize in AADL all the relevant properties of the components being integrated. We are interested in properties that are relevant from a system perspective, both implicit and explicit. For example, a Simulink algorithm implicitly assumes that its persistent data is not changed between two consecutive computations. Likewise, a SPARK program explicitly states its system-relevant contracts in the top-level module. Once the properties have been extracted, the pivotal AADL model can be used to verify the correctness of the integration of atomic components.

The two approaches are summarized in the following picture:

Before proceeding with our paper, we would like to highlight that our approach works only when using languages providing design-by-contract facilities. This is of course the case of Simulink (assertion blocks) and SPARK 2014. However, other languages present similar features: UML can use OCL constraints and C can be decorated with ACSL contracts. We chose to consider Simulink and SPARK because Simulink is the From now on, we will concretely show how properties can be translated between different languages and abstraction levels, and we will discuss the level of automation attainable with currently available tools.

Related work

Regardless of whether the development follows a bottom-up approach, a top-down approach or a mix of both, one core activity is the low-level verification of components in isolation, that is the verification that source code correctly implements its specifications. In this section, we list six different ways to achieve this goal. We provide this list upfront to better position our approach with respect to the current state of the art.

Peer review

This approach is the classical one and consists of having an experienced person review the specification and implementation looking for pitfalls and errors. This static verification is typically manual but can be supported by appropriate verification tools such as CodePeer . This approach is easy to deploy, but quite costly and 4 error-prone, as it relies on manual labor.

Extensive testing

Testing is a dynamic form of verification that infers correctness of the implementation by checking that the compiled executable behaves as expected with respect to an oracle. The oracle may be manually produced. However, if the specification is executable, the oracle may be produced by executing the specification with a set of test data and checking that the implementation produces the same output. A typical example of the latter is comparing Simulink simulation with the behavior of its source code translation. Another example is checking compiled contracts dynamically during the testing of the executable. Testing is relatively easy to deploy, but it cannot of course be extensive.

Qualified automatic code generation

This approach consists in the automated production of the implementation of a component from its specification, such as the automatic generation of a C language implementation from a Simulink control algorithm. In this case, the correctness of the implementation is inferred from the correctness of the code generation itself. The latter is verified once and for all as a COTS tool. Depending on the safety standard of reference, this verification may be lightweight or extremely costly. Examples of such qualified code generators are SCADE KCG and the Simulink code generator developed within the FUI project Project P 5 (GNAT Pro Simulink). The main advantage of this approach is the low-cost of the verification activities across various projects once the code generator is qualified.

Formalize requirements as source code contracts

This approach consists of formalizing the requirements using elements of the lower level abstraction (source code) and verifying the consistency between the formalized requirements and the source code, either statically or dynamically [ARTIFACT]. It is the approach used in the Unit Proof methodology at Airbus [AIRBUS] and the SPARK contract-based verification technology [SPARK_CASE_STUDY]. Low-level requirements are expressed as subprogram contracts (typically preconditions and postconditions), and the source code is verified against these contracts, either through testing or through formal verification, or a mix of both [TEST_AND_PROOF].

Translation of contracts across different abstraction levels

This approach consists of expressing the same property at different levels of abstraction and verifying it at every abstraction level. It is the approach used in this paper when translating Simulink assertion blocks (observers) into SPARK contracts. The benefit of performing the verification at each level is that errors in the (automatic or manual) translation of the software can be detected at the lower level. The benefit of translating the property automatically is that it can be expressed at the most natural level, and still be used at the lower level.

Property extraction

The last verification strategy consists of extracting implicit properties out of an implementation and comparing them against a specification. For example, source code can be reverse-engineered to a formal model, and the formal model can be checked (statically or dynamically) against a set of properties. ADI Beacon uses 6 this approach to reverse-engineer SPARK code generated from Simulink and compare it against the source Simulink model by using traceability information encoded in the source code. The main advantage of this approach is that, in theory, it works a posteriori on any implementation. However, it usually requires dedicated tools which need extensive verification and validation and is limited by the capability of programming languages to express complex specifications.

In the industrial state-of-the-art, the most used approaches are peer review and testing. All other approaches (and testing as well) greatly benefit from a specification written in a computable specification language like AADL, UML, Simulink or SPARK.

Our goal: to improve the integration process

In the previous section, we listed the current state-of-the art for property preservation. Due to the increasing complexity of modern systems and the extensive use of longer supply chains for software components, it is unlikely that the same method is used for all components of a system. The deployment of multiple languages, tools and methods is very attractive because it decreases the development costs of each single component: a control algorithm is better developed in Simulink, while a high-security system is better formally specified and developed in SPARK.

Unfortunately, the use of heterogeneous languages and methods increases the cost of verification. This is the specific aspect we want to tackle in this paper. Our main goal is to demonstrate how we can abstract integration-relevant properties out of each component and use them to verify their integration within a complete system. More concretely, we aim to:

A. Use an AADL architectural model as a pivot element to link components developed using heterogeneous methods and tools;

B. Formalize in the above AADL model the assumptions on which each component relies when it is verified in isolation. These assumptions can be extracted from the atomic components when following a bottom-up approach; and can be translated to the implementation languages when following a top-down approach.

C. Verify that the above assumptions still hold in the composed system.

As explained, this approach is intended to fit both the top-down and bottom-up approaches. The main challenges are:

1. To formalize how to translate integration-relevant properties across languages; and 2. To develop automated tools performing most verification tasks.

To give a practical evidence of our idea, we decided to develop a system whose components are developed using the methods identified in section 3, and in particular:

• Use of qualifiable automatic code generators from Simulink

• Use of contract-based programming with formal verification

• Use of peer reviews and extensive testing.

The system we decided to develop is described in the next section.

The Nose Gear Challenge

The Nose Gear challenge was proposed in 2011 by the organizers of the second Workshop on Theorem 7

Proving in Certification as a small, yet realistic case of a critical system, to demonstrate and compare benefits and limitations of formal methods. The problem is that of computing a simple function that estimates the velocity of an aircraft while moving on the ground. The only information available comes from an interrupt routine which is called each time the wheel completes a full rotation (the "click"). It updates the value of two 16-bit counters called NGRotations and NGClickTime which denote respectively the count of full rotations of the wheel, and the time of the last click. A third 16-bit counter Millisecs updated every millisecond denotes the current time. The following diagram illustrates this behavior:

Two requirements were specified on the system:

1. A flag estimatedGroundVelocityIsAvailable shall be set to true if the velocity has been correctly estimated and to false otherwise. When available, the estimated value of the velocity shall be within 3km/h of the true velocity of the aircraft at some moment within the past 3 seconds.

2. Estimated velocity should be available during taxi, takeoff and landing. We assume the maximum velocity for a typical airliner like the A320 to be at most 200 km/h.

The challenge is to develop a solution to this problem which provides the required assurance that the software developed complies with requirements 1 and 2 above, while at the same time following a strawman certification standard .

8

The original version of the challenge presented above could be developed using just Simulink. In fact, QinetiQ developed in 2011 a solution entirely in Simulink, using a non-qualifiable code generator and a verification tool able to compare the generated code with the Simulink model to formally prove their consistency. To better fit it to our needs, we decided to extend the original scope of the challenge by adding two features to the system :

1. a logging mechanism should store all events and computations of the last 5 minutes.

2. a simple graphical user interface should display the current estimated velocity when it is available and the log of events.

Our solution to the extended Nose Gear challenge consists of:

1. a model of the architecture in AADL;

2. a model of the velocity computation in Simulink;

3. an implementation of the logger in SPARK;

4. an implementation of the GUI in Ada.

Modelling the architecture in AADL

For the ease of discussion, we start by presenting a top-down approach.

We begin by defining the global system architecture using AADL. This language offers inheritance and refinement features that allow us to start with a very abstract representation of the system and refine it step by step as design decisions are made, while preserving information along the process. In this manner it is possible to express high-level properties of abstract components of the architecture early in the design, and keep that information attached to the components throughout the refinement process.

Two modeling stages have been defined.

• Stage 0 represents the interfaces of each block of the system. It is complemented with sequences of subprogram calls modeled using the AADL Behavior annex and BLESS annotations [BLESS] representing invariants deduced from LLR.

• Stage 1 refines the previous model, using AADL inheritance mechanism, turning abstract components into concrete ones (threads, devices) and associating components to execution resources (CPUs, communication buses, etc.).

The source code in Ada is generated from the Ocarina [OCARINA] code generator for AADL. Ocarina targets a reduced middleware that is compatible with the Ravenscar profile for high-integrity concurrent systems.

The static analyzer CodePeer is used to detect all potential run-time errors in the generated code (not the run time library, independently certified), which were manually reviewed. CodePeer generates error messages for all potential run-time errors (including reads of uninitialized data), and warnings for some cases of suspicious constructs (for example dead code). Analysis of the generated code by Ocarina resulted in 30 messages (18 errors and 12 warnings) which were all manually inspected. Half of them were intentional, typically tests always true which is common in generated code, and functions always failing by returning an exception because not yet implemented, but never called. The other half were false positives, where the static analyzer misidentifies a potential problem though lack of knowledge of the execution context, which were easily diagnosed as such.

AADL can be used to store various system metrics, including performance information. We use this mechanism to store relevant information for all LLRs.

Let us recall an interrupt is triggered at every rotation of the wheel. HLR#2 provides a maximum speed for the plane, that can be linked to the maximum number of interrupts to be handled by the CPU hosting the Nose Gear. Using the AADL Constraint Annex [ACL], we can model compatibility relationships between properties of the model, and thus confirm the target CPU is a valid choice for deploying the system. This is depicted in the example below. HLR#1 is concerned with the availability of a result based on interrupts received. Addressing it completely would require physics modeling of the aircraft which we consider to be out of the scope of the tools presented in this paper. To simplify, we state that the velocity estimation shall be available when all the data used for the computation is less than 3 seconds old. This requirement is formalized as a BLESS assertion attached to the calculation component of the architecture. In that assertion N G C l i c k T i m e ( -1 ) refers to the value of N G C l i c k T i m e at the previous activation of the periodic thread.

n n e x A C L { * * t h e o r e m c h e c k _ I T _ R a t e --E v a l u a t i o n H L R # 2 i s m e t f o r e a c h p i n p r o c e

t --e s t i m a t e d G r o u n d V e l o c i t y I s A v a i l a b l e i s s e t t o t r u e i f a n d o n l y i f --t h e s e n s o r d a t a u s e d f o r t h e c o m p u t a t i o n i s n o o l d e r t h a n t h a n 3 0 0 0 m s .

< < h l r _ a v a i l a b i l i t y : : ( e s t i m a t e d G r o u n d V e l o c i t y I s A v a i l a b l e ) i f f ( ( M i l l i s e c s -N G C l i c k T i m e ( -1 ) ) < = 3 0 0 0 ) > > Such a contract requires the full implementation to be verified. Here, we use AADL only to store the contract, and trace it to the corresponding support entity: a Simulink model. We will discharge this contract later.

Modelling the velocity computation in Simulink

The computation algorithm is designed using Simulink. To ensure property preservation, we translate the BLESS formalization into the Simulink model with the help of an Assertion block as depicted in the following diagram. Our goal is to further translate it down to SPARK. The property is verified by simulation in Simulink, by formal proof in SPARK and can be dynamically checked during integration phase because SPARK contracts can be executed as run-time assertions. This approach honours our original idea of translating properties until we are sufficiently sure they truly hold.

The source code in SPARK is generated from the Simulink model by using GNAT Pro for Simulink. A contract for the main procedure Nose_Gear_Comp is generated from the Simulink model as well In this component, property preservation is demonstrated by translating properties across abstraction levels, by automatic code generation and by formal proof. Note that the SPARK toolset currently proves the absence of run-time errors in the implementation of N o s e _ G e a r _ C o m p , but not yet that the postcondition above is respected, due to a current limitation related to the use of modular types in Ada. This limitation is planned to be lifted in the future.

w i t h P o s t = > --@ l l r l l r _ a v a i l a b i l i t y --T h e g r o u n d v e l o c i t y s h a l l b e a v a i l a b l e i f a n d o n l y i f t h e d a t a u s e d f o r t h e --c o m p u t a t i o n i s n o o l d e r t h a

Implementing the logger in SPARK

The logger API consists of two subprograms: a function Log_Content to retrieve the content of the log (say, to display it on a control panel) and a procedure Write_To_Log to add an entry to the log. Only the most recent 600 entries are saved, which corresponds to 5 minutes of logging at a rate of one event every 500 ms.

A detailed functional specification of Write_To_Log was written as a SPARK contract: This contract is expressed as a set of disjoint and complete cases, using the Contract_Cases notation. It was checked automatically against the implementation of Write_To_Log using the formal verification tool GNATprove in the SPARK toolset. By using SPARK for specifying the logger and verifying its implementation, the following formal guarantees are obtained:

p r o c e d u r e W r i t e _ T o _ L o g ( E : L o g _ E n t r y ) --@ l l r W r i t e _ T o _ L o g w i t h C o n t
1. There will not be any reads of uninitialized data at run time.

2. There will not be any run-time errors.

3. The contract of Write_To_Log is respected by its implementation.

Currently, the SPARK toolset manages to prove automatically points 1 and 2 above, but not point 3. This is a temporary limitation of the toolset that is being worked on.

Implementing the GUI in Ada

The GUI was developed in Ada, based on the GtkAda library providing a binding to GTK graphical library. The requirements for the GUI were expressed in natural language, and checked manually. The requirements were that the GUI would display the most recent entries in the log with the most recent at the top and the least recent at the bottom, and the current computed velocity if available. The left panel below shows the appearance of the GUI when the velocity is available, and the right panel the appearance of the GUI when the velocity is not available:

The CodePeer static analysis tool was applied on this code to check for possible run-time errors, and all alarms were manually inspected.

Recap system verification

The following table recaps how we decomposed the complete system and which techniques we used to verify property preservation. The table above demonstrates how different techniques for property verification can be deployed and integrated in the same system while ensuring traceability of property preservation and providing enough confidence that the property truly holds.

We now miss the bottom-up part of our process: showing that the properties verified in isolation on each component still hold in the integrated system. To do this we need to show that assumptions made for the isolated verifications are not violated by the integration, relying on the main integration artifact: the AADL model. This step requires the reverse translation of contracts from SPARK and Simulink to AADL where they are represented as AADL properties and BLESS assertions attached to component interfaces. For example assertions attached to output ports express guarantees ensured for the destination component, and those attached to input ports express assumptions made by the receiver component. Therefore we believe that a model-level analysis [BLESS] can show the compatibility between guarantees and assumptions of sibling components, however this remains to be explored in upcoming experiments.

Tool automation

In the table process above, there are three main steps that require specific support to be automated: translation between AADL and Simulink, between Simulink and SPARK and between AADL and SPARK. All verification within the same language (BLESS assertions, SPARK contracts, Simulink assertion blocks) are already available within their respective development environments. Automating the translation of properties across languages is then a major step toward a fully automated property-preserving process where properties are proved and translated at multiple abstraction layers.

We currently can translate Simulink assertion blocks to SPARK code. Translating Simulink code to SPARK contracts is more complicated, but feasible: we currently support a limited set of blocks and and only scalar datatypes in this context.

As for AADL contracts, we know of no existing tools that translate them automatically to Simulink or SPARK mainly because the BLESS language is relatively recent. Moreover the semantics of BLESS contain notions of time that make the translation potentially difficult -this is part of future work.Yet, current experiments demonstrate code generated from GNAT Pro Simulink can already be integrated in generated code from AADL. Similarly, the extended coverage of Ada by SPARK 2014 allows for a significant coverage of the generated code for ensuring glue code is matching SPARK code expectations.

Conclusion

In this paper, we proposed a pragmatic view to assess property preservation when developing complex systems using heterogeneous languages and integrating existing components.

The approach relies on AADL as a pivot language to express system-level properties and to verify correctness of integration.

In a top-down approach, properties are translated from AADL system models down to software modeling languages (such as Simulink) or programming languages (such as SPARK). Properties are translated until they can be discharged by relying on tools such as provers or qualified code generators.

In a bottom-up approach, integration-relevant properties are extracted from existing components and represented in AADL, where they can be discharged by using BLESS, thus showing that the verification of components in isolation still holds when they are integrated.

In both cases, we need to rely on languages providing design-by-contract facilities: REAL and BLESS for AADL, assertion blocks for Simulink, contracts for SPARK.

The main open point is related to the degree of automation to move from one abstraction level to the other. In a top-down approach, code generators can easily take care of producing an implementation, however, translation of properties is a more complex task. We currently support this translation in a limited form from Simulink to SPARK. No such automation exists yet for BLESS and REAL.

In a bottom up approach the current tool support is lacking many elements: ensuring that AADL generated code can support verification activities for SPARK code (e.g. bounding the number of events, respect of timing invariant, etc). This specific challenge is conceptually similar to an advanced reverse engineering tool and will require more study from our side.

Our future work will then focus on improving the automation of the property translation process, in particular increasing the support for the generation and extraction of SPARK contracts from and to AADL.

  n e _ P r o p e r t i e s : : T a k e o f f _ S p e e d = > 2 0 0 k p h ; P l a n e _ P r o p e r t i e s : : W h e e l _ P e r i m e t e r = > 5 m ; --. . . e n d A i r l i n e r ; s y s t e m i m p l e m e n t a t i o n A i r l i n e r . i s u b c o m p o n e n t s C P U : p r o c e s s o r N o s e g e a r _ C P U { P l a n e _ P r o p e r t i e s : : I T _ P r o c e s s i n g _ T i m e = > 1 u s ; } ; --. . . a

  s s o r _ s e t d o v a r I S R _ W C E T : = G e t _ P r o p e r t y _ V a l u e ( p , " p l a n e _ p r o p e r t i e s : : i t _ p r o c e s s i n g _ t i m e " ) ; s y s : = { s i n S y s t e m _ S e t | I s _ S u b c o m p o n e n t _ O f ( p , s ) } ; v a r S p e e d : = G e t _ P r o p e r t y _ V a l u e ( s y s , " p l a n e _ p r o p e r t i e s : : t a k e o f f _ s p e e d " ) ; v a r W h e e l : = G e t _ P r o p e r t y _ V a l u e ( s y s , " p l a n e _ p r o p e r t i e s : : w h e e l _ p e r i m e t e r " ) ; v a r M a x _ I S R _ F r e q : = ( h e a d ( S p e e d ) / h e a d ( W h e e l ) ) ; --M a x i m u m n u m b e r o f I S R s p e r s e c . c h e c k ( M a x _ I S R _ F r e q * I S R _ W C E T < 1 ) ; e n d c h e c k _ I T _ R a t e ; * * } ; e n d A i r l i n e r . i ;

  t h r e a d V e l o c i t y _ C a l c u l a t i o n f e a t u r e s --. . . a n n e x B L E S S { * * a s s e r

  . The O l d _ N G C l i c k T i m e _ m e m o r y variable used in the contract is a persistent variable storing the value of N G C l i c k T i m e at the previous invocation (i.e. the output of the Unit Delay block).p r o c e d u r e N o s e _ G e a r _ C o m p ( N G R o t a t i o n s : i n U n s i g n e d _ 1 6 ; N G C l i c k T i m e : i n U n s i g n e d _ 1 6 ; M i l l i s e c s : i n U n s i g n e d _ 1 6 ; e s t i m a t e d G r o u n d V e l o c i t y : o u t L o n g _ F l o a t ; e s t i m a t e d G r o u n d V e l o c i t y I s A v a i l a b l e : o u t B o o l e a n )

  n 3 0 0 0 m s . ( e s t i m a t e d G r o u n d V e l o c i t y I s A v a i l a b l e = ( M i l l i s e c s -O l d _ N G C l i c k T i m e _ m e m o r y < = 3 0 0 0 ) ) ;

  r a c t _ C a s e s = > --T h e l o g g e r c o m p o n e n t s h a l l b e a b l e t o a c c e p t a n e w l o g g i n g m e s s a g e . --F o r a n o l d e m p t y l o g , t h e n e w c o n t e n t i s t h e n e w e n t r ya l o n e . ( I s _ E m p t y = > L o g _ C o n t e n t = S i n g l e t o n _ L o g ( E ) , --F o r a n o l d f u l l l o

The work described in this paper has been funded via the FUI 11 project "Project P", FUI 10 project "Hi-Lite" and Artemis project "Safecer".

REAL and BLESS are two AADL annexes for expressing structural constraints on architectural models, these will be merged in one annex language called ACL: AADL Constraint Language.

most widely used modeling language in high-integrity real-time systems and SPARK is the only commercially-supported programming language amenable for our domain of interest and offering design-by-contract.3 http://frama-c.com/acsl.html

http://www.adacore.com/codepeer

http://www.esterel-technologies.com/products/scade-suite/generate/qualified-code-generation

http://www.adi.com/products/b4s

http://www.cl.cam.ac.uk/~mjcg/FMStandardsWorkshop/NoseGear.html

http://www.cl.cam.ac.uk/%7Emjcg/FMStandardsWorkshop/standard.pdf


Marc Boyer

Luca Santinelli

Integrating end-system frame scheduling for more accurate AFDX timing analysis

Keywords: Timing verification, AFDX, Network Calculus, worst-case traversal times, offsets

Avionics systems distributed on AFDX networks are subject to stringent real-time constraints that require guaranteeing the Worst-Case Traversal Time (WCTT) on the network for each of the data flows. Over the last 10 years, since the initial use of Network Calculus in certification, important progresses have bee n made in AFDX timing verification. The maximum pessimism for the latencies is now known to range from 10 to 25% on realistic systems. Further progresses towards more accurate timing analysis can still be made by considering additional temporal information. In this paper, we show that integrating the knowledge of the scheduling of the frames that is done within an end -system in the timing analysis enables to dramatically reduce the WCTT bounds computed by Network Calculus. Indeed, in our experiments perform ed on a realistic configuration provided by Thales Avionics, this technique reduces the WCTT upper bound by 40% on average over all flows. The reason is that the scheduling of the frames shapes the outgoing traffic, reducing thus peaks of load on the outgo ing traffic, which can be accounted for in the timing analysis. Importantly, because the scheduling of the frames within the endsystems is in the scope of the network supplier, unlike the scheduling of tasks done at the application level, the approach presented here does not imply major changes in the design process.

I n t r o d u c t i o n 1.Context of the stu dy

Avionics Full DupleX (AFDX -see [START_REF]Aircraft data network part 7: Avionics Full DupleX switched Ethernet (AFDX) network[END_REF]) is an aeronautic-specific switched Ethernet technology that supports data exchanges among avionics sub -systems with bounded latencies, without requiring the sub-systems to share a common global clock like in TDMA networks. In AFDX, virtual links (VLs) define the unicast and multicast connections there exist between end-systems. The predictable latencies of AFDX can be achieved because the standard enforces appropriate switching mechanisms within the communication switches and because the workload submitted to the network by each sub-system is upper bounded and known in advance. Indeed, to each VL is associated a maximum frame size and a minimum time between the transmission of t wo successive frames of the same VL. This latter quantity is called the Bandwidth Allocation Gap (BAG) and has to take a value that is a power of two in the range 1 to 128ms.

With the increasing amount of critical data exchanged with real -time constraints in on-board aerospace systems, the computation of accurate upper bounds on network traversal times is an industrial requirement. Indeed, it is needed in the certification process to convince the certification authorities that the real-time and safety constraints are met and this should be achieved without over-provisioning the hardware resources.

If, for realistic AFDX networks, it is in practice not possible to compute the exact Worst-Case Traversal Time (WCTT), conservative upper bounds on the WCTT can be computed in reasonable time (a few seconds using state-of-the-art Network Calculus). The accuracy of these bounds is crucial since over-approximation leads to over-provisioning of hardware resources and is a hindrance to system evolutions. Over the la st 10 years, since the initial use of Network Calculus in certification, important progresses have been made in timing verification and the maximum pessimism for the latencies is now known to range from 10 to 25% on realistic systems (see experiments in [START_REF] Boyer | Experimental assessment of timing verification techniques for AFDX[END_REF] for timing verification with Network Calculus and [START_REF] Bauer | Improving the worst-case delay analysis of an AFDX network using an optimized trajectory approach[END_REF] with the trajectory approach).

Contribution and related works

Further progresses towards more accurate timing behavior analysis can still be made by considering additional temporal information. In par ticular, as done in [START_REF] Boyer | Collaboration entre méthode d'ordonnancement et calcul réseau[END_REF][START_REF] Boyer | Combining network calculus and scheduling theory to improve delay bounds[END_REF], taking into account the scheduling of the tasks provides more accurate bounds on the quantity of work that can possibly be submitted to the network, and thus enable to more precisely evaluate the maximum interference that can be suffered by a flow. But in aircraft design, linking network analysis to task scheduling will create strong dependencies and complexity to the global design. The approach presented in this paper is similar in the spirit with the work in [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF][START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF] where AFDX virtual links are desynchronized with offsets so as to better balance network load over time, in a similar manner to what has been done in automotive CAN networks for almost the last 10 years [START_REF] Grenier | Pushing the limits of CAN -Scheduling frames with offsets provides a major performance boost[END_REF]. The approach discussed here do not required a number of assum ptions placed in [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF][START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF] that make those proposals non-practical without changes in the design flow. Importantly, the knowledge of the scheduling of tasks is not needed, and the technique discussed is usable with non-periodic streams as well as with streams with a deadline smaller than their period. The rationale and limitations of existing approaches are further discussed in Section 3. In this study, we show experimentally that integrating the knowledge of the scheduling of the frames that is done within an end-system in the timing analysis enables to importantly reduce the WCTT bounds computed by Network Calculus, up to 40% on average. Importantly, because the scheduling of the frames in an end-system is in the scope of the network supplier, unlike the scheduling of tasks done at the application level, this does not imply major changes in the design process. The ARINC 664P7 specification defines 3 delays [ § 2.1, §3.2.4.1, 8]: the transmission latency, at source and receiver ends, the network latency, and the sum of the latencies in the switches that are crossed. The latency at the receiver end is mainly a technological latency, and is not further discussed here.

D e c o m p o s i t i o n o f t h e e n d -to-e n d l a t e n c y f r o m t h e s e n d i n g t o t h e r e c e i v i n g a p p l i c a t i o n

Network latency

The network latency is the delay inside the network, i.e. the sum of the delays inside the network switches, divided into packetisation at input port (the frame size divided by the link speed), a filtering delay (to reject out-of-contract frames), a switch commutation latency (sum of both must less than 100µs, [ §4.11.13, 8]), and waiting time in the two-level priority output ports that is due to link sharing among flows.

This network latency can typically be upper bounded using the network calculus theory [START_REF] Grieu | Analyse et évaluation de techniques de commutation Ethernet pour l'interconnexion des systèmes avioniques[END_REF] which is a technique used in certification. The evaluation of the network bounds, with the latest advances in network calculus, have been shown to be moderately pessimistic (typically less than 25%) on experiments made on realistic large AFDX networks [START_REF] Boyer | Experimental assessment of timing verification techniques for AFDX[END_REF].

Figure 2: Generic AFDX switch architecture

Source end-system latency

The latency at source starts when an application writes a data in an APEX port. After some UDP/IP handling, an AFDX frame is placed into a sub-VL queue. Sub-VL queues are then multiplexed into the VL queue using a Round-Robin scheduler, knowing that sub-VLs are optional (an APEX port can be directly linked to a VL queue). A traffic regulator is associated to each VL queue. It ensures that there is at least duration of one BAG between any two successive frames. Lastly, a VL scheduler is used to share the network bandwidth between the VLs. This scheduler must also ensure that output flows still respect the per-VL BAG, up to some jitter MAX_Jitter that must be less than 500µs (see §3.2.3 and §3.2.4.3 in [START_REF]Aircraft data network part 7: Avionics Full DupleX switched Ethernet (AFDX) network[END_REF]). That is to say, the time interval between the first bits of two frames of the same VL, with BAG B, must be not less that B -MAX_jitter.

To ensure this constraint, the per-VL scheduler cannot implement a simple FIFO or Round Robin policy. As an illustration, consider the end-system shown in Figure 2 with 3 VLs: two frames m2 and m3 are placed into empty VL queues while frame m1 is being sent. Assume that m2 is sent before m3 (as a result of applying the FIFO or Round Robin policy). Then, m3 is sent after m1 and m2. Let us call t3 this instant. Then, assume that VL3 queues a new frame m'3, with strict BAG respect. Assume also that when m'3 is sent, all other VL queues are empty. Then, if m'3 is sent immediately, the interval between m 3 and m'3 will be less than the BAG. Let t'3 be the time when m'3 is sent. The value t'3-t3-BAG3 is called the jitter. With only three VL, this jitter is always less than 500µs, but with 5 VL of maximal frame size, at 100Mb/s, the condition no more holds. The specification requires also that "if the system has no other data to proceed on this virtual link", the latency must at the source end-system respects MAX_latencyi  BAGi + MAX_Jitter + Technological_latency

It is up to the end-system provider to implement a scheduler that respects these two requirements, on jitter and latency.

M o d e l i n g t h e s e n d i n g e n d -s y s t e m : a s t a te-of-t h e -a r t 3.1 From task schedu ling to data pro duction windows

The AFDX network is a shared resource: several virtual links cross it. While no information is given, one must assume that is it possible for all VLs to send their frames simultaneously. But th e data to be transmitted in the VLs are produced by tasks, and on mono -processor systems, only one task is active at a given time. In [START_REF] Boyer | Collaboration entre méthode d'ordonnancement et calcul réseau[END_REF][START_REF] Boyer | Combining network calculus and scheduling theory to improve delay bounds[END_REF], a system with periodic tasks (with variable execution times) is considered, where tasks send frames only at end of execution (assuming a typical execution model: data acquisition/control computation/actuation), and assuming a static priority scheduler. Under these assumptions, the traffic generated by the tasks (known as "arrival curves" in network calculus theory) is computed, considering all possible executions. To do so, common scheduling analysis must be adapted to consider tasks instances. These papers show, on hundreds of generated configurations, that the burst size at system output decrease s linearly with the number of tasks. Nevertheless, the computation is not propagated through the network, and no evaluation of the impact of the approach on the network delay is given. This study in [START_REF] Boyer | Collaboration entre méthode d'ordonnancement et calcul réseau[END_REF][START_REF] Boyer | Combining network calculus and scheduling theory to improve delay bounds[END_REF] was a theoretical one, and cannot be directly applied to aircraft design: to facilitate the re-use of components and ease system evolutions during the development cycle, it is may not be possible to make assumptions about the scheduling of tasks while designin g the network. Nevertheless, the method in [START_REF] Boyer | Collaboration entre méthode d'ordonnancement et calcul réseau[END_REF][START_REF] Boyer | Combining network calculus and scheduling theory to improve delay bounds[END_REF] is the basis for this study.

Scheduling virtual links with offsets

Another way to reduce the interferences between the flows in the sending end -system and the switches is to desynchronize the flows in such a way as to better uniformize the load over time. This approach, called scheduling with offsets is routinely used today in the design of vehicles [START_REF] Grenier | Pushing the limits of CAN -Scheduling frames with offsets provides a major performance boost[END_REF].

Its use in the context of AFDX is explored in [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF][START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF]. The experiments in these studies show that offsets are very efficient to reduce the latencies of the packets in the networ k. In [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF], it is assumed that the VL are send in a purely peri odic way by the end systems, and that per-end systems offsets are assigned to VL (i.e. local synchronization on an end-system between flows, but no synchronizations between the end-systems). Then a method is given to take into account the offsets between flows, to propagate them throughout the network, and to compute a better bound on network delays. Different strategies to assign offsets are comp ared in [START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF], and evaluated on a realistic case study. It is shown that offsets can reduce the network delay up to 51% (average of the VLs). Another contribution of the paper is an upper bound on the possible gain: whatever the offsets are, without synchronization between end -systems, each frame can compete in each queue against one frame of each other end-systems. Using this upper bound, it is shown on the case study of the paper that the maximal possible gain would be of 53%.

However there is a downside if data production and data transmission are not e xplicitly synchronized: before being transmitted, a packet may have to wait for a time that can be up to one transmission period (i.e., one BAG) in the end-systems. It means that this method decrease s the network delay but increases the end-system delay. Since it is commonly assumed that the network delay in AFDX is in general less than the BAG, it means that, without synchronization of task and network scheduling, this approach may actually increase the global communication latency, by increasing the "transmission latency" more than the reduction of the "network latency".

The End-System VL s cheduler is a schedu ler

As presented in Section 2, there is a VL scheduler in each end-system. The implementation of this scheduler is up to the system provider. In this study, the behavior of the Thales end-system has been modeled. For confidentiality reasons, the exact behavior of this scheduler will not be presented here. It just have to be noticed that the same kind of method that the one of [START_REF] Boyer | Collaboration entre méthode d'ordonnancement et calcul réseau[END_REF][START_REF] Boyer | Combining network calculus and scheduling theory to improve delay bounds[END_REF] is being used. Nevertheless, it can be mentioned that this scheduler has be en configured so as to ensure the respect of the 500µs maximum jitter. It can also be mentioned that this scheduler offers some way to "prioritize" the flows into the end-system, independently of the priority of the VL inside the network. A VL with a local high priority is ensured to have a end-system latency less than 1ms. Of course, if too many VLs are placed into this local high priority class, the 1ms constraint cannot be satisfied anymore.

E x p e r i m e n t a l a s s e s s m e n t 4.1 Case-study and too lset

The experiments are performed on a realistic large AFDX configuration provided by Thales Avionics, whose main characteristics are summarized in the table below.

End-systems configuration

Average gain Purely periodic 42% All VLs in local high-priority class 26% VLs with BAG ≤ 8 in local high-priority class 38%

The average gain is presented in the above table, but the table does not inform about how this gain is distributed among the VLs. This question is answered by Figure 3 by plotting the bounds with and without scheduling for all VLs. For readability, VLs are sorted by increasing value of latency with frame scheduling taken into account.

Figure 3: Upper bounds on the worst-case traversal times (WCTT in us) with (lower curve) and without the knowledge of the frame scheduling within the sending end -system, placing VLs with BAG not greater than 8ms in local high priority class. Virtual Links are sorted by increasing latencies. The VLs on the graph are sorted by increasing latencies computed with frame scheduling knowledge, which explains why the lower curve is monotonous unlike the upper curve.

C o n c l u s i o n a n d f u t u r e w o r k

The network calculus theory is used to provide upper bounds the network latencies since the A380 [START_REF] Grieu | Analyse et évaluation de techniques de commutation Ethernet pour l'interconnexion des systèmes avioniques[END_REF]. However, measures on real networks were dramatically smaller than the theoretical bounds. It was first supposed that the theory was overly pessimistic. Since the work in [START_REF] Bauer | Improving the worst-case delay analysis of an AFDX network using an optimized trajectory approach[END_REF] on the estimation of lower bounds on the latencies, it was experimentally shown in [START_REF] Boyer | Experimental assessment of timing verification techniques for AFDX[END_REF] that the pessimism of the method was less than 25%. This means that, without taking into account new information on the real system in the model, no large improvement of the bounds can be achieved.

It has been shown in previous theoretical studies [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF][START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF][START_REF] Boyer | Collaboration entre méthode d'ordonnancement et calcul réseau[END_REF][START_REF] Boyer | Combining network calculus and scheduling theory to improve delay bounds[END_REF] that considering the offsets between the flows in an AFDX network can dramatically reduce the evaluation of the network traversal times. Because these studies assume a strong link between the task scheduling and the network scheduling, they would impose an unaffordable overhead in aircraft design. This study however does not consider the applicative scheduling, but only the frame scheduling done in Thales endsystems. The system that is analyzed remains in the network perimeter and can be managed by the network designer.

Figure 1 :

 1 Figure 1: Communication delays: end-system latency and network traversal latency.

Figure 3 :

 3 Figure 3: Jitter at end-System output.

The choice to combine the gain of two improvements in the same value is done to show their impact in an industrial context. The reader can refer to[START_REF] Boyer | Experimental assessment of timing verification techniques for AFDX[END_REF] for an evaluation of the impact of the use of Ultimately Pseudo-Periodic (UPP) functions alone, without modeling the frame scheduling at the source end-system.

©2013 ONERA / UL / RTaW / THALES AVIONICS 8/8

In our experiments performed on a realistic case-study, integrating the frame scheduling done at the sending end in the timing analysis allow to reduce the upper bound on the network delay by an average of 38%. This improvement opens the door to a more efficient use of the network bandwidth and may ease the incrementally of existing systems.

©2013 ONERA / UL / RTaW /

Entities

The computations are performed with the RTaW-Pegase tool [START_REF] Boyer | PEGASE -a robust and efficient tool for worst-case network traversal time evaluation on AFDX[END_REF] that implements AFDX and switched Ethernet timing analysis with network calculus. Unlike most other timing analysis tools, RTaW-PEGASE is no black-box in the sense that the algorithms are documented and have been proven correct in peer-reviewed publications (see [START_REF] Bouillard | An Algorithmic Toolbox for Network Calculus[END_REF][START_REF] Boyer | Deficit Round Robin with network calculus[END_REF][START_REF] Boyer | A simple and efficient class of functions to model arrival curve of packetised flows[END_REF] and, more recently, with the help of formal methods in [START_REF] Mabille | Certifying Network Calculus in a Proof Assistant[END_REF] to assert the correctness of the computation). When information about the scheduling of frames in the sending end-system is available, RTaW-Pegase makes use of a more fine-grained model that accounts for the resulting desynchronization between flows, and thus leads to more accurate latency bounds.

Results with several End -System configurations

The gain is computed on a per-VL basis: for each VL, the bound on the latency is computed first without considering the end-system scheduling using the state-of-the-art of network calculus as most often used in the industry now, that is with piecewise linear functions [START_REF] Grieu | Analyse et évaluation de techniques de commutation Ethernet pour l'interconnexion des systèmes avioniques[END_REF]. The corresponding bound is denoted by ai for VL i. Then, for a given configuration of the VL scheduler on the sending end-system, the new delay bound bi is computed, using the generic ultimately pseudo-periodic functions [START_REF] Bouillard | An Algorithmic Toolbox for Network Calculus[END_REF]. The per-VL gain is gi =(ai-bi)/ai. It should be noted that the gains gi combine the benefits of two recent advances in network calculus: better computing functions and better endsystem modeling 1 . Finally, the average of all gains is computed.

The first experiment was done to compare the current appr oach with the previous works of [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF][START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF]: a purely periodic scheduler was assumed, with the same offset assignment algorithms. It leads to an average gain of 42%. This must be compared with the 51% of [START_REF] Li | Improving end-to-end delay upper bounds on an AFDX network by integrating offsets in analysis[END_REF][START_REF] Li | Existing offset assignments are near optimal for an industrial AFDX network[END_REF], while we do not know if this is because the case study is different, or because of the analysis method itself.

In the second experiment, all VLs are placed in the local high priority class. This class tries to minimize the waiting time into the end-system, while still maintaining the 500µs jitter constraint . Of course, if the end-system is too loaded, the 1ms of local delay cannot be satisfied. In this case, the average gain is equal to 26% only. Finally, only the VLs with a BAG no greater than 8ms are placed into this local high priority class. The rational is that VLs with smaller BAGs are more often used by avionics systems with stringent delay requirements. In this case, the gain is 38%, which is almost as good as for the purely periodic configuration.


Jean-Charles Chaudemar

Vitaly Savicks

Michael Butler

John Colley

Co-simulation of Event-B and Ptolemy II Models via FMI

Introduction

In the framework of model-based design formal modelling, verification and simulation of safety-critical systems are supported by several methods and tools. Interfacing these tools often becomes challenging for heterogeneous systems. The FMI standard enables integration of different simulation tools through artefacts called Functional Mockup Units (FMU) [START_REF] Blochwitz | The functional mockup interface for tool independent exchange of simulation models[END_REF]. The FMI standard is mainly based on the concept of scalability of the simulation as it deals with heterogeneous cyber-physical systems. The combination of discrete behaviour and continuoustime environment is a common case study in hybrid simulation. Moreover, another aspect of the FMI is to enhance the capability of the tools. Thus, a collaborative simulation between the Rodin [START_REF] Abrial | Rodin: an open toolset for modelling and reasoning in Event-B[END_REF] and Ptolemy [START_REF] Brooks | Ptolemy II-heterogeneous concurrent modeling and design in Java[END_REF] is leveraged by both platforms. While Event-B is enhanced by new models of computation of Ptolemy, Ptolemy leverages the expressivity and properties validation (theorem/invariant proofs) implemented by Event-B. The main rationale of the co-simulation between Event-B and Ptolemy relies on the intention of dissimilarity and complementarity of the modelling viewpoints. Event-B provides formal modelling by specifying conditions, actions and properties that manage discrete event behaviour, whereas Ptolemy gives a structural viewpoint in terms of actors, components or functions with relation to concerned behaviour. Thus, the association of Ptolemy and Event-B puts together structural and formal aspects.

This paper focuses on the collaborative simulation of models supported by both Ptolemy II and Event-B. The ongoing work consists of the design of a diagrammatic co-simulation surface and its application to a controller case study.

Event-B

Event-B is a refinement-based formal method for modelling and analysis of complex safety-critical systems [START_REF] Abrial | Modeling in Event-B: system and software engineering[END_REF]. A system is modelled in Event-B as a collection of state variables and events (guarded actions) that act on variables. System properties are specified as invariants on state variables and are formally verified by deductive proof. The key mechanism of the method is the refinement, i.e. incremental development from an abstract to a concrete model that splits the complex task of formal verification into manageable proofs, allowing to detect the errors as soon as they are introduced along the modelling process. The extensible Rodin platform aids this process with automatic provers and additional modelling features from third-party plug-ins. Models can also be validated by the ProB model checker and animator tool [START_REF] Leuschel | ProB: an automated analysis toolset for the B method[END_REF].

In general an Event-B model consists of a static context, which contains constants and axioms, and a dynamic machine that comprises variables (sets, binary relations, functions, etc.), invariants (constraints on variables that must hold) and events that model the behaviour. An event may contain parameters, guards (event-enabling conditions) and actions that modify state variables. Events are atomic (all actions happen instantaneously) and their choice is nondeterministic, i.e. when multiple events are enabled a single event is selected non-deterministically.

There may exist relationships in Event-B. A machine can see a context in order to use its constants. On refinement: 1) a context can extend another context by introducing new constants; 2) a machine can refine another machine by introducing more details either in the systems state (data refinement) or in the behaviour (horizontal refinement).

Ptolemy II

Ptolemy II is an open source framework for modelling and simulation of cyberphysical systems. This platform enables the hierarchical composition of components for the design of embedded systems. A system component is described by a set of interfaced actors in interaction. The design of a system is actor-oriented in Ptolemy [START_REF] Lee | Heterogeneous actor modeling[END_REF].

Actors are executable Ptolemy components which have syntax and semantics. An actor reacts to stimuli (token) at its input port and produces stimuli at its output port. Different relations could be applied to actors like composition (hierarchy), or high-order relation (an actor which enables a reduction and a simplification of a model).

Directors are special components which give meaning to a model. Various directors are implemented in Ptolemy so as to provide different models of computation and determine how actors communicate. The execution of actors is composed of three main phases:

-Setup phase divided in two steps: preinitialise and initialise. The preinitialise step is performed once at the very beginning of the execution. This step relates to a static analysis of the actor's actions and communication. It is just followed by the initialise step. The latter sets initial values to data and resets local state. -Iterate phase or sequence of iterations divided into three steps: prefire, fire, postfire. The prefire step enables to meet preconditions related to the execution termination. The fire step reads the input data, computes the actor's behaviour and produces output data. Then the postfire step updates the state. Iteration is resumed possibly several times to reach a steady state. -Wrapup phase: this phase ensures that the execution is properly terminated.

The execution of an actor is enabled through the implementation of a model of computation (MoC) associated with this actor. The MoC describes how the actor interaction is related to other actors. Indeed the MoC defines the communication semantics.

Co-simulation Approach

The FMI standard relies on the development of artefacts called Functional Mockup Units (FMU). An FMU is a zipped file, which contains an xml document describing the variables and capabilities of the model, and a dynamic-link library (dll) implementing the behaviour performed by the tool that simulates it. We are using the FMI standard and the structure of the FMU to bundle Ptolemy models for co-simulation framework developed in the Rodin platform [START_REF] Savicks | Co-simulation of Event-B and Continuous Models in Rodin[END_REF].

Our approach to perform a co-simulation between Rodin and Ptolemy consists of several steps. First, we develop an Event-B model of controller in Rodin and a Ptolemy model of the environment behaviour we want to co-simulate. The latter model consists of a composite actor and sub-actors coordinated by the Synchronous Data Flow (SDF) director. The model takes an input signal, generated by the model of controller, and produces a dependant feedback output signal. The controller model is a standard Event-B machine extended with modal semantics using the state machines plug-in for Rodin [START_REF] Savicks | Event-B Wiki: Event-B Statemachines[END_REF].

As a second step we generate C code from the Ptolemy model via automatic code generator module and transform it into a .dll using FMU SDK 3 . DLL and corresponding model description XML are bundled into an FMU file.

Next we import the FMU into the Rodin co-simulation environment together with Event-B model and compose two models into a component graph. The component composition is achieved using the Component diagram plug-in for Rodin -a front-end of the co-simulation framework, developed as part of the ADVANCE project 4 .

Finally we implement the FMI master algorithm in Groovy scripting language on top of ProB animator for Event-B and integrate it with the composition graph model. This algorithm initialises and coordinates the simulation process between two components, as well as provides the simulation output. The Event-B component (controller) is coordinated by the master via ProB API, while the Ptolemy component (environment) is coordinated using FMI.

AOA Sensor Processing

Case Study

Traditionally in aeronautics, safety-critical systems are based on a rigorous dissimilarity applied to the architectures to avoid common points of failure. One of the widely used technics is the COM/MON architecture which consists of two separated command and monitoring units [START_REF] Sghairi | Distributed and Reconfigurable Architecture for Flight Control System[END_REF]. All input and output data are monitored permanently and only the command unit sends the command data to actuators under the control of the monitoring unit. This dual behaviour is of interest in the application of the co-simulation between Ptolemy and Event-B. The environment and the command data generation are devoted to Ptolemy model whereas Event-B model is in charge of the monitoring unit and controls the output data to be sent.

Likewise our case study extracted from a J. Rushby's presentation [START_REF] Rushby | Safety, Fault-tolerance, Verification, and Certification for Embedded Systems[END_REF] relates to the utilisation of three Angle of Attack (AOA) sensors in the Flight Control System (FCS). As safety is the first objective that is required for aircraft avionics systems, these three sensors are combined in an algorithm which provides the most relevant value of measurement. The algorithm is synthetically based on the computation of the median of the three measures so as to detect erroneous values and erroneous devices, along with on the computation of the average value between two of the three sensors.

From this illustration, our study consists in modelling the strategy of combination of the sensors by distinguishing an AOA sensors algorithm modelled in Ptolemy and the same algorithm modelled in Event-B.

Ptolemy Model

The Ptolemy model of AOA sensors consists of a SDF MoC as a first abstraction in order to only focus on the specification of the algorithm part (figure 2). Indeed the time aspect is modelled by series of iterations based on the measurement sampling frequency of 20Hz. Thus to represent a delay of 1.2 seconds, 24 iterations are performed. The first CompositeActor mainly describes the processing for the detection of erroneous measures: the median of the three measures is computed, then the difference between each measure and the median is compared to a threshold; the result of this comparison indicates if the measure is erroneous or not. This processing is followed by the FSMActor for each sensor. The FSMActor enables to identify a erroneous sensor after 1 second of erroneous measures sent by this sensor.

Similarly a second CompositeActor2 follows the previous and deals with the strategy about the final AOA measure (figure 3). Its output is either the current mean of sensor 1 and sensor 2 or the previous mean held during 1.2 seconds. It is provided by the Case actor associated with the FSMActor. The CompositeActor2 behaviour is also modelled in Event-B.

Event-B Controller

The controller actor of the Ptolemy model has been duplicated, which is a standard practice in aeronautics [START_REF] Sghairi | Distributed and Reconfigurable Architecture for Flight Control System[END_REF], by an Event-B model. The model has been implemented using a state machine plug-in for Rodin [START_REF] Savicks | Event-B Wiki: Event-B Statemachines[END_REF], which allowed the control flow, i.e. the ordering of events, to be specified. Two state machines have been defined in the controller:

-controlSM (Figure 4(a)), which defines the control flow from an interface (to master) perspective, with a readInputs event for reading sensor inputs and two output events useCurrent and usePrev that model current and previous mean output, respectively. -modeSM (Figure 4(b)), which defines the modal semantics of the controller and models a delay in the output. The controller operates in either sCurrent or sPrevious mode, switching to the latter when a threshold is exceeded, and to the former after 1.2 seconds since the threshold crossing. The delay of 1.2 seconds is modelled by a variable modeCounter that is set on a switchPrev execution and is decremented by usePrev event until it reaches 0, at which point a switchCurrent event becomes enabled. The Event-B code for switch events is given below. Note that sPrevious and sCurrent are modelled as boolean variables (translated from the state machines automatically).

Simulation Master

Our simulation master, displayed below, is written in the Groovy language to facilitate the scripting capabilities of the ProB animator tool, which is used in the Rodin for animating (simulating) Event-B models. The design of the master is based on a proposed algorithm demonstrated in the FMI for Co-simulation specification [START_REF]MODELISAR: Functional Mock-up Interface for Co-Simulation[END_REF]. The key aspects of the master script are the passing of the sensor values, read from the Ptolemy FMU, to the Event-B controller via readInputs event parameters, and the semantics of a simulation step of the Event-B component -a non-deterministic execution of events until one of the step-finishing events (useCurrent or usePrev) is executed. The step of an FMU component is performed by a standard FMI call doStep. Another important aspect is the treatment of the Real-typed signals by Event-B, which currently does not support the Real type [START_REF] Abrial | Formalizing hybrid systems with Event-B[END_REF]. Real values from the FMU are converted to Event-B integers by agreed decimal point shift.

import

Co-Simulation Results

A successful simulation has been carried out for 30 seconds with a step size 1. The results are shown in Figure 5.

The specification of the system defines the operational frequency of 20Hz, which we have mapped to 20 steps. Consequently, the delay of the mean value for 1.2 seconds was modelled by 24 steps, visible as a meanOut signal on the plot. Notice that the actual delay is 25 steps due to a delay of the control signal for 1 step, caused by the discrete data synchronisation and simplistic algorithm of the master, i.e. a mean signal received by the controller at t=N is processed and output at t=N+1. This behaviour can be improved by adapting a predictive control logic and a master with a rollback and step-size prediction [START_REF] Broman | Determinate composition of FMUs for co-simulation[END_REF].

Conclusions and Outlook

In this work we have tried to demonstrate the proof of concept of a co-simulation between a well-known formalism, such as Event-B, and a heterogeneous simulation tool Ptolemy II. A mixture of domain specific modelling and simulation tools, which is based on the rigorous analysis approaches for verifying safety and reliability constraints, is arguably an essential technology in the face of the development of cyber-physical systems [START_REF] Lee | Cyber physical systems: Design challenges[END_REF][START_REF] Rajkumar | Cyber-physical systems: the next computing revolution[END_REF][START_REF] Marwedel | Embedded and cyber-physical systems in a nutshell[END_REF]. Our simulation results have showed that an integration is possible, even more advantageous, as it is based on the tool-independent FMI standard, which in theory allows a Ptolemy FMU to be used in any other FMI-compliant simulator. The results have also revealed the existing problems and limitations of both tools, namely limited support of directors and actors by the Ptolemy's C code generator and a strong requirement for Real type support in the Event-B language. We hope that these issues will be addressed as the tools develop.

This ongoing work highlights the ability of the FMI co-simulation between Ptolemy and Event-B, although both tools do not provide a support for FMI standard yet. The main difficulties have been to generate the FMU file from Ptolemy model manually since its code generation component is working partially. Therefore, several Ptolemy models have been carried out to ease the code generation.

Within the framework of the FMI co-simulation the outlook is twofold: to take into account continuous time and to implement the verification of combined system properties.

Fig. 1 .

 1 Fig. 1. Co-simulation process in Rodin

Fig. 2 .Fig. 3 .

 23 Fig. 2. Ptolemy model of AOA processing

Fig. 4 .

 4 Fig. 4. State machines of the Event-B controller

  event switchP rev where sCurrent = T RU E medianS1 > T HRESHOLD ∨ medianS2 > T HRESHOLD then sCurrent := F ALSE sP revious := T RU E modeCounter := DELAY end event switchCurrent where sP revious = T RU E modeCounter = 0 then sP revious := F ALSE sCurrent := T RU E end

Fig. 5 .

 5 Fig. 5. Co-simulation output (simulation time = 30s, step size = 1s)

FMU SDK source code is available at https://github.com/cxbrooks/fmusdk

ADVANCE: EU Project IP-287563, http://www.advance-ict.eu