{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T22:25:22Z","timestamp":1648851922859},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron Commerce Res"],"published-print":{"date-parts":[[2006,10]]},"DOI":"10.1007\/s10660-006-8676-8","type":"journal-article","created":{"date-parts":[[2006,9,27]],"date-time":"2006-09-27T22:29:49Z","timestamp":1159396189000},"page":"265-303","source":"Crossref","is-referenced-by-count":3,"title":["The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems"],"prefix":"10.1007","volume":"6","author":[{"given":"A.","family":"Pereira","sequence":"first","affiliation":[]},{"given":"M.","family":"Song","sequence":"additional","affiliation":[]},{"given":"G.","family":"Gorgulho","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"11","key":"8676_CR1","doi-asserted-by":"crossref","first-page":"1204","DOI":"10.1109\/32.106975","volume":"17","author":"G. S. Avrunin","year":"1991","unstructured":"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\u20131222.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8676_CR2","unstructured":"Bolignano. (1997). Towards the formal verification of electronic commerce protocols. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop."},{"issue":"3","key":"8676_CR3","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/52.391826","volume":"12","author":"J. P. Bowen","year":"1995","unstructured":"Bowen, J. P. & Hinchey, M. G. (1995). Seven more myths of formal methods. IEEE Software 12(3), 34\u201341.","journal-title":"IEEE Software"},{"key":"8676_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R. E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8).","DOI":"10.1109\/TC.1986.1676819"},{"key":"8676_CR5","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/ICCD.1995.528793"},{"key":"8676_CR6","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/WIFT.1995.515482"},{"key":"8676_CR7","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/REAL.1994.342709"},{"key":"8676_CR8","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., & Roveri M. (1998). NuSMV: A reimplementation of smv."},{"key":"8676_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., & Roveri M. (1999). NuSMV: A new symbolic model verifier.","DOI":"10.1007\/3-540-48683-6_44"},{"key":"8676_CR10","unstructured":"Cimatti, A., & Roveri M. (1997). User Manual."},{"issue":"2","key":"8676_CR11","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"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\u2013263.","journal-title":"TOPLAS"},{"key":"8676_CR12","volume-title":"Model checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke, E. M., Grumberg, O., & Peled D. A. (1999). Model checking. Cambridge, Massachusetts: The MIT Press."},{"key":"8676_CR13","doi-asserted-by":"crossref","unstructured":"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).","DOI":"10.1145\/232069.232086"},{"key":"8676_CR14","unstructured":"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."},{"key":"8676_CR15","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/298595.298598"},{"key":"8676_CR16","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/302405.302672"},{"key":"8676_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer, M. B., & Clarke, L. A. (1994). Data flow analysis for verifying properties of concurrent programs. In: Proceedings of the ACM SIGSOFT \u201994 Symposium on the Foundations of Software Engineering, pp. 62\u201375.","DOI":"10.1145\/193173.195295"},{"key":"8676_CR18","unstructured":"Gamma, E., Helm, R., Jonhson, R., & Vlissides. J. (1994). Design patterns: Elements of reusable object-oriented software. Addison-Wesley."},{"key":"8676_CR19","doi-asserted-by":"crossref","unstructured":"Gurgens, S., Lopez, J., & Peralta, R. (1999). Efficient detection of failure modes in electronic commerce protocols. In: DEXA Workshop, pp. 850\u2013857.","DOI":"10.1109\/DEXA.1999.795293"},{"issue":"1","key":"8676_CR20","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"Z. Har\u2019El","year":"1990","unstructured":"Har\u2019El, Z. & Kurshan, R. (1990). Software for analytical development of communications protocols. AT&T Technical Journal, 69(1), 45\u201359.","journal-title":"AT&T Technical Journal"},{"key":"8676_CR21","volume-title":"A companion to modal logic","author":"G. E. Hughes","year":"1984","unstructured":"Hughes, G. E., & Cresswell M. J. (1984). A companion to modal logic. London: Methuen."},{"key":"8676_CR22","unstructured":"Jr., W. M., Murta, C. D., Campos, S. V. A., & Neto D. O. G. (2002). Sistemas de comercio eletronico, projeto e desenvolvimento. Campus."},{"key":"8676_CR23","unstructured":"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."},{"key":"8676_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic m odel c hecking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L. (1993). Symbolic m odel c hecking. Norwell Massachusetts: Kluwer Academic Publishers."},{"issue":"3","key":"8676_CR25","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L. (1994). The temporal logic of actions. TOPLAS, 16(3), 872\u2013923.","journal-title":"TOPLAS"},{"key":"8676_CR26","doi-asserted-by":"crossref","unstructured":"McMillan, K. (1992). The SMV system DRAFT.","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"8676_CR27","unstructured":"Milgrom, P. (1985). The economics of competitive bidding: A selective survey. In L. Horwicz, D. Schmeidler, and H. Sonneschein, (eds.)."},{"key":"8676_CR28","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1257\/jep.3.3.3","volume":"3","author":"P. Milgrom","year":"1989","unstructured":"Milgrom, P. (1989). Auctions and bidding: A Primer. Journal of Economic Perspectives, 3, 3\u201322.","journal-title":"Journal of Economic Perspectives"},{"key":"8676_CR29","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.2307\/1911865","volume":"50","author":"P. Milgrom","year":"1982","unstructured":"Milgrom, P., & Robert Weber. (1982). A theory of auctions and competitive bidding. Econometrica, 50, 1089\u20131122.","journal-title":"Econometrica"},{"key":"8676_CR30","unstructured":"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."},{"key":"8676_CR31","doi-asserted-by":"crossref","unstructured":"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\u201372.","DOI":"10.1145\/151646.151648"},{"issue":"8","key":"8676_CR32","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E. (1986). Graph-b ased a lgorithms for b oolean f unction m anipulation. IEEE Transactions on Computers C-35(8), 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"8676_CR33","unstructured":"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."},{"key":"8676_CR34","unstructured":"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."},{"key":"8676_CR35","unstructured":"Systems, F. (1999). FDR: A Tool for Checking the Failures-Divergence Preorder of CSP."},{"key":"8676_CR36","unstructured":"Visa, M. (1997). Secure electronic transaction (SET) specification book 1,2,3."},{"key":"8676_CR37","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1111\/j.1540-6261.1961.tb02789.x","volume":"16","author":"W. Vickrey","year":"1961","unstructured":"Vickrey, W. (1961). Counterspeculation, auctions, and competitive sealed tenders. Journal of Finance, 16, 8\u201337.","journal-title":"Journal of Finance"},{"key":"8676_CR38","unstructured":"Wang, W., Hidv\u00e9gi, Z., Bailey, A., & Whinston, A. (2000). E-process design and assurance using model checking. In: IEEE Computer."}],"container-title":["Electronic Commerce Research"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10660-006-8676-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10660-006-8676-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10660-006-8676-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T16:49:52Z","timestamp":1559234992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10660-006-8676-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":38,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["8676"],"URL":"https:\/\/doi.org\/10.1007\/s10660-006-8676-8","relation":{},"ISSN":["1389-5753","1572-9362"],"issn-type":[{"value":"1389-5753","type":"print"},{"value":"1572-9362","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]}}}