Verifying data refinements using a model checker

Smith, Graeme and Derrick, John (2006) Verifying data refinements using a model checker. Formal Aspects of Computing, 18 3: 264-287. doi:10.1007/s00165-006-0002-7

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Smith, Graeme
Derrick, John
Title Verifying data refinements using a model checker
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 0934-5043
Publication date 2006
Sub-type Article (original research)
DOI 10.1007/s00165-006-0002-7
Volume 18
Issue 3
Start page 264
End page 287
Total pages 24
Editor E. Boiten
M. Butler
Place of publication Surrey, United Kingdom
Publisher Springer U. K.
Collection year 2006
Language eng
Subject C1
280302 Software Engineering
700199 Computer software and services not elsewhere classified
Abstract In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.
Keyword State-based Specifications
Z Refinement
Downward And Upward Simulations
Model Checking
Computer Science, Software Engineering
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 3 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 9 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Wed, 15 Aug 2007, 09:28:18 EST