\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

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}

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

• 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
• Specification of communicating processes: temporal logic versus refusals-based refinement
• Title not available (Why is that?)
• ZRC -- A refinement calculus for \(Z\)
• FM 2005: Formal Methods
• Computing maximal weak and other bisimulations
• Title not available (Why is that?)

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)