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

DOI10.1007/978-3-030-30942-8_14MaRDI QIDQ6535951zbMATHFDO

Authors Artur Oliveira Gomes, Andrew Butterfield

Publication date 14 March 2024

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)

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}

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• A refinement strategy for Circus
• Computing maximal weak and other bisimulations
• FDR3 -- a modern refinement checker for CSP
• FM 2005: Formal Methods
• From LOTOS to LNT
• Guarded commands, nondeterminacy and formal derivation of programs
• Isabelle/UTP: a mechanised theory engineering framework
• Modeling in Event B. System and software engineering.
• Test generation from state based use case models
• Unifying theories in ProofPower-Z
• ZRC -- A refinement calculus for \(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)