Mesoscopic approach for steady‐state free convection in a diamond array

The purpose of the present paper is testing an in‐house efficiency algorithm based on lattice Boltzmann method (LBM) and using it to resolve the obtained coupled nondimensional governing equations to analyze two‐dimensional free convection inside a cold outer cavity subjected to a heated cylindrical diamond array. Steady state or oscillatory results are obtained using the Bhatnagar‐Gross‐Krook collision model associated to the thermal LBM. Both the velocity and temperature fields are solved using the D2Q9 models. With different Rayleigh numbers (Ra), the tested free convection can either achieve to steady state or oscillatory. We extended our in house Fortran 90 code using curved boundary conditions and implemented them into a cavity with a diamond array. The numerical simulations were done using distinct Ra (10⁶ and 10 ⁷) and distances between the four neighboring circular cylinders aligned in a diamond array. The effects of several physical parameters, including Ra and position of the hot body array on flow and heat transfer characteristics are investigated. The obtained results are highlighted in the form of streamlines, isotherms, and velocities plots. We show in this paper the stability and the efficiency of the LBM to deal with a complex geometry and its ability to reach suitable convergence criteria for high Ra (10 ⁶ and 10 ⁷). The numerical results indicate that LBM can simulate numerical problems with a high Ra reaching a steady state where we can depict the change of the flow pattern and enhancement of the heat transfer in the presence of heated diamond array.     

Heat and mass transfer studies on metal-hydrogen reactor filled with MmNi4.6Fe0.4

A transient, three-dimensional computational investigation of coupled heat and mass transfer in an annular cylindrical hydrogen storage tank, equipped with fins and filled with MmNi_4.6Fe_0.4, is presented. The effects of different parameters such as length, thickness and thermal conductivity of fins and overall heat transfer coefficient on the hydrogen storage performance of the tank are studied. The predicted hydrogen storage capacity at different supply pressures showed good agreement with the experimental data reported in the literature. In addition, it is observed that the use of fins enhances heat transfer within the hydride bed and consequently 40% improvement of the time required for 90% storage can be achieved over the case without fins.     

Measurement and modelling of kinetics of hydrogen sorption by LaNi5 and two related pseudobinary compounds

The hydriding/dehydriding rates and the pressure–composition isotherms were measured for LaNi5, LaNi_4.85Al_0.15 and LaNi_4.75Fe_0.25 under quasi-isothermal and variable pressure conditions. Isothermal conditions were obtained by reducing the thermal time constant of the experimental device. Empirical rate equations to describe the sorption reaction kinetics were derived. These rates are expressed as a function of temporal composition, saturated composition, temperature, applied pressure and essentially the initial operating conditions which were not considered in most of all the previous studies related to the reaction kinetics of metal hydrides. Besides, the rate equations presented in this work can be integrated easily in the numerical models that predict dynamic flow and heat and mass transfer within realistic metal–hydrogen devices. This paper also discusses the effects of Fe and Al as substituents for Ni on P–C isotherms and reaction rates of LaNi₅ alloy.     

The treatment of ureteroceles complicated by calculi

In a series of 13 adults with calculi in ureteroceles, 10 cases underwent endoscopic meatotomy associated with endoscopic lithotripsy. In 2 bulky ureteroceles with calculi, the authors performed excision of the ureterocele and reimplantation of the ureter. In one case, the authors successfully performed extracorporeal lithotripsy. The authors obtained good results in all cases. Endoscopic meatotomy with lithotripsy is a very useful procedure for treatment of small or medium sized ureteroceles with calculi in adults.     

Improvement of thermal performance of spiral heat exchanger on hydrogen storage by adding copper fins

The reaction time of hydrogen in metal-hydride vessels (MHVs for short) is strongly influenced by the heat transfer from/to the hydride bed. In the present work an experimental study of the geometric and the operating parameters of a finned spiral heat exchanger has been carried out to identify their influence on the performance of the charging process of the MHV. The experimental results show that the charge time of the reactor is considerably reduced, when finned spiral heat exchanger is used. In addition, the effect of different parameters (flow mass and temperature of the cooling fluid, applied pressure of hydrogen in the case of absorption and desorption) has been discussed and obtained results show that a good choice of these parameters is important.     

A formal approach for the development of reactive systems

Context

This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA⁺ to verify liveness properties on Event-B models.

Objective

This paper deals with the use of two verification approaches: theorem proving and model-checking, in the construction and verification of safe reactive systems. The theorem prover concerned is part of the Click_n_Prove tool associated to the Event-B method and the model checker is TLC for TLA⁺ models.

Method

To verify liveness properties on Event-B systems, we extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we propose semantics of the extension over traces, in the same spirit as TLA⁺ does. Third, we give verification rules in the axiomatic way of the Event-B method. Finally, we give transformation rules from a temporal B model into a TLA⁺ module. We present in particular, our prototype system called B2TLA⁺, that we have developed to support this transformation; then we can verify liveness properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams and its associated tool DIXIT. As the B refinement preserves invariance properties through refinement steps, we propose some rules to get the preservation of liveness properties by the B refinement.

Results

The proposed approach is applied for the development of some reactive systems examples and our prototype system B2TLA⁺ is successfully used to transform a temporal B model into a TLA⁺ module.

Conclusion

The paper successfully defines an approach for the specification and verification of safety and liveness properties for the development of reactive systems using the Event-B method, the language TLA⁺ and the predicate diagrams with their associated tools. The approach is illustrated on a case study of a parcel sorting system.