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

Abstract

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 thiscontext, 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.