{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T17:34:50Z","timestamp":1754156090429,"version":"3.41.2"},"reference-count":51,"publisher":"Emerald","issue":"2","license":[{"start":{"date-parts":[[2015,6,15]],"date-time":"2015-06-15T00:00:00Z","timestamp":1434326400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.emerald.com\/insight\/site-policies"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,6,15]]},"abstract":"\n Purpose<\/jats:title>\n \u2013 This paper aims to present the verification process conducted to assess the functional correctness of the voting system. Consejo Nacional de Investigaciones Cient\u00edficas y T\u00e9cnicas (CONICET) is the most important research institution in Argentina. It depends directly from Argentina\u2019s President but its internal authorities are elected by around 8,000 research across the country. During 2011, the CONICET developed a Web voting system to replace the traditional mail-based process. In 2012 and 2014, CONICET conducted two Web election with no complaints from candidates and voters. Before moving the system into production, CONICET asked the authors to conduct a functional and security assessment of it. <\/jats:p>\n <\/jats:sec>\n \n Design\/methodology\/approach<\/jats:title>\n \u2013 This process is the result of integrating formal, semi-formal and informal verification activities from formal proof to code inspection and model-based testing. <\/jats:p>\n <\/jats:sec>\n \n Findings<\/jats:title>\n \u2013 Given the resources and time available, a reasonable level of confidence on the correctness of the application could be transmitted to senior management. <\/jats:p>\n <\/jats:sec>\n \n Research limitations\/implications<\/jats:title>\n \u2013 A formal specification of the requirements must be developed. <\/jats:p>\n <\/jats:sec>\n \n Originality\/value<\/jats:title>\n \u2013 Formal methods and semi-formal activities are seldom applied to Web applications.<\/jats:p>\n <\/jats:sec>","DOI":"10.1108\/ijwis-11-2014-0042","type":"journal-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T13:21:20Z","timestamp":1433337680000},"page":"183-204","source":"Crossref","is-referenced-by-count":1,"title":["Formal and semi-formal verification of a web voting system"],"prefix":"10.1108","volume":"11","author":[{"given":"Maximiliano","family":"Cristia","sequence":"first","affiliation":[]},{"given":"Claudia","family":"Frydman","sequence":"additional","affiliation":[]}],"member":"140","reference":[{"key":"key2020122304252686200_b1","doi-asserted-by":"crossref","unstructured":"Am\u00e1lio, N.\n , \n Stepney, S.\n and \n Polack, F.\n (2004), \u201cFormal proof from UML models\u201d, in Davies, J., Schulte, W. and Barnett, M. (Eds), 6th International Conference on Formal Engineering Methods, Seattle, WA, 8-12 November, pp. 418-433.","DOI":"10.1007\/978-3-540-30482-1_35"},{"key":"key2020122304252686200_b2","doi-asserted-by":"crossref","unstructured":"Am\u00e1lio, N.\n , \n Stepney, S.\n and \n Polack, F.\n (2006), \u201cA formal template language enabling metaproof\u201d, in \n Misra, J.\n , \n Nipkow, T.\n and \n Sekerinski, E.\n (Eds), 14th International Symposium on Formal Methods, Hamilton, 21-27 August, pp. 252-267.","DOI":"10.1007\/11813040_18"},{"key":"key2020122304252686200_b3","unstructured":"Barnes, J.\n , \n Chapman, R.\n , \n Johnson, R.\n , \n Widmaier, J.\n , \n Cooper, D.\n and \n Everett, B.\n (2006), \u201cEngineering the Tokeneer enclave protection software\u201d, Proceedings of the IEEE International Symposium on Secure Software Engineering, Washington, DC."},{"key":"key2020122304252686200_b4","doi-asserted-by":"crossref","unstructured":"Bartetzko, D.\n , \n Fischer, C.\n , \n M\u00f6ller, M.\n and \n Wehrheim, H.\n (2001), \u201cJass \u2013 java with assertions\u201d, \n Electronic Notes in Theoretical Computer Science\n , Vol. 55 No. 2, pp. 103-117.","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"key2020122304252686200_b5","doi-asserted-by":"crossref","unstructured":"Berdine, J.\n , \n Cook, B.\n and \n Ishtiaq, S.\n (2011), \u201cSlayer: memory safety for systems-level code\u201d, in Gopalakrishnan, G. and Qadeer, S. (Eds), 23rd International Conference, Snowbird, UT, 14-20 July, pp. 178-183.","DOI":"10.1007\/978-3-642-22110-1_15"},{"key":"key2020122304252686200_b6","unstructured":"Blanchet, B.\n , \n Cousot, P.\n , \n Cousot, R.\n , \n Feret, J.\n , \n Mauborgne, L.\n , \n Min\u00e9, A.\n , \n Monniaux, D.\n and \n Rival, X.\n (2002), \n The Essence of Computation\n , Springer-Verlag, New York, NY, pp. 85-108."},{"key":"key2020122304252686200_b7","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N.\n and \n Huisman, M.\n (2002), \u201cFormal specification and static checking of gemplus\u2019 electronic purse using ESC\/Java\u201d, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, London, pp. 272-289.","DOI":"10.1007\/3-540-45614-7_16"},{"key":"key2020122304252686200_b8","unstructured":"Flanagan, C.\n , \n Leino, K.R.M.\n , \n Lillibridge, M.\n , \n Nelson, G.\n , \n Saxe, J.B.\n and \n Stata, R.\n (2013), \n Extended Static Checking for Java\n , Compaq Systems Research Center, Palo Alto, CA."},{"key":"key2020122304252686200_b12","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M.\n , \n Albertengo, P.\n , \n Frydman, C.S.\n , \n Pl\u00fcss, B.\n and \n Monetti, P.R.\n (2011a), \u201cApplying the test template framework to aerospace software\u201d, in \n Rash, J.L.\n and \n Rouff, C.\n (Eds), \n 34th IEEE Software Engineering Workshop (SEW\n ), Limerick, pp. 128-137.","DOI":"10.1109\/SEW.2011.25"},{"key":"key2020122304252686200_b10","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M.\n , \n Albertengo, P.\n and \n Rodr\u00edguez Monetti, P.\n (2010), \u201cPruning testing trees in the test template framework by detecting mathematical contradictions\u201d, in Fiadeiro, J.L. and Gnesi, S. (Eds), 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), Pisa, pp. 268-277.","DOI":"10.1109\/SEFM.2010.31"},{"key":"key2020122304252686200_b9","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M.\n and \n Frydman, C.S.\n (2014), \u201cA functional verification of a web voting system\u201d, in Murgante, B., Misra, S., Rocha, A.M.A.C., Torre, C.M., Rocha, J.G., Falc\u00e3o, M.I., Taniar, D., Apduhan, B.O. and Gervasi, O. (Eds), 14th International Conference, Guimar\u00e3es, 30 June-3 July, pp. 640-655.","DOI":"10.1007\/978-3-319-09144-0_44"},{"key":"key2020122304252686200_b11","unstructured":"Cristi\u00e1, M.\n and \n Pl\u00fcss, B.\n (2010), \u201cGenerating natural language descriptions of Z test cases\u201d, in Kelleher, J.D., Namee, B.M., van der Sluis, I., Belz, A., Gatt, A. and Koller, A. (Eds), The International Natural Language Generation Conference, Dublin, pp. 173-177."},{"key":"key2020122304252686200_b14","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M.\n , \n Albertengo, P.\n , \n Frydman, C.S.\n , \n Pl\u00fcss, B.\n and \n Rodr\u00edguez Monetti, P.\n (2014), \u201cTool support for the test template framework\u201d, \n Software Testing, Verification and Reliability\n , Vol. 24 No. 1, pp. 3-37.","DOI":"10.1002\/stvr.1477"},{"key":"key2020122304252686200_b13","unstructured":"Cristi\u00e1, M.\n , \n Rossi, G.\n and \n Frydman, C.\n (2012), \u201c{log} as a test case generator for the test template framework\u201d, Technical report, Dipartimento di Matematica, Universit\u00e0 di Parma, Parma."},{"key":"key2020122304252686200_b15","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M.\n , \n Hollmann, D.\n , \n Albertengo, P.\n , \n Frydman, C.S.\n and \n Monetti, P.R.\n (2011b), \u201cA language for test case refinement in the Test Template Framework\u201d, in Qin, S. and Qiu, Z. (Eds), 13th International Conference on Formal Engineering Methods, Durham, 26-28 October, pp. 601-616.","DOI":"10.1007\/978-3-642-24559-6_40"},{"key":"key2020122304252686200_b16","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M.\n and \n Frydman, C.S.\n (2012), \u201cExtending the Test Template Framework to deal with axiomatic descriptions, quantifiers and set comprehensions\u201d, in \n Derrick, J.\n , \n Fitzgerald, J.A.\n , \n Gnesi, S.\n , \n Khurshid, S.\n , \n Leuschel, M.\n , \n Reeves, S.\n and \n Riccobene, E.\n (Eds), Third International Conference, ABZ 2012, Pisa, 18-21 June, pp. 280-293.","DOI":"10.1007\/978-3-642-30885-7_20"},{"key":"key2020122304252686200_b17","doi-asserted-by":"crossref","unstructured":"Dong, J.S.\n , \n Sun, J.\n and \n Wang, H.H.\n (2002), \u201cZ approach to semantic web\u201d, in George, C. and Miao, H. (Eds), 4th International Conference on Formal Engineering Methods, Shanghai, 21-25 October, pp. 156-167.","DOI":"10.1007\/3-540-36103-0_18"},{"key":"key2020122304252686200_b18","doi-asserted-by":"crossref","unstructured":"Frade, M.J.\n and \n Pinto, J.S.\n (2011), \u201cVerification conditions for source-level imperative programs\u201d, \n Computer Science Review\n , Vol. 5 No. 3, pp. 252-277.","DOI":"10.1016\/j.cosrev.2011.02.002"},{"key":"key2020122304252686200_b21","unstructured":"Freitas, L.\n (2004), \u201cZ\/Eves extended Z toolkit\u201d, Technical Report, University of York, Heslington."},{"key":"key2020122304252686200_b20","doi-asserted-by":"crossref","unstructured":"Freitas, L.\n , \n Fu, Z.\n and \n Woodcock, J.\n (2007), \u201cPosix file store in z\/eves: an experiment in the verified software repository\u201d, 12th IEEE International Conference on Engineering Complex Computer Systems, Auckland, pp. 3-14.","DOI":"10.1109\/ICECCS.2007.36"},{"key":"key2020122304252686200_b19","doi-asserted-by":"crossref","unstructured":"Freitas, L.\n and \n Woodcock, J.\n (2008), \u201cMechanising mondex with z\/eves\u201d, \n Formal Aspects of Computing\n , Vol. 20, pp. 117-139.","DOI":"10.1007\/s00165-007-0059-y"},{"key":"key2020122304252686200_b22","doi-asserted-by":"crossref","unstructured":"Gomes, A.O.\n and \n Oliveira, M.V.\n (2009), \u201cFormal specification of a cardiac pacing system\u201d, Proceedings of the 2nd World Congress on Formal Methods, Berlin, pp. 692-707.","DOI":"10.1007\/978-3-642-05089-3_44"},{"key":"key2020122304252686200_b23","unstructured":"Haidar, A.N.\n , \n Coveney, P.V.\n , \n Abdallah, A.E.\n , \n Ryan, P.Y.A.\n , \n Beckles, B.\n , \n Brooke, J.M.\n and \n Jones, M.A.S.\n (2009), \u201cFormal modelling of a usable identity management solution for virtual organizations\u201d, in \n Bryans, J.\n and \n Fitzgerald, J.S.\n (Eds), Formal Aspects of Virtual Organisations 2009 (FAVO2009), Electronic Proceedings in Theoretical Computer Science (EPTCS), Eindhoven, pp. 41-50."},{"key":"key2020122304252686200_b24","unstructured":"Hartig, K.\n , \n Gerlach, J.\n , \n Soto, J.\n and \n Busse, J.\n (2010), \u201cFormal specification and automated verification of safety-critical requirements of a railway vehicle with frama-c\/Jessie\u201d, in \n Schnieder, E.\n and \n Tarnai, G.\n (Eds), \n Formal Methods for Automation and Safety in Railway and Automotive Systems\n , Springer, pp. 145-153."},{"key":"key2020122304252686200_b25","unstructured":"ISO\n (2002), \u201cInformation technology \u2013 Z formal specification notation \u2013 syntax, type system and semantics\u201d, Technical Report ISO\/IEC 13568, International Organization for Standardization."},{"key":"key2020122304252686200_b26","unstructured":"Jackson, M.\n (1995), \n Software Requirements & Specifications: A Lexicon of Practice, Principles and Prejudices\n , ACM Press\/Addison-Wesley Publishing, New York, NY."},{"key":"key2020122304252686200_b27","doi-asserted-by":"crossref","unstructured":"Jacky, J.\n (1996), \n The Way of Z: Practical Programming with Formal Methods\n , Cambridge University Press, New York, NY.","DOI":"10.1017\/CBO9780511574924"},{"key":"key2020122304252686200_b28","doi-asserted-by":"crossref","unstructured":"Jacobs, B.\n (2004), \u201cWeakest pre-condition reasoning for java programs with jml annotations\u201d, \n The Journal of Logic and Algebraic Programming\n , Vol. 58 Nos 1\/2, pp. 61-88.","DOI":"10.1016\/j.jlap.2003.07.005"},{"key":"key2020122304252686200_b29","unstructured":"Jones, C.\n and \n Bonsignour, O.\n (2011), \n The Economics of Software Quality\n , Addison-Wesley."},{"key":"key2020122304252686200_b30","unstructured":"Khan, S.A.\n , \n Hashmi, A.A.\n , \n Alhumaidan, F.\n and \n Zafar, N.A.\n (2012), \u201cSemantic web specification using Z-notation\u201d, \n Life Science Journal\n , Vol. 9 No. 4."},{"key":"key2020122304252686200_b31","doi-asserted-by":"crossref","unstructured":"King, S.\n , \n Hammond, J.\n , \n Chapman, R.\n and \n Pryor, A.\n (2000), \u201cIs proof more cost-effective than testing?\u201d, \n IEEE Transactions on Software Engineering\n , Vol. 26 No. 8, pp. 675-686.","DOI":"10.1109\/32.879807"},{"key":"key2020122304252686200_b32","doi-asserted-by":"crossref","unstructured":"March\u00e9, C.\n , \n Paulin-Mohring, C.\n and \n Urbain, X.\n (2004), \u201cThe krakatoa tool for certificationof java\/javacard programs annotated in jml\u201d, \n Journal of Logic and Algebraic Programming\n , Vol. 58 Nos 1\/2, pp. 89-106.","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"key2020122304252686200_b33","unstructured":"Moy, Y.\n and \n Wallenburg, A.\n (2010), \u201cTokeneer: beyond formal program verification\u201d, Proceeding 5th International Congress on Embedded Real Time Software and Systems (ERTS\u201910), Toulouse."},{"key":"key2020122304252686200_b34","doi-asserted-by":"crossref","unstructured":"Philippaerts, P.\n , \n M\u00fchlberg, J.T.\n , \n Penninckx, W.\n , \n Smans, J.\n , \n Jacobs, B.\n and \n Piessens, F.\n (2014), \u201cSoftware verification with VeriFast: industrial case studies\u201d, \n Science of Computer Programming\n , Vol. 82 No. 1, pp. 77-97.","DOI":"10.1016\/j.scico.2013.01.006"},{"key":"key2020122304252686200_b35","unstructured":"Roscoe, A.W.\n (1997), \n The Theory and Practice of Concurrency\n , Prentice Hall PTR, Upper Saddle River, NJ."},{"key":"key2020122304252686200_b36","unstructured":"Saaltink, M.\n (1999), \n The Z\/EVES 2.0 User\u2019s Guide\n , Ora Canada."},{"key":"key2020122304252686200_b37","unstructured":"Saaltink, M.\n (1997a), \u201cThe Z\/EVES mathematical toolkit version 2.2 for Z\/EVES version 1.5\u201d, Technical Report, ORA Canada."},{"key":"key2020122304252686200_b38","doi-asserted-by":"crossref","unstructured":"Saaltink, M.\n (1997b), \u201cThe Z\/EVES system\u201d, in \n Bowen, J.P.\n , \n Hinchey, M.G.\n and \n Till, D.\n (Eds), 10th International Conference of Z Users, Reading, 3-4 April, pp. 72-85.","DOI":"10.1007\/BFb0027284"},{"key":"key2020122304252686200_b39","unstructured":"Saff, D.\n (2014), \u201cJUnit.org \u2013 resources for test driven development\u201d, available at: http:\/\/junit.org\/"},{"key":"key2020122304252686200_b40","unstructured":"Spivey, J.M.\n (1992), \n The Z Notation: A Reference Manual\n , Prentice Hall International, Hertfordshire."},{"key":"key2020122304252686200_b41","unstructured":"SpringSource\n (2013a), \n Grails \u2013 The Search is Over\n , SpringSource."},{"key":"key2020122304252686200_b42","unstructured":"SpringSource\n (2013b), \n Groovy \u2013 A Dynamic Language for the Java Platform\n , SpringSource."},{"key":"key2020122304252686200_b43","unstructured":"Sqali, M.\n , \n Trojet, W.\n , \n Torres, L.\n and \n Frydman, C.\n (2009), \u201cCombining interaction and state based modelling to validate system specification via simulation and formal methods\u201d, Winter Simulation Conference (WSC 2009), Poster Session, Austin, TX."},{"key":"key2020122304252686200_b44","doi-asserted-by":"crossref","unstructured":"Stocks, P.\n and \n Carrington, D.\n (1996), \u201cA framework for specification-based testing\u201d, \n IEEE Transactions on Software Engineering\n , Vol. 22 No. 11, pp. 777-793.","DOI":"10.1109\/32.553698"},{"key":"key2020122304252686200_b45","unstructured":"Sun, J.\n , \n Zhang, H.\n and \n Wang, H.\n (2005), \u201cFormal semantics and verification for feature modeling\u201d, ICECCS \u201905: Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems, Washington, DC, pp. 303-312."},{"key":"key2020122304252686200_b46","unstructured":"Trojet, W.\n , \n Sqali, M.\n , \n Frydman, C.\n , \n Torres, L.\n and \n el-amine Hamri, M.\n (2009), \u201cValidating the global behaviour of a system described with scenarios using GDEVS and Z\u201d, 21th European Modeling and Simulation Symposium (EMSS0\u20329), Tenerife - Canary Islands."},{"key":"key2020122304252686200_b47","doi-asserted-by":"crossref","unstructured":"Wang, H.H.\n , \n Gibbins, N.\n , \n Payne, T.R.\n and \n Redavid, D.\n (2012), \u201cA formal model of the semantic web service ontology (WSMO)\u201d, \n Information Systems\n , Vol. 37 No. 1, pp. 33-60.","DOI":"10.1016\/j.is.2011.07.003"},{"key":"key2020122304252686200_b48","doi-asserted-by":"crossref","unstructured":"Woodcock, J.\n and \n Freitas, L.\n (2006), \u201cZ\/eves and the mondex electronic purse\u201d, in \n Barkaoui, K.\n , \n Cavalcanti, A.\n and \n Cerone, A.\n (Eds), \n Theoretical Aspects of Computing - ICTAC (2006\n ), Springer Berlin Heidelberg, pp. 15-34.","DOI":"10.1007\/11921240_2"},{"key":"key2020122304252686200_b49","doi-asserted-by":"crossref","unstructured":"Yuan, C.\n , \n He, Y.\n , \n He, J.\n and \n Zhou, Z.\n (2006), \u201cA verifiable formal specification for rbac model with constraints of separation of duty\u201d, in \n Lipmaa, H.\n , \n Yung, M.\n and \n Lin, D.\n (Eds), \n Information Security and Cryptology\n , Springer Berlin Heidelberg, pp. 196-210.","DOI":"10.1007\/11937807_16"},{"key":"key2020122304252686200_b50","unstructured":"Zafar, N.A.\n , \n Khan, S.A.\n and \n Araki, K.\n (2012), \u201cTowards the safety properties of moving block railway interlocking system\u201d, \n International Journal of Innovative Computing, Information and Control\n , Vol. 8 No. 8."},{"key":"key2020122304252686200_b51","unstructured":"Zeigler, B.P.\n , \n Kim, T.G.\n and \n Praehofer, H.\n (2000), \n Theory of Modeling and Simulation\n , Academic Press, Orlando, FL."}],"container-title":["International Journal of Web Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.emeraldinsight.com\/doi\/full-xml\/10.1108\/IJWIS-11-2014-0042","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/IJWIS-11-2014-0042\/full\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/IJWIS-11-2014-0042\/full\/html","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T22:24:23Z","timestamp":1753395863000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.emerald.com\/ijwis\/article\/11\/2\/183-204\/160893"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,15]]},"references-count":51,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,6,15]]}},"alternative-id":["10.1108\/IJWIS-11-2014-0042"],"URL":"https:\/\/doi.org\/10.1108\/ijwis-11-2014-0042","relation":{},"ISSN":["1744-0084"],"issn-type":[{"type":"print","value":"1744-0084"}],"subject":[],"published":{"date-parts":[[2015,6,15]]}}}