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

DOI10.1007/978-3-030-30942-8_15zbMATH Open1539.68164MaRDI QIDQ6535952FDOQ6535952

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

• Towards a model-checker for \textit{\textsf{Circus}}
• FM 2005: Formal Methods
• Type checking \textsf{Circus} specifications
• Stateflow diagrams in Circus
• Testing for refinement in \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?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• Computing maximal weak and other bisimulations
• FDR3 -- a modern refinement checker for CSP
• FM 2005: Formal Methods
• Guarded commands, nondeterminacy and formal derivation of programs
• Modeling in Event B. System and software engineering.
• Specification of communicating processes: temporal logic versus refusals-based refinement
• Test generation from state based use case models
• ZRC -- A refinement calculus for \(Z\)

Cited in

(1)

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

This page was built for publication: \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR

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