Estudo de sistemas multicomponentes no processo de injeção cíclica de vapor

In Brazilian Northeast there are reservoirs with heavy oil, which use steam flooding as a recovery method. This process allows to reduce oil viscosity, increasing its mobility and consequently its oil recovery. Steam injection is a thermal method and can occurs in continues or cyclic form. Cyclic steam stimulation (CSS) can be repeated several times. Each cycle consisting of three stages: steam injection, soaking time and production phase. CSS becomes less efficient with an increase of number of cycles. Thus, this work aims to study the influence of compositional models in cyclic steam injection and the effects of some parameters, such like: flow injection, steam quality and temperature of steam injected, analyzing the influence of pseudocomponents numbers on oil rate, cumulative oil, oil recovery and simulation time. In the situations analyzed was compared the model of fluid of three phases and three components known as Blackoil . Simulations were done using commercial software (CMG), it was analyzed a homogeneous reservoir with characteristics similar to those found in Brazilian Northeast. It was observed that an increase of components number, increase the time spent in simulation. As for analyzed parameters, it appears that the steam rate, and steam quality has influence on cumulative oil and oil recovery. The number of components did not a lot influenced on oil recovery, however it has influenced on gas production

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs