×

The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems. (English) Zbl 1104.68528

Summary: Electronic commerce is an important application that has evolved significantly recently. However, electronic commerce systems are complex and difficult to be correctly designed. Guaranteeing the correctness of an e-commerce system is not an easy task due to the great amount of scenarios where errors occur, many of them very subtle. In this work we presents a methodology that uses formal-method techniques, specifically symbolic model checking, to design electronic commerce applications and to automatically verify them. Also, a model checking pattern hierarchy has been developed – it specifies patterns to construct and verify the formal model of e-commerce systems. We consider this research the first step to the development of a framework, which will integrate the methodology, an e-commerce specification language based on business rules, and a model checker.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68U99 Computing methodologies and applications

Software:

NuSMV
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Avrunin, G. S., Buy, U. A., Corbett, J. C., Dillon, L. K., & Wileden, J. C. (1991). Automated analysis of concurrent systems with the constrained expression toolset. IEEE Transactions on Software Engineering, 17(11), 1204–1222. · Zbl 05114671 · doi:10.1109/32.106975
[2] Bolignano. (1997). Towards the formal verification of electronic commerce protocols. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop.
[3] Bowen, J. P. & Hinchey, M. G. (1995). Seven more myths of formal methods. IEEE Software 12(3), 34–41. · Zbl 05102049 · doi:10.1109/52.391826
[4] Bryant, R. E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8). · Zbl 0593.94022
[5] Campos, S., Clarke, E., Marrero, W., & Minea. M. (1995). Verifying the performance of the PCI local bus using symbolic techniques. In: International Conference on Computer Design.
[6] Campos, S. V., Clarke, E. M., Marrero, W., & Minea, M. (1995). Timing analysis of industrial real-time systems. In: Workshop on Industrial-strength Formal specification Techniques.
[7] Campos, S. V., Clarke, E. M., Marrero, W., Minea, M., & Hiraishi H. (1994). Computing quantitative Characteristics of finite-state real-time systems. In: IEEE Real-Time Systems Symposium.
[8] Cimatti, A., Clarke, E., Giunchiglia, F., & Roveri M. (1998). NuSMV: A reimplementation of smv.
[9] Cimatti, A., Clarke, E., Giunchiglia, F., & Roveri M. (1999). NuSMV: A new symbolic model verifier. · Zbl 1046.68587
[10] Cimatti, A., & Roveri M. (1997). User Manual.
[11] Clarke, E. M., Emerson, E. A., & Sistla A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8(2), 244–263. · Zbl 0591.68027 · doi:10.1145/5397.5399
[12] Clarke, E. M., Grumberg, O., & Peled D. A. (1999). Model checking. Cambridge, Massachusetts: The MIT Press.
[13] Rosenblum, D. (1996). Formal methods and testing: Why the state-of-the-art is not the state-of-the-practice. ACM SIGSOFT Software Engineering Notes 21(4).
[14] Department, S. L. (1998). 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.
[15] Dwyer, M. B., Avrunin, G. S., & Corbett J. C. (1998). Property specification patterns for finite-state verification. In: 2nd Workshop on Formal Methods in Software Practice.
[16] Dwyer, M. B., Avrunin, G. S., & Corbett J. C.(1999). Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering.
[17] Dwyer, M. B., & Clarke, L. A. (1994). Data flow analysis for verifying properties of concurrent programs. In: Proceedings of the ACM SIGSOFT ’94 Symposium on the Foundations of Software Engineering, pp. 62–75.
[18] Gamma, E., Helm, R., Jonhson, R., & Vlissides. J. (1994). Design patterns: Elements of reusable object-oriented software. Addison-Wesley.
[19] Gurgens, S., Lopez, J., & Peralta, R. (1999). Efficient detection of failure modes in electronic commerce protocols. In: DEXA Workshop, pp. 850–857.
[20] Har’El, Z. & Kurshan, R. (1990). Software for analytical development of communications protocols. AT&T Technical Journal, 69(1), 45–59.
[21] Hughes, G. E., & Cresswell M. J. (1984). A companion to modal logic. London: Methuen. · Zbl 0625.03005
[22] Jr., W. M., Murta, C. D., Campos, S. V. A., & Neto D. O. G. (2002). Sistemas de comercio eletronico, projeto e desenvolvimento. Campus.
[23] McMillan, K. L. (1992). Symbolic m odel c hecking. An a pproach to the s tate e xplosion p roblem. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA.
[24] McMillan, K.L. (1993). Symbolic m odel c hecking. Norwell Massachusetts: Kluwer Academic Publishers.
[25] Lamport, L. (1994). The temporal logic of actions. TOPLAS, 16(3), 872–923. · doi:10.1145/177492.177726
[26] McMillan, K. (1992). The SMV system DRAFT.
[27] Milgrom, P. (1985). The economics of competitive bidding: A selective survey. In L. Horwicz, D. Schmeidler, and H. Sonneschein, (eds.).
[28] Milgrom, P. (1989). Auctions and bidding: A Primer. Journal of Economic Perspectives, 3, 3–22.
[29] Milgrom, P., & Robert Weber. (1982). A theory of auctions and competitive bidding. Econometrica, 50, 1089–1122. · Zbl 0487.90017 · doi:10.2307/1911865
[30] Pereira, A., Song, M., Gorgulho, G., Meira Jr., W., & Campos S. (2002). A formal methodology to specify e-commerce systems. In: Proceedings of the 4th International Conference on Formal Engineering Methods. Shanghai, China. · Zbl 1015.68576
[31] Cleaveland, R. Parrow, J.,& Steffen, B.(1993). The concurrency workbench : A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1), 36–72.
[32] Bryant, R.E. (1986). Graph-b ased a lgorithms for b oolean f unction m anipulation. IEEE Transactions on Computers C-35(8), 677–691. · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819
[33] Campos, S. V. (1996). A quantitative approach to the formal verification of real-time systems. Ph.D. thesis, School of Computer Science, Carnegie Mellon University.
[34] Song, M., Pereira, A., Lima, F., Gorgulho, G., Campos, S., & Meira Jr., W. (2003). Extending UML to specify and verify e-commerce systems. In: Proceedings of the Fifteenth International Conference on Software Engineering Knowledge Engineering. San Francisco, USA.
[35] Systems, F. (1999). FDR: A Tool for Checking the Failures-Divergence Preorder of CSP.
[36] Visa, M. (1997). Secure electronic transaction (SET) specification book 1,2,3.
[37] Vickrey, W. (1961). Counterspeculation, auctions, and competitive sealed tenders. Journal of Finance, 16, 8–37. · doi:10.2307/2977633
[38] Wang, W., Hidvégi, Z., Bailey, A., & Whinston, A. (2000). E-process design and assurance using model checking. In: IEEE Computer.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.