Validation of the Formal Model of Web Services Applications for Digital Reference Service of Library Information System
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.
[1] Jusoh J. A. (2009). Formal Specification and Validation for Pattern
Scanning. (Master Thesis, Universiti Malaysia Terengganu).
[2] Jusoh J.A., Saman M.Y.M. and Man M. (2011). “Formal Validation of
DNA Database Using Theorem Proving Technique”. In International
Journal of the Computer, the Internet and Management. 19:74 – 78.
[3] Li G. (2010). Formal Verification of Programs and Their
Transformations. (PhD Thesis, University of Utah).
[4] Pederson D. O. (2010). ‘Introduction to Formal Verification. Center for
Electronic Systems Design”.
Http//:embedded.eecs.berkeley.edu/research/vis/doc/VisUser/visuser/
node4.html/accessed on 04/07/2014.
[5] Pnueli A. (2002). “Deductive Verification in Action. Analysis of
Reactive Systems, NYU, Fall, 2008”.
http://www.wisdom.weizman.ac.il/~amir/course02a/header.html/accesse
d on 04/07/2014.
[6] Saaltink M. (1999). “Proving Theorems” in The Z/EVES 2.0 User’s
Guide Ch. 5.
[7] Spivey J. M. (1998). “Tutorial Introduction” in The Z Notation: A
Reference Manual. pp 1-17.
[1] Jusoh J. A. (2009). Formal Specification and Validation for Pattern
Scanning. (Master Thesis, Universiti Malaysia Terengganu).
[2] Jusoh J.A., Saman M.Y.M. and Man M. (2011). “Formal Validation of
DNA Database Using Theorem Proving Technique”. In International
Journal of the Computer, the Internet and Management. 19:74 – 78.
[3] Li G. (2010). Formal Verification of Programs and Their
Transformations. (PhD Thesis, University of Utah).
[4] Pederson D. O. (2010). ‘Introduction to Formal Verification. Center for
Electronic Systems Design”.
Http//:embedded.eecs.berkeley.edu/research/vis/doc/VisUser/visuser/
node4.html/accessed on 04/07/2014.
[5] Pnueli A. (2002). “Deductive Verification in Action. Analysis of
Reactive Systems, NYU, Fall, 2008”.
http://www.wisdom.weizman.ac.il/~amir/course02a/header.html/accesse
d on 04/07/2014.
[6] Saaltink M. (1999). “Proving Theorems” in The Z/EVES 2.0 User’s
Guide Ch. 5.
[7] Spivey J. M. (1998). “Tutorial Introduction” in The Z Notation: A
Reference Manual. pp 1-17.
@article{"International Journal of Information, Control and Computer Sciences:70883", author = "Zainab M. Musa and Nordin M. A. Rahman and Julaily A. Jusoh", title = "Validation of the Formal Model of Web Services Applications for Digital Reference Service of Library Information System", abstract = "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.", keywords = "Validation, verification, formal, theorem proving.", volume = "9", number = "8", pages = "1959-7", }