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

Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

Este trabalho apresenta uma técnica de verificação formal de Sistemas de Raciocínio Procedural, PRS (Procedural Reasoning System), uma linguagem de programação que utiliza a abordagem do raciocínio procedural. Esta técnica baseia-se na utilização de regras de conversão entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, são apresentadas regras de conversão de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verificação formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verificação das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional disponível para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de conversão PRS-RPC, podemos ser levados a querer fazer esta conversão de maneira estritamente manual. No entanto, a probabilidade de introdução de erros na conversão é grande, fazendo com que o esforço necessário para garantirmos a corretude da conversão manual seja da mesma ordem de grandeza que a eliminação de eventuais erros diretamente no programa PRS original. Assim, a conversão automatizada é de suma importância para evitar que a conversão manual nos leve a erros indesejáveis, podendo invalidar todo o processo de conversão. A principal contribuição deste trabalho de pesquisa diz respeito ao desenvolvimento de uma técnica de verificação formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de conversão de PRS para RPC. A segunda fase é concernente ao desenvolvimento de um conversor para fazer a transformação de maneira automatizada dos programas PRS para as RPCs. A conversão automática é possível, porque todas as regras de conversão apresentadas seguem leis de formação genéricas, passíveis de serem incluídas em algoritmos

Aplicação do método B ao projeto formal de software embarcado

This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry

Método híbrido para detecção e diagnóstico de falhas baseado em resíduos

The detection and diagnosis of faults, ie., find out how , where and why failures occur is an important area of study since man came to be replaced by machines. However, no technique studied to date can solve definitively the problem. Differences in dynamic systems, whether linear, nonlinear, variant or invariant in time, with physical or analytical redundancy, hamper research in order to obtain a unique solution . In this paper, a technique for fault detection and diagnosis (FDD) will be presented in dynamic systems using state observers in conjunction with other tools in order to create a hybrid FDD. A modified state observer is used to create a residue that allows also the detection and diagnosis of faults. A bank of faults signatures will be created using statistical tools and finally an approach using mean squared error ( MSE ) will assist in the study of the behavior of fault diagnosis even in the presence of noise . This methodology is then applied to an educational plant with coupled tanks and other with industrial instrumentation to validate the system.

Contribuição ao estudo da isonomia na tributação sob a perspectiva da ordem econômica

The study aims to investigate the limits of state intervention via induction on Economic Order, especially in cases regarding tax equality, through the analysis of their effects on economic development and on free competition from the perspective of economic efficiency and the Constitution. Thus, the work seeks to demonstrate that the achievement of equality in taxation is important in that it strengthens the economic relations in terms of efficiency, protects competition and fosters economic development to reduce regional and social inequalities and other constitutional desiderata. A dissertation is characterized by interdisciplinarity and was divided into two parts. The first is to discuss the legal meaning of equality from the doctrinal analysis of the principle and the relationship between equality and justice in the economic sense without rejecting its philosophical content. It is noteworthy that hermeneutics and the philosophy of language are useful tools for achieving equality in presenting the pragmatic methodologies applicable to the subject in terms of corrective justice. Based on these general assumptions, is going to study the tax equality and their characteristics, the corollary of the ability to pay and its relation to the economic capacity and the issue of progressivity in taxation as an ideal of distributive justice. The second part concerns the legal foundations of Economic Order and its relation to extrafiscality as a means of economic regulation in order to investigate the efficiency of this induction in order to promote economic development, free competition and tax equality itself to reduce inequalities and distributing wealth. Within this context, we investigated the scope of the constitutional principles of economic order, free enterprise and free competition, and favored differential treatment for small and medium enterprises, the issue of regional development for the reduction of regional and social inequalities, the problem the "fiscal war" and finally the efficiency from the perspective of Economic Analysis of Law

Uma linguagem de modelagem da interação para auxiliar a comunicação designer-usuário

The development of interactive systems involves several professionals and the integration between them normally uses common artifacts, such as models, that drive the development process. In the model-driven development approach, the interaction model is an artifact that includes the most of the aspects related to what and how the user can do while he/she interacting with the system. Furthermore, the interactive model may be used to identify usability problems at design time. Therefore, the central problematic addressed by this thesis is twofold. In the first place, the interaction modeling, in a perspective that helps the designer to explicit to developer, who will implement the interface, the aspcts related to the interaction process. In the second place, the anticipated identification of usability problems, that aims to reduce the application final costs. To achieve these goals, this work presents (i) the ALaDIM language, that aims to help the designer on the conception, representation and validation of his interactive message models; (ii) the ALaDIM editor, which was built using the EMF (Eclipse Modeling Framework) and its standardized technologies by OMG (Object Management Group); and (iii) the ALaDIM inspection method, which allows the anticipated identification of usability problems using ALaDIM models. ALaDIM language and editor were respectively specified and implemented using the OMG standards and they can be used in MDA (Model Driven Architecture) activities. Beyond that, we evaluated both ALaDIM language and editor using a CDN (Cognitive Dimensions of Notations) analysis. Finally, this work reports an experiment that validated the ALaDIM inspection method

MARISA-MDD: uma abordagem para transformações entre modelos orientados a aspectos: dos requisitos ao projeto detalhado

Aspect Oriented approaches associated to different activities of the software development process are, in general, independent and their models and artifacts are not aligned and inserted in a coherent process. In the model driven development, the various models and the correspondence between them are rigorously specified. With the integration of aspect oriented software development (DSOA) and model driven development (MDD) it is possible to automatically propagate models from one activity to another, avoiding the loss of information and important decisions established in each activity. This work presents MARISA-MDD, a strategy based on models that integrate aspect-oriented requirements, architecture and detailed design, using the languages AOV-graph, AspectualACME and aSideML, respectively. MARISA-MDD defines, for each activity, representative models (and corresponding metamodels) and a number of transformations between the models of each language. These transformations have been specified and implemented in ATL (Atlas Definition Language), in the Eclipse environment. MARISA-MDD allows the automatic propagation between AOV-graph, AspectualACME, and aSideML models. To validate the proposed approach two case studies, the Health Watcher and the Mobile Media have been used in the MARISA-MDD environment for the automatic generation of AspectualACME and aSideML models, from the AOV-graph model

Visual IMML: um perfil UML para a modelagem de interfaces de usuário

The software development processes proposed by the most recent approaches in Software Engineering make use old models. UML was proposed as the standard language for modeling. The user interface is an important part of the software and has a fundamental importance to improve its usability. Unfortunately the standard UML does not offer appropriate resources to model user interfaces. Some proposals have already been proposed to solve this problem: some authors have been using models in the development of interfaces (Model Based Development) and some proposals to extend UML have been elaborated. But none of them considers the theoretical perspective presented by the semiotic engineering, that considers that, through the system, the designer should be able to communicate to the user what he can do, and how to use the system itself. This work presents Visual IMML, an UML Profile that emphasizes the aspects of the semiotic engineering. This Profile is based on IMML, that is a declarative textual language. The Visual IMML is a proposal that aims to improve the specification process by using a visual modeling (using diagrams) language. It proposes a new set of modeling elements (stereotypes) specifically designed to the specification and documentation of user interfaces, considering the aspects of communication, interaction and functionality in an integrated manner

CrossMDA2: Uma abordagem para minimizar o problema da fragilidade de pointcuts na evolução de sistemas orientados a aspectos

This work proposes a model based approach for pointcut management in the presence of evolution in aspect oriented systems. The proposed approach, called conceptual visions based pointcuts, is motivated by the observation of the shortcomings in traditional approaches pointcuts definition, which generally refer directly to software structure and/or behavior, thereby creating a strong coupling between pointcut definition and the base code. This coupling causes the problem known as pointcut fragility problem and hinders the evolution of aspect-oriented systems. This problem occurs when all the pointcuts of each aspect should be reviewed due to any software changes/evolution, to ensure that they remain valid even after the changes made in the software. Our approach is focused on the pointcuts definition based on a conceptual model, which has definitions of the system's structure in a more abstract level. The conceptual model consists of classifications (called conceptual views) on entities of the business model elements based on common characteristics, and relationships between these views. Thus the pointcuts definitions are created based on the conceptual model rather than directly referencing the base model. Moreover, the conceptual model contains a set of relationships that allows it to be automatically verified if the classifications in the conceptual model remain valid even after a software change. To this end, all the development using the conceptual views based pointcuts approach is supported by a conceptual framework called CrossMDA2 and a development process based on MDA, both also proposed in this work. As proof of concept, we present two versions of a case study, setting up a scenario of evolution that shows how the use of conceptual visions based pointcuts helps detecting and minimizing the pointcuts fragility. For the proposal evaluation the Goal/Question/Metric (GQM) technique is used together with metrics for efficiency analysis in the pointcuts definition

Dos requisitos à arquitetura em linhas de produtos de software: uma estratégia de transformações entre modelos

The tracking between models of the requirements and architecture activities is a strategy that aims to prevent loss of information, reducing the gap between these two initial activities of the software life cycle. In the context of Software Product Lines (SPL), it is important to have this support, which allows the correspondence between this two activities, with management of variability. In order to address this issue, this paper presents a process of bidirectional mapping, defining transformation rules between elements of a goaloriented requirements model (described in PL-AOVgraph) and elements of an architectural description (defined in PL-AspectualACME). These mapping rules are evaluated using a case study: the GingaForAll LPS. To automate this transformation, we developed the MaRiPLA tool (Mapping Requirements to Product Line Architecture), through MDD techniques (Modeldriven Development), including Atlas Transformation Language (ATL) with specification of Ecore metamodels jointly with Xtext , a DSL definition framework, and Acceleo, a code generation tool, in Eclipse environment. Finally, the generated models are evaluated based on quality attributes such as variability, derivability, reusability, correctness, traceability, completeness, evolvability and maintainability, extracted from the CAFÉ Quality Model

Sistema Híbrido de Inferência Baseado em Análise de Componentes Principais e Redes Neurais Artificiais Aplicado a Plantas de Processamento de Gás Natural

Nowadays, where the market competition requires products with better quality and a constant search for cost savings and a better use of raw materials, the research for more efficient control strategies becomes vital. In Natural Gas Processin Units (NGPUs), as in the most chemical processes, the quality control is accomplished through their products composition. However, the chemical composition analysis has a long measurement time, even when performed by instruments such as gas chromatographs. This fact hinders the development of control strategies to provide a better process yield. The natural gas processing is one of the most important activities in the petroleum industry. The main economic product of a NGPU is the liquefied petroleum gas (LPG). The LPG is ideally composed by propane and butane, however, in practice, its composition has some contaminants, such as ethane and pentane. In this work is proposed an inferential system using neural networks to estimate the ethane and pentane mole fractions in LPG and the propane mole fraction in residual gas. The goal is to provide the values of these estimated variables in every minute using a single multilayer neural network, making it possibly to apply inferential control techniques in order to monitor the LPG quality and to reduce the propane loss in the process. To develop this work a NGPU was simulated in HYSYS R software, composed by two distillation collumns: deethanizer and debutanizer. The inference is performed through the process variables of the PID controllers present in the instrumentation of these columns. To reduce the complexity of the inferential neural network is used the statistical technique of principal component analysis to decrease the number of network inputs, thus forming a hybrid inferential system. It is also proposed in this work a simple strategy to correct the inferential system in real-time, based on measurements of the chromatographs which may exist in process under study

Estudo do genoma do vírus causador da mionecrose infecciosa em camarões e desenvolvimento de métodos para detecção de diferentes variantes

Shrimp farming is one of the activities that contribute most to the growth of global aquaculture. However, this business has undergone significant economic losses due to the onset of viral diseases such as Infectious Myonecrosis (IMN). The IMN is already widespread throughout Northeastern Brazil and affects other countries such as Indonesia, Thailand and China. The main symptom of disease is myonecrosis, which consists of necrosis of striated muscles of the abdomen and cephalothorax of shrimp. The IMN is caused by infectious myonecrosis virus (IMNV), a non-enveloped virus which has protrusions along its capsid. The viral genome consists of a single molecule of double-stranded RNA and has two Open Reading Frames (ORFs). The ORF1 encodes the major capsid protein (MCP) and a potential RNA binding protein (RBP). ORF2 encodes a probable RNA-dependent RNA polymerase (RdRp) and classifies IMNV in Totiviridae family. Thus, the objective of this research was study the IMNV complete genome and encoded proteins in order to develop a system differentiate virus isolates based on polymorphisms presence. The phylogenetic relationship among some totivirus was investigated and showed a new group to IMNV within Totiviridae family. Two new genomes were sequenced, analyzed and compared to two other genomes already deposited in GenBank. The new genomes were more similar to each other than those already described. Conserved and variable regions of the genome were identified through similarity graphs and alignments using the four IMNV sequences. This analyze allowed mapping of polymorphic sites and revealed that the most variable region of the genome is in the first half of ORF1, which coincides with the regions that possibly encode the viral protrusion, while the most stable regions of the genome were found in conserved domains of proteins that interact with RNA. Moreover, secondary structures were predicted for all proteins using various softwares and protein structural models were calculated using threading and ab initio modeling approaches. From these analyses was possible to observe that the IMNV proteins have motifs and shapes similar to proteins of other totiviruses and new possible protein functions have been proposed. The genome and proteins study was essential for development of a PCR-based detection system able to discriminate the four IMNV isolates based on the presence of polymorphic sites

Uma abordagem dirigida por modelos para desenvolvimento de middlewares auto-adaptativos para transmissão de fluxo de dados baseado em restrições de QoS

The use of middleware technology in various types of systems, in order to abstract low-level details related to the distribution of application logic, is increasingly common. Among several systems that can be benefited from using these components, we highlight the distributed systems, where it is necessary to allow communications between software components located on different physical machines. An important issue related to the communication between distributed components is the provision of mechanisms for managing the quality of service. This work presents a metamodel for modeling middlewares based on components in order to provide to an application the abstraction of a communication between components involved in a data stream, regardless their location. Another feature of the metamodel is the possibility of self-adaptation related to the communication mechanism, either by updating the values of its configuration parameters, or by its replacement by another mechanism, in case of the restrictions of quality of service specified are not being guaranteed. In this respect, it is planned the monitoring of the communication state (application of techniques like feedback control loop), analyzing performance metrics related. The paradigm of Model Driven Development was used to generate the implementation of a middleware that will serve as proof of concept of the metamodel, and the configuration and reconfiguration policies related to the dynamic adaptation processes. In this sense was defined the metamodel associated to the process of a communication configuration. The MDD application also corresponds to the definition of the following transformations: the architectural model of the middleware in Java code, and the configuration model to XML

Estudo do genoma do vírus causador da mionecrose infecciosa em camarões e desenvolvimento de métodos para detecção de polimorfismos

Shrimp farming is one of the activities that contribute most to the growth of global aquaculture. However, this business has undergone significant economic losses due to the onset of viral diseases such as Infectious Myonecrosis (IMN). The IMN is already widespread throughout Northeastern Brazil and affects other countries such as Indonesia, Thailand and China. The main symptom of disease is myonecrosis, which consists of necrosis of striated muscles of the abdomen and cephalothorax of shrimp. The IMN is caused by infectious myonecrosis virus (IMNV), a non-enveloped virus which has protrusions along its capsid. The viral genome consists of a single molecule of double-stranded RNA and has two Open Reading Frames (ORFs). The ORF1 encodes the major capsid protein (MCP) and a potential RNA binding protein (RBP). ORF2 encodes a probable RNA-dependent RNA polymerase (RdRp) and classifies IMNV in Totiviridae family. Thus, the objective of this research was study the IMNV complete genome and encoded proteins in order to develop a system differentiate virus isolates based on polymorphisms presence. The phylogenetic relationship among some totivirus was investigated and showed a new group to IMNV within Totiviridae family. Two new genomes were sequenced, analyzed and compared to two other genomes already deposited in GenBank. The new genomes were more similar to each other than those already described. Conserved and variable regions of the genome were identified through similarity graphs and alignments using the four IMNV sequences. This analyze allowed mapping of polymorphic sites and revealed that the most variable region of the genome is in the first half of ORF1, which coincides with the regions that possibly encode the viral protrusion, while the most stable regions of the genome were found in conserved domains of proteins that interact with RNA. Moreover, secondary structures were predicted for all proteins using various softwares and protein structural models were calculated using threading and ab initio modeling approaches. From these analyses was possible to observe that the IMNV proteins have motifs and shapes similar to proteins of other totiviruses and new possible protein functions have been proposed. The genome and proteins study was essential for development of a PCR-based detection system able to discriminate the four IMNV isolates based on the presence of polymorphic sites

Desenvolvimento e validação de método analítico para determinação de WE010, WE014 e WE017

The synthetic guanylhydrazones WE010 (3,5-di-tert-butil-4-hidroxibenzaldehyde-guanylhydrazone), WE014 (4-bifenilcarboxialdehydeguanylhydrazone) and WE017 (3,4-diclorobenzaldehydeguanylhydrazone) showed high cytotoxic activity in terms of percentage inhibition of cancer cells growth. However, further progress in the development of these drug candidates requires precise and convenient methods for their qualitative and quantitative analyses. The aim of this study was to develop and validate High Performance Liquid Chromatography with diode-array detection (HPLC-DAD) and Ultra Fast Liquid Chromatography with diode-array detection (UFLC-DAD) methods suitable for as simultaneous as isolated determination of studied guanylhydrazones, based on the optimization of chromatographic parameters and obtaining reduced detection times. The chromatographic analyses of analytes by HPLC were performed on C18 ACE analytical column (150 mm x 4.6 mm), with a particle size of 5.0 μm. Among all the conditions assayed, the best results of separation were obtained with a mixture of methanol:water (60:40, v/v) as the mobile phase at a flow rate 1.5mL/min and pH of 3.5 adjusted at acetic acid. The UFLC method was developed by experimetal desing techniques in order to find optimal chromatographic analytical conditions, which were achieved on XR-ODS analytical column (50 mm x 3.0 mm), with a particle size of 2,2 μm, maintained at 25 ºC. The mobile phase was consisted of methanol:water (65:35, v/v) with 0.1% triethylamine (TEA) and pH of 3.5 adjusted at acetic acid, at a flow rate 0.5 mL/min. The procedure were validated following evaluating parameters such as specificity, linearity, limits of detection (LD) and quantification (LQ), precision, accuracy and robustness, giving results within the acceptable range. Although the UFLC method shows better sensitivity (lower values of LD and LQ), robustness (lower rates of relative standard deviation) and minimize spending time and solvent, both developed methods were adequately applied to the analysis of guanylhydrazones molecules, may be used in routine of quality control laboratories. Keywords: guanylhydrazones, HPLC/DAD, UFLC/DAD, validation of analitical method