Verifying Statemate Statecharts Using CSP and FDR (2008)
Abstract. We propose a framework for the verification of statecharts. We use the CSP/FDR framework to model complex systems designed in statecharts, and check for system consistency or verify special...
CHARACTERIZATIONS OF SIMPLY-CONNECTED FINITE POLYHEDRA IN 3-SPACE (2008)
The following result was discovered by the authors during investigations into the topological problems of three-dimensional pictorial data analysis: THEOREM 1. Let Y be a connected finite polyhedron...
Abstract. A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved. The possibilities of nondetermimsm are...
DENOTAPIONAL SEMANTICS FOR OCCAN (2008)
ABSTRACT. A denota~ional semantics is given for a large subset of occam, a programming language for concurrent systems. ~e semantic domain used is a "failure-sets " model modified...
Published 1997, revised to 2000 and lightly revised to 2005. Contents i The original version is in print in April 2005 with Prentice-Hall (Pearson). This version is made available for personal...
Abstract WLFM 2005 Preliminary Version A taxonomy of web services using CSP (2008)
Lee Momtahan, Andrew Martin, A. W. Roscoe
Terms such as conversational and stateless are widely used in the taxonomy of web services. We give formal definitions of these terms using the CSP process algebra. Within this framework we also...
IOS Press Nets with tokens which carry data (2008)
Ranko Lazić C, Tom Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell
Abstract. We study data nets, a generalisation of Petri nets in which tokens carry data from linearlyordered infinite domains and in which whole-place operations such as resets and transfers are...
A CSP solution to the "trains " problem (2008)
The problem as stated leaves one in doubt as to what one must do. Is one meant to abstractly specify the safety and liveness properties one desires of the network? Is one meant to provide some...
Consistency in Distributed Databases (2007)
We introduce, and prove correct, two novel algorithms for preserving a form of consistency in distributed databases arranged as rings. The first uses as its model databases with a fixed number of...
R. S. Lazic, T. C. Newcomb, T. C. Newcomb, A. W. Roscoe, A. W. Roscoe
On model checking data-independent systems with arrays without reset
T. C. Newcomb, A. W. Roscoe, Coventry Cv Al
model checking data-independent systems with arrays without reset
T. C. Newcomb, A. W. Roscoe, Coventry Cv Al
model checking data-independent systems with arrays without reset
Systems With Arrays, T. C. Newcomb, A. W. Roscoe
A system is data-independent with respect to a data type X i the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output...
Responsiveness and stable revivals (2007)
J. N. Reed, A. W. Roscoe, J. E. Sinclair
Abstract. Individual components in an inter-operating system require assurance from other components both of appropriate functionality and of suitable responsiveness. We have developed properties...
Nets with tokens which carry data (2007)
Ranko Lazić, Tom Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell
Abstract. We study data nets, a generalisation of Petri nets in which tokens carry data from linearly-ordered infinite domains and in which whole-place operations such as resets and transfers are...
Revivals, stuckness and the hierarchy of CSP models (2007)
We give details of a new model for CSP introduced in response to work by Fournet et al [8]. This is the stable revivals model R alluded to in [22]. We provide the full semantics for CSP in this...
Bootstrapping multi-party ad-hoc security (2006)
S. J. Creese, M. H. Goldsmith, A. W. Roscoe, Ming Xiao
Increasingly pervasive computing throws up scenarios where users may wish to achieve some degree of security in their interaction with other people or equipment, in contexts where the entities...
On the relationship between web services security and traditional protocols (2005)
XML and Web Services security specifications define elements to incorporate security tokens within a SOAP message. We propose a method for mapping such messages to an abstract syntax in the style of...
On model checking data-independent systems with arrays without reset (2004)
Lazic, R. S., Newcomb, T. C., Roscoe, A. W.
A system is data-independent with respect to a data type X iff the operations it can perform on values of type X are restricted to just equality testing. The system may also store, input and output...
Seeing beyond divergence (2004)
A long-standing complaint about the theory of CSP has been that all theories which encompass divergence are divergence-strict, meaning that nothing beyond the first divergence can be seen. In this...
Internalising agents in CSP protocol models (2002)
We carry forward the work described in our previous papers [2, 11, 9] on the application of data independence to the model checking of cryptographic protocols using CSP [10] and FDR [4], often via...
Internalising agents in CSP protocol models (2002)
We carry forward the work described in our previous papers [3, 12, 10] on the application of data independence to the model checking of cryptographic protocols using CSP [11] and FDR [5], often via...
What can you decide about resetable arrays? (preliminary version (2001)
We investigate the decidability of reachability specifications in programs data-independent in two types X and Y, and which can contain arrays X Y. We show that this type of specification is...
What can you decide about resetable arrays? (preliminary version (2001)
We investigate the decidability of reachability specifications in programs data-independent in two types X and Y, and which can contain arrays X Y. We show that this type of specification is...
The Successes and Failures of Behavioural Models (2000)
A. W. Roscoe, G. M. Reed, R. Forster
Concurrency is a complex and fascinating subject, and the ways in which a system composed of many processes running in parallel and interacting with each other might behave would seem to most people...
Automating data independence (2000)
P. J. Broadfoot, G. Lowe, A. W. Roscoe
Abstract. In this paper, we generalise and fully automate the use of data independence techniques in the analysis of security protocols, developed in [16, 17]. In [17], we successfully applied these...
Automating data independence (2000)
P. J. Broadfoot, G. Lowe, A. W. Roscoe
Abstract. In this paper, we generalise and fully automate the use of data independence techniques in the analysis of security protocols, developed in [16, 17]. In [17], we successfully applied these...
Data Independent Induction over structured networks (2000)
We extend the classes of network which Data Independent Induction can be used to reason about. Through the use of constants and predicates in the data independent type we build proofs of structured...
What is intransitive noninterference (1999)
The term “intransitive noninterference ” refers to the information flow properties required of systems like downgraders, in which it may be legitimate for information to flow indirectly between...
What is intransitive noninterference (1999)
The term "intransitive noninterference " refers to the information flow properties required of systems like downgraders, in which it may be legitimate for information to flow...
Proving Security Protocols With Model Checkers By Data Independence Techniques (1999)
Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols -- see, for example [16, 20] and many of the papers in [7]. Their use in...
Exploiting Data Independence (1999)
was responsible for the first serious applications of model checkers to security protocols. So succesful was this work that it is now widely immitated across the entire model checking community (with...
Formal Verification of Arbitrary Network Topologies (1999)
We show how data independence results can be used to generalise an inductive proof from binary to arbitrary branching tree networks. The example used is modelled on the RSVP Resource Reservation...
Verifying an infinite family of inductions simultaneously using data independence and FDR (1999)
We present a technique for formally establishing results for scalable systems, such as distributed systems and communication protocol networks, where the results are independent of the system's...
What is Intransitive Noninterference? (1999)
The term "intransitive noninterference" refers to the information flow properties required of systems like downgraders, in which it may be legitimate for information to flow indirectly...
What is intransitive noninterference (1999)
The term “intransitive noninterference ” refers to the information flow properties required of systems like downgraders, in which it may be legitimate for information to flow indirectly between...
Mislove, M. W., Nivat, M., Reed, G. M., Roscoe, A. W., Wachter, R. F.
CONTENTS: MW. Mislove, G.M. Reed, A. W Roscoe and R. F. Wachter Foreword S. Abramsky Preface % Abramsky Proofs as processes G. Bellin and P.j Scott On the it-calculus and linear logic D. Galmiche and...
Nivat, M., Mislove, M. W., Reed, G. M., Roscoe, A. W., Wachter, R. F.
This issue is devoted to some of the papers that were submitted to the Proceedings of the meeting on the Mathematical Foundations of Programming Semantics that took place at the University of Oxford...
Nivat, M., Mislove, M. W., Reed, G. M., Roscoe, A. W., Wachter, R. F.
This is the last of three special issues of TCS devoted to the Proceedings of the meeting on the Mathematical Foundations of Programming Semantics that took place at the University of Oxford in...
Proving Security Protocols With Model Checkers By Data Independence Techniques (1998)
Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols -- see, for example [11, 12, 14] and many of the papers in [3]. Their use in...
Intensional Specifications of Security Protocols (1998)
It is often difficult to specify exactly what a security protocol is intended to achieve, and there are many example of attacks on protocol which have been proved to satisfy the `wrong', or too...
TTP: A case study in combining induction and data independence (1998)
The TTP, or Time Triggered Protocol is designed as an ecient mechanism for diagnosing faulty members of a network of peer processes. It exists in a number of versions and can be considered at a...
On Transition Systems and Non-Well-Founded Sets (1996)
(Labelled) transition systems are relatively common in theoretical computer science, chiey as vehicles for operational semantics. The rst part of this paper constructs a hierarchy of canonical...
Modelling and verifying key-exchange protocols using CSP and FDR (1995)
We discuss the issues involved in modelling and verifying key-exchange protocols within the framework of CSP and its model-checking tool FDR. Expressing such protocols within a process algebra forces...
CSP and determinism in security modelling (1995)
We show how a variety of confidentiality properties can be expressed in terms of the abstraction mechanisms that CSP provides. We argue that determinism of the abstracted low-security viewpoint...
Fixed points without completeness (1995)
M. W. Mislove, M. W. Mislove, A. W. Roscoe, A. W. Roscoe, S. A. Schneider, S. A. Schneider
This paper presents a simplification and generalisation of Barrett's "Fixed point theory of unbounded nondeterminism (FACS 3) " for untimed CSP. The difficulties of modelling...
Non-interference through Determinism (1994)
The standard approach to the specification of a secure system is to present a (usually state-hased) abstract security model separately from the specification of the system's functional...
Unbounded Non-determinism in CSP (1993)
We show how the standard failures/divergences model for CSP can be extended by adding to each process' representation the set of all infinite traces it can perform. This allows a full and...
An Alternative Order for the Failures Model (1992)
The failures-divergences model for CSP is usually presented with the refinement order being the one used for fixed points in the semantics of recursion. The requirement that this order be complete...
Unbounded Nondeterminism in CSP (1988)
ABSTRACT. We extend the failures/divergences model for CSP to include a component of infinite traces. This allows us to give a denotational semantics for a version of CSP including general...
J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, ...
A complete set of algebraic laws is given for Dijkstra’s nondeterministic sequential programming language. Iteration and recursion are explained in terms of Scott’s domain theory as fixed points...
Metric spaces as models for real-time concurrency (1987)
Abstract. We propose a denotational model for real time concurrent systems, based on the failures model for CSP. The fixed point theory is based on the Banach fixed point theorem for complete metric...
An important current area of research in the verification of distributed systems is scalability: how do we handle the verification of realistic sized systems, and families of system under...