Operational semantics for model checking Circus

DOI10.1007/11526841_17MaRDI QIDQ5716879zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Leo Freitas, Jim Woodcock

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b27882

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Testing for refinement in \textsf{Circus}
• A UTP semantics for \textsf{Circus}
• Type checking \textsf{Circus} specifications
• The semantics of Circus
• Encoding Circus programs in ProofPower-Z

Cited in

(13)

• A UTP semantics for \textsf{Circus}
• FDR explorer
• Automated verification of reactive and concurrent programs by calculation
• Type checking \textsf{Circus} specifications
• Specification coverage for testing in Circus
• The semantics of Circus
• Model checking RAISE applicative specifications
• Operational semantics for fun and profit
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Towards a model-checker for \textit{\textsf{Circus}}
• \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
• Testing for refinement in \textsf{Circus}
• A process algebraic framework for specification and validation of real-time systems

Describes a project that uses

Uses Software

• Circus
• ProofPower

This page was built for publication: Operational semantics for model checking Circus

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