Uma metodologia para verificação de modelos de sistemas de comércio eletrônico (A model checking methodology for e-commerce systems)

• Main Author: Adriano César Machado Pereira
• Other Authors: Wagner Meira Junior
• Format: Others
• Language: Portuguese
• Published: Universidade Federal de Minas Gerais 2002
• Online Access: http://hdl.handle.net/1843/BUBD-9KJNFH

=== Electronic commerce is an important application that has evolved significantly in recent past. However, electronic commerce systems are complex and difficult to be designed correctly. Current most approaches are ad-hoc, frequently leading to expensive and unreliable systems that may take a long time to implement due to the great amount of errors. Moreover, guaranteeing the correctness of an e-commerce system is not an easy task due to the great amount of scenarios where subtle errors may occur. Such task is quite hard and laborious if only tests and simulation, common techniques for system validation, are used. In this work we propose a methodology that uses formal-method techniques, specifically symbolic model checking, to design electronic commerce applications and to automatically verify that these designs satisfy properties such as atomicity, isolation, and consistency. Using the proposed methodology, the designer is able to identify errors early in the design process and correct them before they propagate to later stages. Thus, its possible to generate more reliable applications, developed faster and at low costs. In order to demonstrate the applicability and feasibility of the technique, we have modeled and verified a virtual store m which multiple buyers compete for product items. For instance, the verification process pointed out a concurrency control error which allowed the same item to be sold twice. The proposed method can be applied in general e-commerce systems, where the business rules can be modeled by state transitions of the items on sale. As the method is based on CTL-formulas, the business rules should be represented by them, what can be considered a limitation of the method. We are currently studying other features of electronic commerce systems that we have not yet been formalized, as well as the possibility of generating the actual code that will implement the system from its specification. In this context, we have been developing a set of design patterns to be used in the design and verification process of e-commerce systems. The idea is to define a model checking pattern hierarchy, which specifies patterns to construct and verify the formal model of e-commerce systems. We consider this research the first step for the development of a framework, which will integrate the methodology, an e-commerce specification language based on business rules, and a model checker. A future research is to apply our methodology in other application areas, such as mobile e-commerce and telecommunications. === Comércio eletrônico é uma importante área de aplicação associada à computação que tem evoluído significativamente nos últimos anos. Entretanto, sistemas de comércio eletrônico são complexos e difíceis de serem projetados corretamente. Atualmente, a maioria das abordagens é ad-hoc, o que normalmente torna os sistemas menos confiáveis e implica em alto custo em termos de tempo e recursos. Além disso, garantir a corretude de um sistema de comercio eletrônico não é tarefa trivial devido à grande variedade de erros, muitos deles muito sutis. Tal tarefa é complexa e trabalhosa se apenas testes e simulação, técnicas comuns de validação de sistemas, são utilizados. Neste trabalho propõe-se uma metodologia que utiliza métodos formais, especificamente verificação simbólica de modelos, para projetar aplicações de comércio eletrônico e verificar automaticamente se suas regras de negócio são satisfeitas. Usando a metodologia proposta, o projetista é capaz de identificar, antecipadamente, erros no processo de desenvolvimento do projeto e corrigi-los antes que se propaguem a estágios posteriores da implementação. Dessa forma, torna-se possível gerar aplicações mais confiáveis, desenvolvidas mais rapidamente e a baixo custo. A fim de demonstrar a aplicabilidade e a praticabilidade da técnica proposta, modelou-se e verificouse uma loja virtual, na qual múltiplos compradores competem para adquirir itens de um produto. A utilização de verificação automática se mostrou de extrema importância, pois indicou erros difíceis de serem detectados durante o projeto da aplicação como, por exemplo, uma falha do controle de concorrência que permitia que o mesmo artigo fosse vendido para clientes distintos. A metodologia proposta pode ser aplicada em sistemas de comércio eletrônico em geral, onde as regras de negócio podem ser modeladas através de transições no estado dos itens a venda. Como o método proposto é baseado em fórmulas CTL, as regras de negócio devem ser representadas através das mesmas, o que pode ser considerado uma limitação da metodologia. Estamos estudando outras características dos sistemas de comércio eletrônico que ainda não foram formalizadas, assim como a possibilidade de geração do atual código que implementa o sistema a partir de sua especificação. Neste contexto, estamos desenvolvendo um conjunto de padrões de projeto a serem utilizados no projeto e verificação de sistemas de comércio eletrônico. A idéia principal é definir uma hierarquia de padrões para verificação de modelos, que especifique padrões para construção e verificação de modelos formais de comércio eletrônico. Consideramos esse trabalho o primeiro passo para o desenvolvimento de um ambiente que integre a metodologia, uma linguagem de especificação de sistemas de comércio eletrônico baseada em regras de negócio, e um verificador de modelos. Um trabalho futuro é aplicar a metodologia proposta em outras áreas, tais como comércio eletrônico móvel e telecomunicações.