Now showing items 1-6 of 6

    • From CCS to CSP: the m-among-n Synchronisation Approach 

      Butterfield, Andrew; Ekembe Ngondi, Gerard; Koutavas, Vasileios (Open Publishing Association, 2022)
      We present an alternative translation from CCS to an extension of CSP based on m-among-n syn chronisation (called CSPmn). This translation is correct up to strong bisimulation. Unlike the g-star renaming approach ([4]), ...
    • Fully Abstract Normal Form Bisimulation for Call-by-Value PCF 

      Koutavas, Vasileios; Lin Hou, Yu (IEEE, 2023)
      We present the first fully abstract normal form bisimulation for call-by-value PCF (PCFv). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental ...
    • Model-checking circus with FDR using circus2csp 

      GOMES, ARTUR OLIVEIRA (Trinity College Dublin. School of Computer Science & Statistics. Discipline of Computer Science, 2019)
      The current lack of tool support for model-checking Circus, a formalism which combines Z, CSP, refinement calculus and Dijkstra's guarded commands, is one of the constraints for its use at industrial scale. Nowadays, it ...
    • Modelling the Haemodialysis Machine with Circus 

      BUTTERFIELD, ANDREW (Springer International Publishing, 2016)
    • Tools for model-based security engineering 

      JUERJENS, JAN; FOX, JORGE (ACM, 2006)
      We present tool-support for checking UML models and C code against security requirements. A framework supports implementing verification routines, based on XMI output of the diagrams from UML CASE tools, and on control ...
    • Translation of CCS into CSP, Correct up to Strong Bisimulation 

      Butterfield, Andrew; Ekembe Ngondi, Gerard; Koutavas, Vasileios (Springer, 2021)
      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 ...