{"references": ["Jusoh J. A. (2009). Formal Specification and Validation for Pattern\nScanning. (Master Thesis, Universiti Malaysia Terengganu).", "Jusoh J.A., Saman M.Y.M. and Man M. (2011). \"Formal Validation of\nDNA Database Using Theorem Proving Technique\". In International\nJournal of the Computer, the Internet and Management. 19:74 \u2013 78.", "Li G. (2010). Formal Verification of Programs and Their\nTransformations. (PhD Thesis, University of Utah).", "Pederson D. O. (2010). 'Introduction to Formal Verification. Center for\nElectronic Systems Design\".\nHttp//:embedded.eecs.berkeley.edu/research/vis/doc/VisUser/visuser/\nnode4.html/accessed on 04/07/2014.", "Pnueli A. (2002). \"Deductive Verification in Action. Analysis of\nReactive Systems, NYU, Fall, 2008\".\nhttp://www.wisdom.weizman.ac.il/~amir/course02a/header.html/accesse\nd on 04/07/2014.", "Saaltink M. (1999). \"Proving Theorems\" in The Z/EVES 2.0 User's\nGuide Ch. 5.", "Spivey J. M. (1998). \"Tutorial Introduction\" in The Z Notation: A\nReference Manual. pp 1-17."]}

The web services applications for digital reference service (WSDRS) of LIS model is an informal model that claims to reduce the problems of digital reference services in libraries. It uses web services technology to provide efficient way of satisfying users' needs in the reference section of libraries. The formal WSDRS model consists of the Z specifications of all the informal specifications of the model. This paper discusses the formal validation of the Z specifications of WSDRS model. The authors formally verify and thus validate the properties of the model using Z/EVES theorem prover.