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

DOI10.1007/s00165-011-0183-6zbMath1259.68131MaRDI 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-checking; CSP; expressiveness; hyperproperties; refinement-testing

Mathematics Subject Classification ID

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

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Foundations for using linear temporal logic in Event-B refinement

Uses Software

• Isabelle
• SPIN
• CSP-prover
• FDR2

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item