UML-CAFE: um ambiente para especificar e verificar sistemas de comércio eletrônico

Abstract

Since the last decade the internet has been growing exponentially. As a new computational infra-structure has became available, new distributed applications which were previously too expensive or too complex have become common. E-commerce systems, for example, has simplified the access to goods and services and has revolutionized the economy as a whole. However, web applications tends to generate complex systems. As new services are created, the frequency with which errors appear has increased significantly. Besides, ensuring the correctness of the software design at the earliest stage, a problem known as design validation, is still a major challenge in any system development process. The most popular methods for design validation are still the techniques of simulation and testing. Although effective in the early stages of debugging, their effectiveness drops quickly as the design becomes cleaner. New approaches can be used in order to improve the quality of the software and to guarantee the integrity of critical systems. Formal Methods is one such approach. Unfortunately, it is not a simple task to apply them. Acquiring a level of expertise can represent an obstacle to their adoption in the software development process. Usually, to build a complex system the developer abstracts different views of it, builds models using some notation, verifies that the models satisfy the requirements, and gradually adds details to transform the models into an implementation. In this context, an unified notation plays an important role once a symbol can mean different things to different people. UML-CAFE is an environment that aggregates a model checking approach, an unified modeling language, a set of transformation patterns, and a methodology to specify and automatically verify transactional applications. Using the proposed environment the designer is able to automatically identify errors in early stages of the software development and correct them before they propagate to later stages. Thus, it is possible to generate more reliable applications which is developed faster and at low costs.