Circus2CSP: A tool for model-checking circus using FDR
![Thumbnail](/themes/edepositireland/images/white_rectangle.jpeg)
File Type:
PDFItem Type:
Journal ArticleDate:
2019Access:
openAccessCitation:
Gomes, A.O. & Butterfield, A., Circus2CSP: A tool for model-checking circus using FDR, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11800 LNCS, 2019, 235-242Download Item:
Abstract:
In this paper, we introduce Circus2CSP, a tool that automatically translates Circus into 𝐶𝑆𝑃𝑀, with an implementation based on a published manual translation scheme. This scheme includes new and modified translation rules that emerged as a result of experimentation. We addressed issues with FDR state-space explosion, by optimising our models using the Circus Refinement Laws. We briefly describe the usage of Circus2CSP along with a discussion of some experiments comparing our tool with the literature.
URI:
https://link.springer.com/chapter/10.1007%2F978-3-030-30942-8_15http://hdl.handle.net/2262/91359
Author's Homepage:
http://people.tcd.ie/butrfeld
Author: Butterfield, Andrew; Gomes, Artur Oliveira
Type of material:
Journal ArticleURI:
https://link.springer.com/chapter/10.1007%2F978-3-030-30942-8_15http://hdl.handle.net/2262/91359
Collections
Series/Report no:
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics);11800 LNCS;
Availability:
Full text availableKeywords:
Model checking, Unifying theories of programming, Circus, CSPDOI:
http://dx.doi.org/10.1007/978-3-030-30942-8_15Metadata
Show full item recordLicences: