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

STREAM-AP: um processo para sistematizar a escolha de padrões arquiteturais baseado em requisitos não-funcionais

The importance of non-functional requirements for computer systems is increasing. Satisfying these requirements requires special attention to the software architecture, since an unsuitable architecture introduces greater complexity in addition to the intrinsic complexity of the system. Some studies have shown that, despite requirements engineering and software architecture activities act on different aspects of development, they must be performed iteratively and intertwined to produce satisfactory software systems. The STREAM process presents a systematic approach to reduce the gap between requirements and architecture development, emphasizing the functional requirements, but using the non-functional requirements in an ad hoc way. However, non-functional requirements typically influence the system as a whole. Thus, the STREAM uses Architectural Patterns to refine the software architecture. These patterns are chosen by using non-functional requirements in an ad hoc way. This master thesis presents a process to improve STREAM in making the choice of architectural patterns systematic by using non-functional requirements, in order to guide the refinement of a software architecture

BTS:uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes

The component-based development of systems revolutionized the software development process, facilitating the maintenance, providing more confiability and reuse. Nevertheless, even with all the advantages of the development of components, their composition is an important concern. The verification through informal tests is not enough to achieve a safe composition, because they are not based on formal semantic models with which we are able to describe precisally a system s behaviour. In this context, formal methods provide ways to accurately specify systems through mathematical notations providing, among other benefits, more safety. The formal method CSP enables the specification of concurrent systems and verification of properties intrinsic to them, as well as the refinement among different models. Some approaches apply constraints using CSP, to check the behavior of composition between components, assisting in the verification of those components in advance. Hence, aiming to assist this process, considering that the software market increasingly requires more automation, reducing work and providing agility in business, this work presents a tool that automatizes the verification of composition among components, in which all complexity of formal language is kept hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport) helps to create and compose components, predicting, in advance, undesirable behaviors in the system, such as deadlocks

Geração de processos WS-BPEL com base em um algoritmo de reescrita de regras

Web services are computational solutions designed according to the principles of Service Oriented Computing. Web services can be built upon pre-existing services available on the Internet by using composition languages. We propose a method to generate WS-BPEL processes from abstract specifications provided with high-level control-flow information. The proposed method allows the composition designer to concentrate on high-level specifi- cations, in order to increase productivity and generate specifications that are independent of specific web services. We consider service orchestrations, that is compositions where a central process coordinates all the operations of the application. The process of generating compositions is based on a rule rewriting algorithm, which has been extended to support basic control-flow information.We created a prototype of the extended refinement method and performed experiments over simple case studies

Condutividade térmica de rochas: uma aplicação para granitos ornamentais

This dissertation focuses on rock thermal conductivity and its correlations with petrographic, textural, and geochemical aspects, especially in granite rocks. It aims at demonstrating the relations of these variables in an attempt to enlighten the behavior of thermal effect on rocks. Results can be useful for several applications, such as understanding and conferring regional thermal flow results, predicting the behavior of thermal effect on rocks based upon macroscopic evaluation (texture and mineralogy), in the building construction field in order to provide more precise information on data refinement on thermal properties emphasizing a rocky material thermal conductivity, and especially in the dimension stone industry in order to open a discussion on the use of these variables as a new technological parameter directly related to thermal comfort. Thermal conductivity data were obtained by using Anter Corporation s QuicklineTM -30 a thermal property measuring equipment. Measurements were conducted at temperatures ranging between 25 to 38 OC in samples with 2cm in length and an area of at least 6cm of diameter. As to petrography data, results demonstrated good correlations with quartz and mafics. Linear correlation between mineralogy and thermal conductivity revealed a positive relation of a quartz percentage increase in relation to a thermal conductivity increase and its decrease with mafic minerals increase. As to feldspates (K-feldspate and plagioclase) they show dispersion. Quartz relation gets more evident when compared to sample sets with >20% and <20%. Sets with more than 20% quartz (sienogranites, monzogranites, granodiorites, etc.), exhibit to a great extent conductivity values which vary from 2,5 W/mK and the set with less than 20% (sienites, monzonites, gabbros, diorites, etc.) have an average thermal conductivity below 2,5 W/mK. As to textures it has been verified that rocks considered thick/porphyry demonstrated in general better correlations when compared to rocks considered thin/medium. In the case of quartz, thick rocks/porphyry showed greater correlation factors when compared to the thin/medium ones. As to feldspates (K-feldspate and plagioclase) again there was dispersion. As to mafics, both thick/porphyry and thin/medium showed negative correlations with correlation factor smaller than those obtained in relation to the quartz. As to rocks related to the Streckeisen s QAP diagram (1976), they tend to fall from alcali-feldspates granites to tonalites, and from sienites to gabbros, diorites, etc. Thermal conductivity data correlation with geochemistry confirmed to a great extent mineralogy results. It has been seen that correlation is linear if there is any. Such behavior could be seen especially with the SiO2. In this case similar correlation can be observed with the quartz, that is, thermal conductivity increases as SiO2 is incremented. Another aspect observed is that basic to intermediate rocks presented values always below 2,5 W/mK, a similar behavior to that observed in rocks with quartz <20%. Acid rocks presented values above 2,5 W/mK, a similar behavior to that observed in rocks with quartz >20% (granites). For all the other cases, correlation factors are always low and present opposite behavior to Fe2O3, CaO, MgO, and TiO2. As to Al2O3, K2O, and Na2O results are not conclusive and are statistically disperse. Thermal property knowledge especially thermal conductivity and its application in the building construction field appeared to be very satisfactory for it involves both technological and thermal comfort aspects, which favored in all cases fast, cheap, and precise results. The relation between thermal conductivity and linear thermal dilatation have also shown satisfactory results especially when it comes to the quartz role as a common, determining phase between the two variables. Thermal conductivity studies together with rocky material density can function as an additional tool for choosing materials when considering structural calculation aspects and thermal comfort, for in the dimension stone case there is a small density variation in relation to a thermal conductivity considerable variation

Structural insights for fatty acid binding in a Lys49-phospholipase A(2): crystal structure of myotoxin II from Bothrops molojeni complexed with stearic acid

The crystal structure of dimeric Lys49-phospholipase A2 myotoxin-II from Bothrops moojeni (MjTX-II) co-crystallized with stearic acid (C18H36O2) has been determined at a resolution of 1.8 angstrom. The electron density maps permitted the unambiguous inclusion of six stearic acid molecules in the refinement. Two stearic acid molecules could be located in the substrate-binding cleft of each monomer in positions, which favor the interaction of their carboxyl groups with active site residues. The way of binding of stearic acids to this Lys49-PLA(2)s is analogous to phospholipids and transition state analogues to catalytically active PLA(2)s. Two additional stearic acid molecules were located at the dimer interface region, defining a hitherto unidentified acyl-binding site on the protein surface. The strictly conserved Lys122 for Lys49-PLA(2)s may play a fundamental role for stabilization of legend-protein complex. The comparison of MjTX-II/satiric acid complex with other Lys-PLA(2)s structures whose putative fatty acids were located at their active site is also analysed. Molecular details of the stearic acid/protein interactions provide insights to binding in croup I/II PLA(2)s and to the possible interactions of Lys49-PLA(2)s with target membranes. (c) 2004 Elsevier SAS. All rights reserved.

Vírus da leucemia felina: análise da classificação da infecção, das técnicas de diagnóstico e da eficácia da vacinação com o emprego de técnicas sensíveis de detecção viral

O Vírus da leucemia felina (FeLV) pertence à família Retroviridae, gênero Gammaretrovirus. Diferentemente de outras retroviroses, uma parcela dos gatos jovens e adultos exposta ao FeLV não apresenta antigenemia/viremia, de acordo com as técnicas convencionais de detecção viral, como isolamento em cultivo celular, imunofluorescência direta e ELISA. O emprego de técnicas de maior sensibilidade para detecção e quantificação viral, como o PCR quantitativo, permitiu a identificação de animais positivos para a presença de DNA proviral e RNA na ausência de antigenemia/viremia e, com isso, um refinamento da análise das diferentes evoluções da infecção. Assim, reclassificou-se a patogenia do FeLV em 4 categorias: infecção abortiva, regressiva, latente e progressiva. Foi possível também detectar DNA proviral e RNA em animais considerados imunes ao FeLV após vacinação. Diante disso, os objetivos desta revisão de literatura foram demonstrar as implicações da utilização de técnicas sensíveis de detecção viral na interpretação e classificação da infecção do FeLV e rever as técnicas de detecção do vírus para fins de diagnóstico. Além disso, apresentar os resultados referentes à eficácia da vacinação contra o FeLV com a utilização dessas técnicas.

Density and Spatial Distribution of Buffy-tufted-ear Marmosets (Callithrix aurita) in a Continuous Atlantic Forest

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Bonding Efficacy of New Self-etching, Self-adhesive Dual-curing Resin Cements to Dental Enamel

Purpose: This study evaluated the efficacy of the union between two new self-etching self-adhesive resin cements and enamel using the microtensile bond strength test.Materials and Methods: Buccal enamel of 80 bovine teeth was submitted to finishing and polishing with metallographic paper to a refinement of #600, in order to obtain a 5-mm(2) flat area. Blocks (2 x 4 x 4 mm) of laboratory composite resin were cemented to enamel according to different protocols: (1) untreated enamel + RelyX Unicem cement (RX group); (2) untreated enamel + Bifix SE cement (BF group); (3) enamel acid etching and application of resin adhesive Single Bond + RelyX Unicem (RXA group); (4) enamel acid etching and application of resin adhesive Solobond M + Bifix SE (BFA group). After 7 days of storage in distillated water at 37 degrees C, the blocks were sectioned for obtaining microbar specimens with an adhesive area of 1 mm(2) (n = 120). Specimens were submitted to the microtensile bond strength test at a crosshead speed of 0.5 mm/min. The results (in MPa) were analyzed statistically by ANOVA and Tu key's test.Results: Enamel pre-treatment with phosphoric acid and resin adhesive (27.9 and 30.3 for RXA and BFA groups) significantly improved (p <= 0.05) the adhesion of both cements to enamel compared to the union achieved with as-polished enamel (9.9 and 6.0 for RX and BF).Conclusion: Enamel pre-treatment with acid etching and the application of resin adhesive significantly improved the bond efficacy of both luting agents compared to the union achieved with as-polished enamel.

A homovalent doping in PMN ceramics by using lithium and scandium cations

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Influence of oxygen flow on crystallization and morphology of LiNbO3 thin films

Polymeric precursor solution (Pechini method) was used to deposit LiNbO3 thin films by spin-coating on (100) silicon substrates. X-ray diffraction data of thin films showed that the increase of oxygen flow promotes a preferred orientation of (001) LiNbO3 planes parallel to the substrate surface. Surface roughness and grain size, observed by atomic force microscopy, change also with oxygen flow.

Crystal Structure Determination of Mebendazole Form A Using High-Resolution Synchrotron X-Ray Powder Diffraction Data

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Crystal structure of propylthiouracil determined using high-resolution synchrotron X-ray powder diffraction

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Powder X-ray characterization of lithium thiazoildine-4-carboxylate

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Electronic structure, growth mechanism and photoluminescence of CaWO4 crystals

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)