On the limits of refinement-testing for model-checking CSP

DOI10.1007/s00165-011-0183-6zbMath1259.68131OpenAlexW1979287973MaRDI QIDQ1941896

Toby Murray

Publication date: 22 March 2013

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

Full work available at URL: https://doi.org/10.1007/s00165-011-0183-6

zbMATH Keywords

model-checkingCSPexpressivenesshyperpropertiesrefinement-testing

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Foundations for using linear temporal logic in Event-B refinement

Uses Software

• Isabelle
• SPIN
• CSP-prover
• FDR2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Specification of communicating processes: temporal logic versus refusals-based refinement
• Revivals, stuckness and the hierarchy of CSP models
• Defining liveness
• Appraising fairness in languages for distributed programming
• Safety, liveness and fairness in temporal logic
• Responsiveness of interoperating components
• On the expressive power of CSP refinement
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Proving the Correctness of Multiprocess Programs
• The Stable Revivals Model in CSP-Prover
• Proof Principles of CSP – CSP-Prover in Practice
• Theoretical Aspects of Computing – ICTAC 2005
• Tools and Algorithms for the Construction and Analysis of Systems
• A Complete Axiomatic Semantics for the CSP Stable-Failures Model
• CONCUR 2005 – Concurrency Theory

This page was built for publication: On the limits of refinement-testing for model-checking CSP