Accession Number : ADA290230

Title :   Exploiting Symmetry in the Model Checking of Relational Specifications,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Jackson, Daniel

PDF Url : ADA290230

Report Date : DEC 1994

Pagination or Media Count : 23

Abstract : Errors in a software design can be detected early on by analyzing a formal model expressed in a specification language such as Z. Since software designs tend to involve infinite (or at least very big) state spaces, it has been assumed that this analysis cannot be automated. Consequently, few formal specifications have been extensively analyzed, and the potential for early detection of errors has not been realized. This paper argues that, while proving properties of designs may be intractable, detecting errors may not be. State transitions of an operation can be enumerated exhaustively, within a scope' defined by the user that places a bound on the size of state components. Symmetry can then be exploited to reduce this finite state space. A state can be shown to be symmetrical, in the context of the analysis, to a state already examined, and thus guaranteed not to reveal an error. Preliminary experiments with a prototype are promising. A small scope often seems sufficient to catch errors, and exhibits enough symmetry to reduce search by a factor of 10 or more.

Descriptors :   *SOFTWARE ENGINEERING, *SYMMETRY, *ERROR DETECTION CODES, COMPUTER PROGRAMS, DETECTION, SPECIFICATIONS, PROGRAMMING LANGUAGES, ERRORS, TRANSITIONS, EQUATIONS OF STATE.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE