Author, Subjects, Keywords

Cited Author

 
 
   » By Author or Editor
 » Browse Author by Alphabet
 » By Journal
 » By Subjects
 » By Affiliations
 » By Type
 » By Year
 » By Latest Additions
 
 
   » By Author
 » Top 20 Authors
 » Top 20 Article
 » Top 20 Journal Cited
 » Top 20 Cited
 » Top 20 Author Cited
 » Usage Since Sept 2007


 
 
 

Login | Create Account

Testing the Satisfiability of Z Formal Specifications by Using Prolog

Abdullah Mohd. Zin, and Zarina Shukur, (2004) Testing the Satisfiability of Z Formal Specifications by Using Prolog. Malaysian Journal of Computer Science, 17 (1). pp. 42-51. ISSN 0127-9084

Full text not available from this repository.

Official URL: http://mjcs.fsktm.um.edu.my/detail.asp?AID=287

Affiliations

Universiti Kebangsaan Malaysia

Abstract

Formal specifications are now being used as a basis for communication, design, testing and verification of a software product. For a formal specification to be used effectively, it must be valid, which means that it must be well-formed and reflects the user requirements. The normal technique for validating a formal specification is by using formal reasoning. However, the use of formal reasoning is extremely tedious and time consuming. In this paper we explore alternative techniques for validating a Z formal specification. In particular, we consider the concept of satisfiability as a weaker alternative to validity and discuss how testing can be used to check the satisfiability of a Z formal specification.

Item Type:Journal
Keywords:Formal specification, Z formal specification, Validation and verification
Subjects:Q Science
ID Code:418

J. V. Guttag, “Notes on Types Abstraction (Version 2)”. IEEE Trans Software Engineering, Vol. 6 No. 1, Jan 1980, pp. 13-23.

D. E Knuth and P. B. Bendix, “Simple Word Problem in Universal Algebra”, in Computational Problem in Abstract Algebra, Pergamon Press, 1970, pp. 263-297.

A. J. J. Dick, “An Introduction to Knuth-Bendix Completion”, The Computer Journal, Vol. 34, No. 1, Jan 1991, pp 2-15.

B. Potter, J. Sinclair and D. Till, An Introduction to Formal Specification and Z. Prentice-Hall, Inc. 1996.

J. M. Spivey, “Specifying a Real-Time Kernel”. IEEE Software, Vol. 7, No. 5, Sept 1990, pp. 21-28.

B. Field, and M. Elvang-Gorasson, “A VDM Case Study in Mural”. IEEE Trans Software Engineering, Vol. 18, No. 4, April 1992, pp. 279-295.

R. S. Pressman, Software Engineering: A Practioner’s Approach. McGraw-Hill, Inc. 2001.

M. E. Fagan, “Design and Code Inspection to Reduce Errors in Program Development”. IBM System Journal, Vol. 15, No. 3, 1976, pp. 182-211.

E. P. Doolan, “Experience with Fagan’s Inspection Method”. Software – Practice and Experience, Vol. 22, No. 2, Feb 1992, pp. 173-182.

J. C. S. Leite, and P. A. Freeman, “Requirement Validation Through Viewpoint Resolution”, IEEE Trans Software Engineering, Vol. 17, No. 12, Dec 1991, pp. 1253-1269.

S Ohlsson, and P. Langley, PRISM: Tutorial and Manual. Feb 1986. Dept of Computer Science, Univ of California.

J. C. King, “Symbolic Execution and Program Testing”. Communication of the ACM, Vol. 19, July 1976, pp. 385-394.

R. A. Kemmerer, “Testing Formal Specifications to Detect Design Errors”. IEEE Trans Software Engineering, Vol. 11, No. 1, Jan 1985, pp. 32-43.

R. Kneuper, “Symbolic Execution as a Tool for Validation of Specification”. PhD Thesis, Manchester University, 1989.

P. Jalote, “Testing the Completeness of Specifiations”. IEEE Trans Software Engineering, Vol. 15, No. 5, May 1989, pp. 526-531.

Abdullah bin Mohd Zin and E Foxley, “Software Tools for Animating a Z Specification”. Sains Malaysiana, Vol. 24, No. 4, Dis 1995, pp. 67-89.

A. D. Heath, Introductory Logic and Formal Methods. Alfred Waller Ltd, Publishers, 1994.

Repository Staff Only: item control page
 
 
 
 
 
   
© Copyright 2007 MyAIS Faculty of Computer Science and Information Technology, University of Malaya – All Rights Reserved. Malaysian Abstracting and Indexing System is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.