Translation of CCS into CSP, Correct up to Strong Bisimulation
File Type:
PDFItem Type:
Conference PaperDate:
2021Access:
openAccessCitation:
Ekembe Ngondi, Gerard, Koutavas, Vasileios, Butterfield, Andrew, Translation of CCS into CSP, Correct up to Strong Bisimulation, International Conference on Software Engineering and Formal Methods, Software Engineering and Formal Methods (SEFM 21), online, 6-10th December 2021, 243 - 261Abstract:
We present a translation of CCS into CSP which is correct with respect to strong bisimulation. To our knowledge this is the first such translation to enjoy a correctness property. This contributes to the unification of the CCS and CSP families of concurrent calculi, in the spirit of Hoare and He’s unification programme through Unifying Theories of Programming. To facilitate this translation, we define CCSTau, the extension of CCS with visible synchronisation actions and the hiding operator. This separation of concerns between synchronisation and hiding turns out be sufficient to obtain our correct translation. Our translation, implemented in a Haskell prototype, makes it possible to use CSP-based verifiers such as FDR to reason about trace and failure (hence may- and must-testing) preorders for CCS processes.
Sponsor
Grant Number
Marie Curie
754489 (ALECS)
Science Foundation Ireland (SFI)
13/RC/2094
Author's Homepage:
http://people.tcd.ie/butrfeldhttp://people.tcd.ie/ekembeng
http://people.tcd.ie/vkoutav
Other Titles:
Springer LNCSSoftware Engineering and Formal Methods (SEFM 21)
Publisher:
SpringerType of material:
Conference PaperCollections
Series/Report no:
13085;Availability:
Full text availableKeywords:
Concurrency theory, Calculus of Communicating Systems (CCS), Communicating Sequential Processes (CSP), Correct translationSubject (TCD):
CONCURRENCY THEORY , Formal Methods , Formal SemanticsDOI:
10.1007/978-3-030-92124-8_14Metadata
Show full item recordLicences: