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

Universidade Federal do Rio Grande do Norte

O desenvolvimento de sistemas baseados em componentes revolucionou o processo de desenvolvimento de software, facilitando a manutenção, trazendo mais confiabilidade e reutilização. Porém, mesmo com todas as vantagens atribuídas ao componente, é necessário uma análise detalhada de sua composição. Realizar verificação a partir de testes de software não é o suficiente para se ter uma composição segura, pois esses não são baseados em modelos semânticos formais nos quais podemos descrever precisamente o comportamento do sistema. Nesse contexto, os métodos formais oferecem a possibilidade de especificarmos sistemas de forma precisa, através de notações com forte base matemática, trazendo, entre outros benefícios, mais segurança. O método formal CSP possibilita a especificação de sistemas concorrentes e verificação de propriedades inerentes a tais sistemas, bem como refinamento entre diferentes modelos. Existem abordagens que aplicam restrições usando CSP, para verificar o comportamento da composição entre componentes, auxiliando a verificação desses componentes antecipadamente. Visando auxiliar esse processo, tendo em vista que o mercado de software busca cada vez mais automação, minimizando trabalhos e trazendo agilidade nos negócios, este trabalho apresenta uma ferramenta que automatiza a verificação da composição entre componentes, onde o conjunto de verificações CSP impostas é gerado e verificado internamente, oculto para o usuário. Dessa forma, através de uma interface simples, a ferramenta BTS (BRIC-Tool-Suport) ajuda a criar e compor componentes, prevendo, com antecedência, comportamentos indesejáveis no sistema, como deadlocks