Verifying data refinements using a model checker

DOI10.1007/S00165-006-0002-7zbMath1105.68074OpenAlexW2019701393MaRDI QIDQ851129

Graeme Smith, John Derrick

Publication date: 17 November 2006

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-006-0002-7

zbMATH Keywords

CTLModel checkingDownward and upward simulationsState-based specificationsZ Refinement

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (5)

Model Checking Simulation Rules for Linearizability ⋮ On using data abstractions for model checking refinements ⋮ Alloy as a Refactoring Checker? ⋮ Checking Z Data Refinements Using Traces Refinement ⋮ Model checking action system refinements

Uses Software

• NuSMV
• Z

Cites Work

• Relational concurrent refinement
• A state-based approach to communicating processes
• A singleton failures semantics for communicating sequential processes
• On the expressive power of CSP refinement
• Data Refinement
• ZB 2005: Formal Specification and Development in Z and B
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Specification, refinement and verification of concurrent systems -- an integration of Object-\(Z\) and \(CSP\)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verifying data refinements using a model checker