Hong Gia Nguyen (LIPN) : Applying Distributed Computing Techniques to The Parametric Verification of Real-Time Systems ; Poster ; Slides

Nowadays, hardware and software systems (such as airplanes, satellites, metros, cars, network protocols, etc.) become more and more complex. Their failure may lead to dramatic consequences, and testing such systems is not sufficient. Therefore, formal verification is required.

Parametric timed automata (PTA) are a formalism allowing the specification and paramet ric model checking of systems with hard timing constraints incompletely specified, or subject to future changes. Among the parametric model checking algorithms, the behavioral cartography algorithm splits the parameter space of PTA in tiles in which the discrete behavior is uniform. Applications include the optimization of timing constants, and the measure of the system robustness (w.r.t. the discrete behavior).

However, parametric model checking real-world system models is impractical to most computers, as such verification techniques exhaustively may take beyond a lifetime and available memory. Distributed computing takes advantage of networked computers which communicate with each other by passing messages. All computers on the network will work simultaneously in order to accelerate computational processing. Redesigning parametric verification algorithms to adapt to the distributed paradigm is important so as to considerably increase their efficiency and their performance.

Here we present several distributed algorithms to compute the behavioral cartography of PTA efficiently. Our experimental results show a very promising decrease in the computation time when compared to the monolithic (i.e. non-distributed) algorithm.

    Imad Kissami (LIPN/LAGA) : Parallelization of ADAPT platform ; Poster ; Slides

At this time, CFD (Computational Fluid Dynamics) plays an important role in industrial designs, environmental impact assessments and academic studies. The aim of our work is to fully parallelize an unstructured adaptive code for the simulation of 3D streamer propagation in cold plasmas. This physical phenomenon is modeled by a coupled system of equations. A convection-diffusion-reaction equation to represent the evolution during time of the electron density, and an elliptic equation to give the speed propagation for the convection part and which gives rise to a linear system tosolve. The sequential version of the Streamer code that we have investigated as our initial work, needed up to one month, running on a single node and for typical benchmark. The idea is to provide a parallel version, keeping the same numerical methodology, the same type of mesh, but with an execution time much less than that given by the sequential version. Thus, the strategy adopted involves two steps:

First step:

Partitioning of the mesh with METIS, each process has a local grid used for calculations independently of the other processors.   In this part every process makes its initialization separately, sending the information of halo cells to neighbor subdomains (cells which are at the boundary of each subdomain).

Second step:   The information is collected by the master process to find the solution of the linear system.   Splitting is made to solve the linear system in parallel by using the MUMPS solver.

    Leila Abidi (LIPN) : Vers l’orchestration de grilles de PCs par les mécanismes de publication-souscription ; Poster ; Slides

Les grilles de PCs ont été proposées comme une alternative aux super-calculateurs par la fédération des milliers d’ordinateurs de bureau. Les détails de la mise en œuvre d’une telle architecture de grille, en termes de mécanismes de mutualisation des ressources, restent très difficile à cerner. Parallèlement, le Web a complètement modifié notre façon d’accéder à l’information. Le Web est maintenant une composante essentielle de notre quotidien. Les équipements ont, à leur tour, évolué d’ordinateurs de bureau ou ordinateurs portables aux tablettes, lecteurs multimédias, consoles de jeux, smartphones, ou NetPCs. Cette évolution exige d’adapter et de repenser les applications/intergiciels de grille de PCs qui ont été développés ces dernières années. Notre contribution se résume dans la réalisation d’un intergiciel de grille de PCs que nous avons appelé RedisDG. Dans son fonctionnement, RedisDG reste similaire à la plupart des intergiciels de grilles de calcul, c’est-à-dire qu’il est capable d’exécuter des applications sous forme de «sacs de tâches» dans un environnement distribué, assurer le monitoring des nœuds, valider et certifier les résultats. . . . L’innovation de RedisDG, réside dans l’intégration de la modélisation et la vérification formelles dans sa phase de conception, ce qui est non conventionnel mais très pertinent dans notre domaine. Notre approche consiste à repenser les grilles de PCs à partir d’une réflexion et d’un cadre formel permettant de les développer, de manière rigoureuse et de mieux maîtriser les évolutions technologiques à venir.

    Saida Sari (IPEN - Tunisie) : A fast finite volume solver for hydrostatic shallow water flows ; Poster ; Slides

We present a new finite volume method for the numerical solution of shallow water equations for either flat or non-flat topography. In terms of advantages, the method is simple, accurate and avoids the solution of Riemann problems during the time integration process. The proposed approach consists of a predictor stage and a corrector stage. The predictor stage uses the method of characteristics to reconstruct the numerical flux, whereas the corrector stage recovers the conservation equations. The proposed approach does not require neither nonlinear solution nor special front tracking techniques, which makes it simple, accurate and easy to implement. This new method has been tested on systems of shallow water equations at different flow regimes. Furthermore, some numerical results and applications have been illustrated for several test problems of dam-breaks for classical, Density-driven, multi-layered and rotational shallow water flows. For the selected test examples, the results obtained using the proposed finite volume method are compared to those obtained using some other schemes. Those results indicate good shock resolution with high accuracy and without any nonphysical oscillations near the shock areas. And most important, in term of CPU times, the proposed method is highly performant in comparison to the others.

    Fayssal Benkhaldoun (LAGA) : High Performance meshfree methods for fluid flows Computation ; Poster ; Slides

We present radial basis functions for solving nonlinear equations of conservation laws. We aim at constructing a general RBF Meshfree method having good qualities of accuracy an robustness, efficient enough and able to deal with convection dominated problems. The method is based on the local collocation formulation and does not require either generation of a grid or evaluation of an integral. Upwind techniques are used to allocate collocation points within the characteristic solutions. The main advantages of this approach are neither mesh generations nor Riemann problem solvers are required during the solution process. Numerical results are shown for several test examples. The main focus is to examine the performance of the proposed meshless method for shock-capturing property in conservation laws. The obtained results demonstrate its ability to capture the main solution features.

    Tarek Ghoudi (LAGA) : Mesh adaptation for numerical calculation - Performance and Efficiency of a posteriori error estimates ; Poster ; Slides

This poster presents an adaptive mesh refinement strategy based on a posteriori error estimator. The method developed in this work is based on Vohralik's estimator and a mesh refinement strategy built on a mix of newest-bisection method and a standard 4-sons-h-refinement method. This method is then illustrated with two 2D cases, the first case with a smooth solution and the second with an irregular solution.
Our work is divided into two steps:
1/ First we consider an elliptique problem with a smooth solution and the example proposed by Martin Vohralik for the computation of the a posteriori error for a simple diffusive problem, and we study several tests on various types of mesh (regular, irregular) to calculate the curves of efficiency, exact errors and estimated errors.
2/ then we compute the execution time for a given precision using both a uniformly refined mesh and an adapted mesh, and we compare the CPU time. The coupling made between the Martin Vohralik's estimator and our method of mesh adaptation "Adapt-Newest" allows us to have a important performance in term of CPU time.

    Aloïs Bissuel (Dassault Aviation) : Improving the convergence of the linearized Navier-Stokes equations ; Poster ; Slides

To produce efficient new designs, aircraft manufacturers may resort to automatic optimizations tools relying on linearized Navier-Stokes solver [1]. Flutter analysis is another application where one can use time-domain linearization of the Navier-Stokes equations [2]. In both cases, one has to solve a linear system. The Navier-Stokes solver uses stabilized finite-elements on unstructured meshes. The linear system to be solved is thus spare, asymmetric, and large with up to 100s of millions of unknowns. To improve the convergence rate, several methods are investigated : SUPG stabilization, domain decomposition using coarse spaces and multiple right-hand sides.