Browsing by Author "Butterfield, Andrew"
Now showing items 1-8 of 8
-
Applying Formal Verification to an Open-Source Real-Time Operating System
Butterfield, Andrew (Springer Nature Switzerland, 2023)This paper describes work done using formal methods to verify parts of the RTEMS real-time operating system, as part of an activity sponsored by the European Space Agency to qualify multi-core processors for spaceflight. ... -
Circus2CSP: A tool for model-checking circus using FDR
Butterfield, Andrew; Gomes, Artur Oliveira (2019)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 ... -
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]), ... -
The Inner and Outer Algebras of Unified Concurrency
Butterfield, Andrew (2019)Algebras have always played a critical role in Unifying Theories of Programming, especially in their role in providing the "laws" of programming. The algebraic laws form a triad with two other forms, namely operational ... -
Slotted-Circus: A UTP-Family of Reactive Theories
Butterfield, Andrew (Springer, 2007)We present a generic framework of UTP theories for describing systems whose behaviour is characterised by regular time-slots, compatible with the general structure of the Circus language [WC01a]. This ?slotted-Circus? ... -
Towards a model-checker for circus
Butterfield, Andrew; Gomes, Artur Oliveira (2019)Among several approaches aiming at the correctness of systems, model-checking is one technique to formally assess system models regarding their desired/undesired behavioural properties. We aim at model-checking the Open ... -
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 ...