Abstract
Electronic commerce is an important application that has evolved significantly recently. It gives companies the possibility of reaching an unprecedented number of clients at very low cost. However, electronic commerce systems are complex and difficult to be correctly designed. Currently, most approaches are ad-hoc, and frequently lead to expensive, unreliable systems that may take a long time to implement. 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, it is 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 in which multiple buyers compete for product items. The model verified has more than 1023 states and verification has been completed in few minutes. For instance, the verification process pointed out a concurrency control error which allowed the same item to be sold twice.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bolignano. Towards the formal verification of electronic commerce protocols. In PCSFW: Proceedings of The 10th Computer Security Foundations Workshop (1997), IEEE Computer Society Press.
Clarke, E. M., Grumberg, O., AND Peled, D. A.Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
Department, S. L. Model checking the secure electronic transaction (set) protocol. In Proceedings of the 7th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (1998).
Dwyer, M. B., Avrunin, G. S., AND Corbett, J. C. Property specification patterns for finite-state verification. In 2nd Workshop on Formal Methods in Software Practice (March 1998).
Dwyer, M. B., Avrunin, G. S., AND Corbett, J. C. Patterns in property specifications for finite-state verification. In 21st International Conference on Software Engineering (May 1999).
Gurgens, S., Lopez, J., AND Peralta, R. Efficient detection of failure modes in electronic commerce protocols. In DEXA Workshop (1999), pp. 850–857.
McMillan, K. L.Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Pittsburgh, PA, 1992.
McMillan, K. L.Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.
Meira Jr., W., Murta, C. D., Campos, S. V. A., AND Neto, D. O. G.Sistemas de Comercio Eletronico, Projeto e Desenvolvimento. Campus, 2002.
Wang, W., Hidvégi, Z., Bailey, A., AND Whinston, A. E-process design and assurance using model checking. In IEEE Computer (Oct. 2000).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pereira, A., Song, M., Gorgulho, G., Meira, W., Campos, S. (2002). A Formal Methodology to Specify E-commerce Systems. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_20
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive