BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B

The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers

Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Verificación Formal de Sistemas basada Formal Software Verification based on Automated Analysisen Análisis Automático.

Identificación y caracterización del problema. Uno de los problemas más importantes asociados con la construcción de software es la corrección del mismo. En busca de proveer garantías del correcto funcionamiento del software, han surgido una variedad de técnicas de desarrollo con sólidas bases matemáticas y lógicas conocidas como métodos formales. Debido a su naturaleza, la aplicación de métodos formales requiere gran experiencia y conocimientos, sobre todo en lo concerniente a matemáticas y lógica, por lo cual su aplicación resulta costosa en la práctica. Esto ha provocado que su principal aplicación se limite a sistemas críticos, es decir, sistemas cuyo mal funcionamiento puede causar daños de magnitud, aunque los beneficios que sus técnicas proveen son relevantes a todo tipo de software. Poder trasladar los beneficios de los métodos formales a contextos de desarrollo de software más amplios que los sistemas críticos tendría un alto impacto en la productividad en tales contextos. Hipótesis. Contar con herramientas de análisis automático es un elemento de gran importancia. Ejemplos de esto son varias herramientas potentes de análisis basadas en métodos formales, cuya aplicación apunta directamente a código fuente. En la amplia mayoría de estas herramientas, la brecha entre las nociones a las cuales están acostumbrados los desarrolladores y aquellas necesarias para la aplicación de estas herramientas de análisis formal sigue siendo demasiado amplia. Muchas herramientas utilizan lenguajes de aserciones que escapan a los conocimientos y las costumbres usuales de los desarrolladores. Además, en muchos casos la salida brindada por la herramienta de análisis requiere cierto manejo del método formal subyacente. Este problema puede aliviarse mediante la producción de herramientas adecuadas. Otro problema intrínseco a las técnicas automáticas de análisis es cómo se comportan las mismas a medida que el tamaño y complejidad de los elementos a analizar crece (escalabilidad). Esta limitación es ampliamente conocida y es considerada crítica en la aplicabilidad de métodos formales de análisis en la práctica. Una forma de atacar este problema es el aprovechamiento de información y características de dominios específicos de aplicación. Planteo de objetivos. Este proyecto apunta a la construcción de herramientas de análisis formal para contribuir a la calidad, en cuanto a su corrección funcional, de especificaciones, modelos o código, en el contexto del desarrollo de software. Más precisamente, se busca, por un lado, identificar ambientes específicos en los cuales ciertas técnicas de análisis automático, como el análisis basado en SMT o SAT solving, o el model checking, puedan llevarse a niveles de escalabilidad superiores a los conocidos para estas técnicas en ámbitos generales. Se intentará implementar las adaptaciones a las técnicas elegidas en herramientas que permitan su uso a desarrolladores familiarizados con el contexto de aplicación, pero no necesariamente conocedores de los métodos o técnicas subyacentes. Materiales y métodos a utilizar. Los materiales a emplear serán bibliografía relevante al área y equipamiento informático. Métodos. Se emplearán los métodos propios de la matemática discreta, la lógica y la ingeniería de software. Resultados esperados. Uno de los resultados esperados del proyecto es la individualización de ámbitos específicos de aplicación de métodos formales de análisis. Se espera que como resultado del desarrollo del proyecto surjan herramientas de análisis cuyo nivel de usabilidad sea adecuado para su aplicación por parte de desarrolladores sin formación específica en los métodos formales utilizados. Importancia del proyecto. El principal impacto de este proyecto será la contribución a la aplicación práctica de técnicas formales de análisis en diferentes etapas del desarrollo de software, con la finalidad de incrementar su calidad y confiabilidad. A crucial factor for software quality is correcteness. Traditionally, formal approaches to software development concentrate on functional correctness, and tackle this problem basically by being based on well defined notations founded on solid mathematical grounds. This makes formal methods better suited for analysis, due to their precise semantics, but they are usually more complex, and require familiarity and experience with the manipulation of mathematical definitions. So, their acceptance by software engineers is rather restricted, and formal methods applications have been confined to critical systems. Nevertheless, it is obvious that the advantages that formal methods provide apply to any kind of software system. It is accepted that appropriate software tool support for formal analysis is essential, if one seeks providing support for software development based on formal methods. Indeed, some of the relatively recent sucesses of formal methods are accompanied by good quality tools that automate powerful analysis mechanisms, and are even integrated in widely used development environments. Still, most of these tools either concentrate on code analysis, and in many cases are still far from being simple enough to be employed by software engineers without experience in formal methods. Another important problem for the adoption of tool support for formal methods is scalability. Automated software analysis is intrinsically complex, and thus techniques do not scale well in the general case. In this project, we will attempt to identify particular modelling, design, specification or coding activities in software development processes where to apply automated formal analysis techniques. By focusing in very specific application domains, we expect to find characteristics that might be exploited to increase the scalability of the corresponding analyses, compared to the general case.

Análisis de los valores de una organización de educación no formal : Pioneros.

1) Identificar lo valores que posee el Programa de Prevención de las Dificultades Psicosociales de la Infancia en Medio Abierto desarrollado por Pioneros.2) Sensibilizar a los profesionales y educadores del Programa de educación en medio abierto sobre el tema de los valores. Las pretensiones de esta investigación son las siguientes: 1) Ofrecer a Pioneros una descripción de sus valores para que tomen conciencia de los mismos con el fin de que todos sus miembros clarifiquen sus valores y lleguen a planteamientos comunes en este tema. 2) Presentar a la sociedad riojana una visión de los valores que Pioneros prioriza en su actividad socio-educativa con el fin de prevenir las conductas inadaptadas. 3) Ofrecer a otras organizaciones que trabajan en el ámbito de la educación no formal la posibilidad de clarificar sus valores utilizando una versión resumida de la clasificación de Hall-Tonna. 4) Mostrar una herramienta informática, programa NUD*IST, que facilita el análisis cualitativo y que puede ser utilizada por los profesionales de una organización para estudiar sus propias actuaciones. Es mixta, primando la cualitativa sobre la cuantitativa. Se centra en el estudio de casos con el enfoque constructivista/cualitativo. Concretamente se han utilizado el análisis de documentos relevantes escritos por la entidad y técnicas de la entrevista de estructura abierta. El programa NUD*IST, como herramienta de codificación y realización de agrupamiento y operaciones de búsqueda en los textos (tanto escritos como los orales, que han sido trascritos), con el fin de facilitar el análisis. La clasificación de valores Hall-Tonna, que contiene 125 palabras-valor, organizadas en cuatro fases. Agrupadas en dos grandes apartados referidos a: 1) El Programa de Prevención de las Dificultades Psicosociales de la Infancia en Medio Abierto: a) Todas las fases de la clasificación de valores Hall-Tonna están representadas en alguna medida en los documentos estudiados, si bien, la fase I y IV son las menos frecuentes. Las fases I y II son las más representadas por tratarse de una organización dedicada a la educación no formal con una trayectoria en el ámbito de la inadaptación psicosocial larga y planificada. Existe coherencia entre los documentos estudiados (programación, estatutos, memoria y entrevistas) lo que demuestra un filosofía consensuada con una serie de valores comunes. B) Los 125 valores de Hall-Tonna se podrían reducir a 61, con el fin de trabajar de forma más ágil en investigaciones posteriores sobre la misma entidad u otras de características similares. c) El estudio detallado de las entrevistas muestra que el tema de los valores no ha sido objeto de reflexión ni formación concreta en el seno de la entidad y, por ello, se observa la necesidad de potenciar la unicidad de criterios de valor para que se transfieran con claridad cuando haya cambios de profesionales. 2) En cuanto a la forma: a) La clasificación de valores Hall-Tonna es un instrumento que ofrece grandes ventajas pare el estudio de los valores, a pesar de su complejidad, tanto en organizaciones de educación formal como no formal. b) El programa informático NUD*IST facilita los análisis cualitativos, porque permite manejar gran cantidad de textos, codificándolos y relacionando su información. Es destacable que permite comparar situaciones y documentos de origen dispar.

Pulverização em CDA 250 herbicida pendimethalin na cultura do arroz de sequeiro

Foi estudada a viabilidade de utilização da pulverização CDA 25C, na aplicação do herbicida em pré-emergência na cultura do arroz de sequeiro. O herbicida empregado foi o pendimethalin nas doses de 0,0; 1,5; 2,0; 2,5 e 3,0 litro s/ha da formulação comercial a 50%. A pulverização convencional foi efetuada com bicos 11003 com consumo de 200 litros de calda per hectare. O processo CDA 250 foi aplicado por meio de bico rotativo (Micromax) com dois níveis de consumo de calda : 50 1/ha e 27 1/ha. Os resultados mostraram que: a) - o método CDA 250 proporciona controle dc mato e produtividade de arroz equivalentes ao método convencional; b) para o bico Micromax, a aplicação da formulação comercial de pendimethalin a 50% com vazão de 0,48 1/min./bico, a distância entre bicos deve ser de 1,75 m e para a vazão de 0,96 1/min./bloco, essa distancia deve ser de 1,90 m; c)- a aplicação do pendimethalin 50% C.E. pelo processo CDA 250, empregando 27 litros de calda por hectare foi o processo mais interessante por oferecer vantagens logísticas apreciáveis.

Indeterminação e fenômenos fronteiriços: considerações segundo o ponto de vista do pragmatismo peirceano

O pragmatismo, como método formal, nos fornece uma importante arena para discussões a respeito do modo pelo qual conceitos podem ser construídos, independentemente de qualquer posição antropocêntrica ou linguística. O presente trabalho tem por finalidade efetuar uma discussão sobre a máxima pragmática e a tese sobre a indeterminação do significado (meaning) que ela traz consigo. Ou seja, busca-se entender o trânsito que há entre o indefinido e o definido, entre o indeterminado e o determinado, bem como algumas fronteiras intermediárias encontradas nos processos de determinação relativa do conceito.

Plan exportador software de encriptación y firma digital de documentos altamente sensibles

Este plan exportador proyectado a un plazo de 3 años, servirá a ITAC IT APPLICATIONS CONSULTING S.A. para direccionar sus actividades en el mercado internacional para los años 2009, 2010, 2011. La prioridad de los 2 primeros años será el mejoramiento interno de la empresa, que será la aplicación de estrategias en diferentes campos como: capital humano, capital intelectual, capital cultural, crecimiento económico, estrategia comercial en el área internacional, construcción de capital financiero para la generación de ingresos. Para tener participación en mercados internacionales, mostrar su potencial exportador y lograr las expectativas de crecimiento de las ventas independientes a las obtenidas en el marcado local; pretende empezar en el año 2009, en el mercado Peruano con exportaciones por $36.000 USD correspondiente a 30 unidades, aumentando a $ 72000 USD con 60 unidades en el 2010 y $ 108000 USD y 90 unidades en el 2011. El Servicio a exportar fue “SecureFile” a partir del cual se definieron factores de éxito como lo son las ventajas competitivas del producto en sí mismo enumeradas a continuación: 1) Precio muy competitivo en el mercado, 2) Automatización del proceso de intercambio de información, 3) Software basado en estándares, 4) Se ejecuta en cualquier sistema operativo. A su vez se realizaron consultorías donde se diagnosticó todas las áreas de la empresa arrojando algunos resultados: La estructura organizacional esta bien definida, pero por su crecimiento y necesidad de incluir nuevo personal, no hay claridad en las funciones dentro del organigrama y depende totalmente de la dirección general. Por esto la gerencia debe estructurar mejor los departamentos comerciales creando nuevos cargos de acuerdo al proceso de internacionalización. Las políticas de personal se trabajan de manera informal con criterios validos para promover trabajadores (mérito, antigüedad, etc.), se realizan actualizaciones Tecnológicas mensuales, reconocimiento y participación en la empresa a sus funcionarios, excelentes relaciones personales que permiten hacer evaluaciones de desempeño acorde a las metas, gran variedad de motivación y responsabilidad social encaminada a los niños de bajos recursos. Aunque se debe crear un área de gestión humana y definir la frecuencia de las capacitaciones. Los ingresos son provenientes de la prestación de servicios de IT con incrementando de 256% durante los tres años anteriores para obtener $ 2`032.784.683 millones de pesos en el 2007. El nivel de endeudamiento también ha ido en aumento, por la necesidad de capacidad instalada, contrataciones de personal, el cumplimiento de requisitos del mercado y la necesidad generar buena imagen crediticia con entidades financieras. Cuenta con un musculo financiero para respaldar sus obligaciones inmediatas con $4,42 por $1 comprometido en el 2007 a pesar de ser el año con mayor nivel de endeudamiento arrojando pasivos corrientes por $127.715.281,37. Los cuatro socios cuentan con un comportamiento de 164,67% (2006) y 132,97% (2007) de rendimiento de sobre la inversión antes de impuestos. Para este año más del 95% de su información financiera y contable se maneja de manera sistematizada. El área Financiera de la empresa no es la más débil, pero no existe un departamento financiero con un solo responsable a la cabeza, por esto deben destinar un área separada de la administrativa con un asesor financiero que tenga disponibilidad de 100%. En el caso particular del proyecto de exportación los costos de producción se centran en SecureFile versión 3.0 que no representa costos marginales, ya que la replica de este software puede hacerse cuantas veces sea requerido sin afectar en ninguna proporción los costos. La empresa no utiliza un método formal para calcular sus costos de operación y desarrollo de programas. Pero ha desarrollado un sistema de evaluación de costos en tablas de Excel que de manera organizada logran un costeo acorde a sus necesidades específicas. Para la selección de los países: objetivo, alterno y contingente; se realizó una matriz de Selección de 6 países basados en la exigencia gubernamental en términos de seguridad de la información vía internet, y la percepción de los empresarios, competencia y otros factores económicos; arrojando como resultado a Perú, Costa Rica y México.

Creatividad y analogía.

Se estudia la creatividad en niños, jóvenes y adultos, y se analizan los pasos para trabajar de forma creativa. La creatividad constituye la vía del avance científico y humanístico, la esencia misma de la investigación que en la mayoría de los casos avanza por analogía, creando. La creatividad, como método de conocimiento, engloba el método utilitarista y el método formal. El primero, no es una forma de pensamiento, sino la ausencia del mismo; nos dice para qué sirve una cosa y supone un freno a la reflexión. Por el contrario, la tendencia formalista, es un tipo de pensamiento que define a personas, ideas, conceptos, fenómenos e instrumentos, por su forma externa. Se incluyen ejemplos que ayudan a clarificar lo expuesto en el artículo.

O processo de desenvolvimento do produto e o planejamento do suporte ao cliente

As empresas estão cada vez mais buscando atingir uma posição de liderança e ser um referencial perante os consumidores no pós-venda. Para isso é necessário que todas as ações necessárias para elaborar um Plano de Suporte ao Cliente ocorram desde o início dos projetos de desenvolvimento de novos produtos. Neste trabalho estudou-se e desenvolveu-se a metodologia do CSP (Customer Support Process), que incorporada a cada fase do PDP (Product Delivery Process), estabelece os requesitos e necessidades da área do Suporte ao Cliente no desenvolvimento de um novo produto. É sabido que se o Suporte ao Cliente não for considerado, o novo produto terá uma baixa aceitação por parte do cliente e consequentemente um pobre desempenho de mercado. Como parte da justificativa do desenvolvimento deste trabalho, verificou-se quais os principais problemas enfrentados atualmente. Problemas estes decorrentes da não aplicação de uma metodologia para planejamento das atividades necessárias para oferecer um bom Suporte ao Cliente no momento do lançamento de novos produtos. Conhecendo as deficiências e problemas atualmente enfrentados pela área de Suporte ao Cliente, foi possível desenvolver e adaptar o Processo de Suporte ao Cliente, às necessidades do departamento e sua estrutura organizacional Com a implantação completa deste método, pretende-se minimizar problemas enfrentados no dia a dia do Suporte ao Cliente, principalmente os relacionados a disponibilidade de informações técnicas atualizadas, treinamento, peças de reposição e ferramentas especiais para a rede de concessionários. Como finalização do trabalho é traçado um comparativo entre o resultado previsto do novo método versus o resultado atual obtido, onde não se aplicava nenhum método formal para o Planejamento do Suporte ao Cliente no desenvolvimento do produto.

O problema do balanceamento de linhas de montagem

A finalidade desta monografia, é a de efetuar uma pesquisa dos métodos desenvolvidos para o balanceamento de linhas de montagem e obter informações para verificar se a indústria usa realmente tais métodos. Normalmente o balanceamento de linhas de montagem é realizado apenas com o uso do bom senso e o método de tentativas erros sem maiores considerações, constitui ainda objetivo desta monografia, determinar o grau de otimização conseguido em algumas fábricas para o balanceamento, com vistas a verificação se e ou não compensador o uso de algum método formal, e no caso afirmativo, qual ou quais, o presente trabalho, possui ainda a finalidade adicional de transferir conhecimentos necessários para as fábricas pesquisadas, possibilitando a introdução de tais métodos e de acompanhar o inicio da implantação resolvendo os problemas decorrentes. Com tal pesquisa, poderiam ser atingidas tanto as metas teóricas, ou seja, o conhecimento dos métodos desenvolvidos sobre balanceamentos de linhas de montagem, como ainda aquelas operacionais quanto à sua aplicação à realidade industrial.

Degradação do PMMA através da reação despolimerização uitlizando catalisadores de óxidos mistos

In this work, mixed oxides were synthesized by two methods: polymeric precursor and gel-combustion. The oxides, Niquelate of Lanthanum, Cobaltate of Lanthanum and Cuprate of Lanthanum were synthesized by the polymeric precursor method, and treated at 300 º C for 2 hours, calcined at 800 º C for 6h in air atmosphere. In gel-combustion method were produced and oxides using urea and citric acid as fuel, forming for each fuel the following oxides Ferrate of Lanthanum, Cobaltato of Lanthanum and Ferrato of Cobalt and Lanthanum, which were submitted to the combustion process assisted by microwave power maximum of 10min. The samples were characterized by: thermogravimetric analysis, X-ray diffraction; fisisorção of N2 (BET method) and scanning electron microscopy. The reactions catalytic of depolymerization of poly (methyl methacrylate), were performed in a reactor of silica, with catalytic and heating system equipped with a data acquisition system and the gas chromatograph. For the catalysts synthesized using the polymeric precursor method, the cuprate of lanthanum was best for the depolymerization of the recycled polymer, obtaining 100% conversion in less time 554 (min), and the pure polymer, was the Niquelate of Lanthanum, with 100% conversion in less time 314 (min). By gel-combustion method using urea as fuel which was the best result obtained Ferrate of Lanthanum for the pure polymer with 100% conversion in less time 657 (min), and the recycled polymer was Cobaltate of Lanthanum with 100 % conversion in less time 779 (min). And using citric acid to obtain the best result for the pure polymer, was Ferrate of Lanthanum with 100% conversion in less time 821 (min and) for the recycled polymer, was Ferrate of Lanthanum with 98.28% conversion in less time 635 (min)

Uma arquitetura para sistemas supervisórios industriais e sua aplicação em processos de elevação artificial de petróleo

The using of supervision systems has become more and more essential in accessing, managing and obtaining data of industrial processes, because of constant and frequent developments in industrial automation. These supervisory systems (SCADA) have been widely used in many industrial environments to store process data and to control the processes in accordance with some adopted strategy. The SCADA s control hardware is the set of equipments that execute this work. The SCADA s supervision software accesses process data through the control hardware and shows them to the users. Currently, many industrial systems adopt supervision softwares developed by the same manufacturer of the control hardware. Usually, these softwares cannot be used with other equipments made by distinct manufacturers. This work proposes an approach for developing supervisory systems able to access process information through different control hardwares. An architecture for supervisory systems is first defined, in order to guarantee efficiency in communication and data exchange. Then, the architecture is applied in a supervisory system to monitor oil wells that use distinct control hardwares. The implementation was modeled and verified by using the formal method of the Petri networks. Finally, experimental results are presented to demonstrate the applicability of the proposed solution

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