Towards a model-checker for \textit{\textsf{Circus}}

DOI10.1007/978-3-030-30942-8_14zbMATH Open1539.68163MaRDI QIDQ6535951FDOQ6535951

Authors: Artur Oliveira Gomes, Andrew Butterfield 

Publication date: 14 March 2024

Recommendations

• FM 2005: Formal Methods
• \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
• Type checking \textsf{Circus} specifications
• Testing for refinement in \textsf{Circus}
• A UTP semantics for \textsf{Circus}

zbMATH Keywords

Circus

Mathematics Subject Classification ID

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

Cites Work

• Isabelle/UTP: a mechanised theory engineering framework
• Title not available (Why is that?)
• Modeling in Event B. System and software engineering.
• Guarded commands, nondeterminacy and formal derivation of programs
• Test generation from state based use case models
• FDR3 -- a modern refinement checker for CSP
• Title not available (Why is that?)
• ZRC -- A refinement calculus for \(Z\)
• A refinement strategy for Circus
• FM 2005: Formal Methods
• Computing maximal weak and other bisimulations
• From LOTOS to LNT
• Unifying theories in ProofPower-Z

Cited In (1)

• \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR

This page was built for publication: Towards a model-checker for \textit{\textsf{Circus}}

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