Testing the satisfiability of Z formal specifications by using prolog

Research output: Contribution to journalArticle

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.

Original languageEnglish
Pages (from-to)42-51
Number of pages10
JournalMalaysian Journal of Computer Science
Volume17
Issue number1
Publication statusPublished - 2004

Fingerprint

Testing
Formal specification
Communication

Keywords

  • Formal specification
  • Validation and verification
  • Z formal specification

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

@article{6e12c923c2c345c5baaa94b79a1f76ee,
title = "Testing the satisfiability of Z formal specifications by using prolog",
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.",
keywords = "Formal specification, Validation and verification, Z formal specification",
author = "{Mohd. Zin}, Abdullah and Zarina Shukur",
year = "2004",
language = "English",
volume = "17",
pages = "42--51",
journal = "Malaysian Journal of Computer Science",
issn = "0127-9084",
publisher = "Faculty of Computer Science and Information Technology",
number = "1",

}

TY - JOUR

T1 - Testing the satisfiability of Z formal specifications by using prolog

AU - Mohd. Zin, Abdullah

AU - Shukur, Zarina

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

KW - Formal specification

KW - Validation and verification

KW - Z formal specification

UR - http://www.scopus.com/inward/record.url?scp=79952777299&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79952777299&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:79952777299

VL - 17

SP - 42

EP - 51

JO - Malaysian Journal of Computer Science

JF - Malaysian Journal of Computer Science

SN - 0127-9084

IS - 1

ER -