Malaysian Journal of Computer Science (ISSN 0127-9084)
Indexing Page
Visit the official web site at

Article Information
Title:Testing the Satisfiability of Z Formal Specifications by Using Prolog
Auhtor(s): Abdullah Mohd. Zin ,Zarina Shukur,
Journal:Malaysian Journal of Computer Science (ISSN 0127-9084)
Volume:17, No 1
Keywords:Formal specification, Z formal specification, Validation and verification
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.

Volume Listing