Verifying data refinements using a model checker
type: Item
instance of: scholarly article
title: Verifying data refinements using a model checker
zbMATH Open document ID: 1105.68074
author: Graeme Smith
author: John Derrick
published in: Formal Aspects of Computing
publication date: 2006-11-17T00:00:00Z
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5073784
zbMATH Keywords: State-based specifications
zbMATH Keywords: Z Refinement
zbMATH Keywords: Downward and upward simulations
zbMATH Keywords: Model checking
zbMATH Keywords: CTL
describes a project that uses: NuSMV
describes a project that uses: Z
MaRDI profile type: Publication
full work available at URL: s00165-006-0002-7
OpenAlex ID: W2019701393
cites work: A singleton failures semantics for communicating sequential processes
cites work: Q4818818
cites work: Q2754081
cites work: Q2724177
cites work: Relational concurrent refinement
cites work: Data Refinement
cites work: Q4385542
cites work: Q4494252
cites work: A state-based approach to communicating processes
cites work: Q2763965
cites work: Model-checking CSP-Z: Strategy, tool support and industrial application
cites work: Q4472176
cites work: On the expressive power of CSP refinement
cites work: Specification, refinement and verification of concurrent systems -- an integration of Object-\(Z\) and \(CSP\)
cites work: Q4940107
cites work: Q4818812
cites work: Q4436972
cites work: ZB 2005: Formal Specification and Development in Z and B
cites work: Q4301167
DOI: 10.1007/S00165-006-0002-7
description: scientific article; zbMATH DE number 5073784