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

DOI10.1007/S00165-011-0183-6MaRDI QIDQ1941896zbMATH OpenOpenAlexFDO

Authors 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

CSPexpressivenesshyperpropertiesmodel-checkingrefinement-testing

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1693430
• On the expressive power of CSP refinement
• On CSP refinement tests that run multiple copies of a process
• FDR3 -- a modern refinement checker for CSP
• Model checking under fairness in ProB and its application to fair exchange protocols

Cites work

• A Complete Axiomatic Semantics for the CSP Stable-Failures Model
• Appraising fairness in languages for distributed programming
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CONCUR 2005 – Concurrency Theory
• Defining liveness
• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• scientific article; zbMATH DE number 3902016 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 1982198 (Why is no real title available?)
• scientific article; zbMATH DE number 1863165 (Why is no real title available?)
• On the expressive power of CSP refinement
• Proof principles of CSP -- CSP-prover in practice
• Proving the Correctness of Multiprocess Programs
• Responsiveness of interoperating components
• Revivals, stuckness and the hierarchy of CSP models
• Safety, liveness and fairness in temporal logic
• Specification of communicating processes: temporal logic versus refusals-based refinement
• The existence of refinement mappings
• The stable revivals model in CSP-Prover
• Theoretical Aspects of Computing – ICTAC 2005
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(10)

• Reducing complex CSP models to traces via priority
• On the expressive power of CSP refinement
• scientific article; zbMATH DE number 1693430 (Why is no real title available?)
• On CSP refinement tests that run multiple copies of a process
• Model checking under fairness in ProB and its application to fair exchange protocols
• Foundations for using linear temporal logic in Event-B refinement
• Inputs and Outputs in CSP
• FDR3 -- a modern refinement checker for CSP
• Testing using CSP Models: Time, Inputs, and Outputs
• Integrated Formal Methods

Describes a project that uses

Uses Software

• Isabelle
• CSP-prover
• FDR2
• SPIN

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1941896)